Formal Verification Creates Hacker-Proof Code (2016)
quantamagazine.org
quantamagazine.org
For instance, this week I needed to build a distributed locking mechanism so a collection of asynchronous actors could only access resources in one region at a time. I described my two requirements in TLA+: only one zone at a time, and everyone who wants a zone eventually gets it (with the assumption nobody goes down forever - weak fairness.) I had several bugs which it caught, until I finally arrived at a protocol that was proven correct (at least for a handful of workers on a handful of zones.) It took around a day from start to finish, and now I know my design is literally flawless.
Sure, I didn't prove it in the general case, nor did I prove that my code implements the spec, but this was still extremely useful! Having the machine check your designs frees you from worrying if you've caught all the races and corner cases.
And for the kind of security this article is talking about, it's not enough to have a proven core algorithm or protocol; your dumb input parsers and output renderers and all that other boring integration code also needs to be bug-free, because those kinds of joinery are where we tend to find vulnerabilities.
2. If you use the model checker, it's not about it "failing to find" a counter example. A model checker result is a proof that no such example exists. True, it is usually a proof about some finite instance of your system description.
3. There is just no such thing as proving a system flawless. Software systems are physical systems exhibiting probabilistic behaviors. At best you can prove things about a mathematical description of a system, which mean that as long as the physical system behaves according to the description, the result follows. Of course, the first part at best holds with some probability.
Correctness might well be defined solely by a set of invariants, so I don't quite understand your point here?
So you start writing a model, and a set of invariants, you run the tool and... it finds nothing. Does that mean you just proved the bug does not exist? No, you _know_ the bug exists, what it means is that you didn't write a correct model on your first try. So you iterate on it, add a few things you missed, put some extra labels, read the docs a bit more, maybe refine your invariants, make them stronger, work through a couple traces that don't actually make sense in practice (e.g. actors just never taking any action whatsoever). During all this time, you either found nothing or things that were not interesting. At no time have you ever proved anything correct, you just iterated on your model until you managed to capture a real life scenario.
It takes some convincing to make the jump from "this model does not violate my invariants" to "I think this model and the invariants are close enough to what I care about that I think it's good enough"... I don't know how to go from there to things like "proven correct" and "flawless".
1. \A z \in Zones: Active(z) => ~\E o \in Zones: z # o /\ Active(o) 2. \A w \in Workers: \A z \in Zones: WorkerWantsZone(w, z) ~> WorkerHasZone(w, z)
Unlike your scenario, I am checking the spec here. I know that code that properly implements the spec satisfies these two properties, therefore I've proven the spec correct. You can disagree on the importance of those two properties but I've mechanically checked that those properties are always preserved in my finite models, so I know the spec is correct, at least for the model size.
You know, it's really not too hard to get started with this stuff. You can always nit-pick but why not try it out and see if it's useful for you?
(This is of course assuming that TLC doesn't have any bugs that would cause it to misreport. By contrast something like randomized testing doesn't guarantee the spec satisfies the invariants even if the tester is bug-free.)
With more work, I could prove the invariants for any number of workers and zones using TLAPS rather than TLC, though I couldn't prove the temporal properties in this way (since TLAPS doesn't support temporal logic, it can only prove invariants.)
Algorithmic invariants: Many optimizations rely on certain properties being always true, so specific checks can be left out or can be replaced by other, more efficient checks. A simple example is that the distinguished idle thread is always in thread state idle and therefore can never be blocked or otherwise waiting for I/O. This can be used to remove checks in the code paths that deal with the idle thread.
https://cacm.acm.org/magazines/2010/6/92498-sel4-formal-veri...
In each, TLA+ has added significant value,
either finding subtle bugs we are sure
we would not have found by other means,
or giving us enough understanding and
confidence to make aggressive performance
optimizations without sacrificing correctness.
There is a small subdiscipline of formal methods that comes from programming language theory (judging by conferences, it makes up no more than 10-20%) that does still have this 1970s "subtext", but actual researchers or practitioners are usually careful with what they actually say, and you'll most often find such claims explicitly made only by fans.
It's all statically-checked and you can incorporate it into your CI/CD: https://pyre-check.org/docs/pysa-basics.html
See also: Property-based testing, and TLA+
Anyways, i would say those are rather different from systems where you give an actual proof of correctness.
- There's no clear definition for formal methods. One of the fundamental problems with 'formal methods' is that it's a very fragmented community of researchers and practitioners (many who never built a real-world software systems). Formal methods depends very much of who you talk with: static analysis, dynamic analysis, type systems, writing specs in Z notation, writing code in a subset of C without malloc, etc.
- Formal methods doesn't produce code: humans produce code. A side note: people forget one of the major successes of 'formal methods' is actually hardware synthesis and verification.
- Security is about risk management. Attack surfaces is a classification of some types of risk but not all. Anyway, formal methods can only help you to protect against attacks that you are already aware. None of this has anything to do with the speed which with code is being produced.
Not sure exactly what you mean here but on its face it isn’t true. Formal Methods are arguably the single best way of protecting you against attacks that you are not already aware of, by eliminating entire classes of bugs, errors or attack vectors, without regard to what type of attacks may be used against them.
Look at how little functionality seL4 provides, compared to hobbyist operating systems.
"A talented programmer can write and verify 4 lines of code a day"
seL4 has some cool ideas, but I can't stress enough how miserable it is to develop for.
Note that formal methods don't get around this as they do nothing for the class of bugs where it works as specified but now that we see it in operation we know the specification was wrong. (once the spec is right though it is faster)
Whether you've proven the right thing still requires judgement - what you end up with is a provably correct implementation of what you thought you wanted. But that's a much smaller problem, and at a minimum you're guaranteed to have an unambiguous definition of what it is you actually built.
That's my point.
Formal methods don't make bugs or debugging disappear. They move it to different domain - the development of the proof.
> what you end up with is a provably correct implementation of what you thought you wanted.
You end up with a provably correct implementation of what you thought you stated on what you thought you wanted.
Serious proofs are highly non-trivial. I've seen experts debate the exact semantics of the most simple properties.
They make the thing we usually call bugs and usually experience as debugging disappear. The thing that remains is a very different activity with very different properties.
Do you write a correct formal spec the first time round? I don't. Proofs sometimes pass or fail when they shouldn't.
When these problem occur I call them bugs, and I call process of finding and fixing them debugging.
What do you find it has in common with the activities that we normally call debugging? For me debugging is characteristically about understanding how a system is behaving, essentially by bisecting: it's all about figuring out what should be the case at each point and identifying the point at which things start to go wrong. Whereas correcting a proof is very different: you immediately know where the problem is, and it's more about coming up with a new lemma or strategy - it's the same kind of activity as writing a new proof/program, whereas (traditional) debugging is very much a separate skill, IME.
A proof can fail for many reasons, and even in the simplest possible case, where the tool provides you with a counter example it could either be a real bug in the design/program/protocol, but there could also be something wrong with the specification you were given, or in your implementation of the specification, or in some assumptions you've made to simplify the proof, or there's ambiguity in the natural language description, or even some typo somewhere.
You now need to understand the domain and the system well enough to come up with an explanation of the phenomena. This is debugging.
Formal methods don't just make bugs and debugging disappear, they just move it to a different domain - the development of the proofs.
Are you referring to the possibility of errors in your model? That's not the same thing.
It is very easy to complete a proof on the wrong model, and there are always errors in the model, at least initially.
There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough? That's quite similar to asking "If you don't use formal methods, how do you know when your work is done?"
That doesn't sound right. Automatic proof assistants/verifiers won't approve your proof unless it really is a proof for the model, right?
> there are always errors in the model, at least initially
Agreed.
> There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough?
It's true that bugs in the model are a possibility.
More broadly, it's possible for defects to get through a formal software-development methodology. There was an interesting case study done on this. [0] Vastly fewer than if formal methods are not used, but you're still right that ultimately it's not a completely rock-solid guarantee. (And that's not counting things like bugs in the proof-assistant, or bugs in the non-verified compiler you end up using.)
[0] https://www.adacore.com/tokeneer ('Analysis' section is on page 59 of PDF)
See also https://blog.adacore.com/tokeneer-fully-verified-with-spark-... , https://github.com/AdaCore/spark2014/tree/master/testsuite/g...
I actually work in an agile environment that uses formal methods and it is possible!
https://galois.com/blog/2017/10/formal-methods-krack-vulnera...
That being said, it's a very valuable tool and should be applied more, not less.
But yeah, fewer bugs is better than more.
The article is presumably referring to the seL4 formally verified operating system. There's not a single mention of it by name, but it lines up, as they're discussing the unmanned Little Bird, which is one of seL4's success stories.
https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597724/
https://www.newscientist.com/article/mg22730392-600-unhackab...
https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
Not all the way down to the instruction level, but it's a start.
This sounds like an interesting idea.
I think the hype around formal verification also tends to misdirect away from the verification that strong type systems already do if used correctly, though vitally not at the protocol level.
For Rust there is https://crates.io/crates/session-types from http://munksgaard.me/papers/laumann-munksgaard-larsen.pdf
Code is an expression of pure logic. So if there is any incorrect assumption or flaw in that logic, it can be verified by simply reading the code.
Given that premise, the usefulness of formal verification can be disproved in a single English sentence:
Formal verification does not remove the element of human error from a system; it removes it from the code and adds it to the system of proofs which verify that code... Proofs can be written with incorrect assumptions (human error) in the same way that code can be written with incorrect assumptions. As one of the people in the article acknowledges, writing good proofs is challenging; "challenging" inescapably means "prone to human error".
Formal verification proponents seem to have conveniently forgotten to apply formal verification to prove the effectiveness of formal verification.
The great irony of this article is that it attempts to rely on exhaustive proof (which is the basis of unit testing) to prove the effectiveness of formal proof - I.e. we tested formal verification with that helicopter that one time and the hackers couldn't hack it for 6 months, therefore formal proof is effective - That's a lousy unit test case and it doesn't prove formal verification.
I think a dedicated red team going after a system for 6 months and not finding anything is a pretty good "unit test", personally. It's _evidence_ of effectiveness, not _proof_.
I think those statements are rather inaccurate, or at a minimum prone to erroneous interpretations. Formal verification is usually based on machine checked proofs. It doesn't matter how much error occurs in the creation of a proof, once it is checked it is known to be a valid proof with mathematical certainty. That does depend on the correctness of the proof checker, but in principle that can be formally verified as well.
I think the main issues with formal verification lie elsewhere than where you seem to be placing them. Such as the problem that the specification itself may be incomplete or contain errors.
If this plan to formally verify internet algorithms included the Wi-Fi standard and implementations, the KRACK vulnerability wouldn't be an issue because it wouldn't verify (with respect to certain specifications, if they realized that those specifications were important to begin with).
But in the first place, most operational semantics on this level still stay at layers of abstraction high enough that they don't guard against Spectre and Meltdown.
Nevertheless, note that formal verification is also widely used at the microchip level.
First, formal verification doesn't create anything. It only certifies code created by other means.
Second, formal verification only certifies that the software implements the machine-expressible details of the spec. It doesn't certify anything expressed only in English.
Finally, it doesn't and can't ever certify that the spec itself is correct or complete. Most bugs and security holes result from incorrect, incomplete, or inconsistent specs. (Any program satisfies an inconsistent spec, but inconsistent specs can at least be identified by formal means.) Very few specs can be formally expressed completely.
So, formal verification is useful, but neither creates hacker-proof code, nor ensures that code is hacker-proof.
I agree that proving the software satisfies some safety properties and is always consistent with some specification doesn't mean that a system is truly "hacker proof".
However:
1. It's a step in the right direction, and something like a necessary condition but not a sufficient condition.
2. It's an attractive, succinct way to describe the value of formal methods and their potential (as the cited DeepSpec project intends to realize) to indeed make a truly hacker-proof system.
Synthesis from specifications completely fails to address omissions and errors in the specifications, except insofar as they get translated to something that is more evidently wrong, or are revealed to be inconsistent.
Some formal modeling tools for specs can actually extract implementations that satisfy the spec, though I think you're being nit-picky on the semantics of "create."
Specs don't have to be English, you know. I write my specs for machines first and humans second.
A specification with parts deliberately omitted is deliberately incomplete. An implementation of a sufficiently incomplete specification may be formally verified to satisfy the spec without ensuring much of anything, although it may suffice to justify payment.
This attitude is typical in formal specification.
Take the example of a reader/writer lock. I claim it's possible to completely define the spec of such a lock, so that any question about the intended behavior of the lock can be decided by the machine. Sure, it's a simple example, but my library is a collection of simple recipes. Do you disagree?
But implementation details are often what hackers rely on.
So, yes, formal modeling is useful, sometimes essential, but does not eliminate hackability. Overselling it does harm.
Here was a lengthier diatribe of mine on a former Quanta article: https://news.ycombinator.com/item?id=22549988
Long version: Formal verification is a broad topic with a lot of different facets. But hopefully this sheds some light on some of the more useful ones:
Model-checkers like TLA+. You can specify an algorithm, say something simple like a bank account transfer where a sender's account is debited, and a receiver's account is credited. You can then set constraints, such that the sender's account must have enough to cover the transfer, etc. TLA+ will then run through all the scenarios in your algorithm to find corner-cases when the constraints aren't met. It's useful for modeling distributed systems, and you can try simulating an algorithm in parallel to see error conditions in multi-threaded code.
The downside to TLA+ is that you produce a specification, but still have to reproduce the specification in compilable/runnable code. I understand Amazon has had a lot of success using TLA+ to wring out potential bugs in systems before implementing them, and Leslie Lamport (author of TLA+ and creator of LaTeX, too) has some great (and entertaining) videos on his website explaining how they work: https://lamport.azurewebsites.net/tla/tla.html
There are formally-verifiable dialects of programming languages like the SPARK dialect of Ada, and Frama-C, which let you specify pre and post-conditions for functions, and then it will perform model-checking with flow analysis and SMT solvers to ensure those conditions are met in a way that's mathematically sound. Some conditions, like lack of buffer or integer overflows, are always checked. This way, code which has passed the proof stage can truly be said to be free of run-time errors, and whatever extra contracts you've added in your code will be met as well. Since all of this is checked at compile/proof-time, there's no run-time penalty for the extra assurance.
I came up with this simple example of SPARK code that proves if I have a function that doubles every element in an array, then the result satisfies a contract where every element in the output is even: https://pastebin.com/BtkaEDQ5
There are also proof assistants and theorem proving tools/languages like HOL, Isabelle, Coq, LEAN, and others which IMO fall under the umbrella of formal verification, but more on the computer science side than software engineering. In contrast, TLA+ and SPARK are very useful and practical for developing high-integrity software. Still, they're programming languages, and you can write executable code in them that can be said to be mathematically sound. A good resource is the Software Foundations course: https://softwarefoundations.cis.upenn.edu/
Some dependently-typed programming languages like Idris, F*, Dafny, and (I think) Liquid Haskell provide different mixes of these capabilities, but are geared towards producing usable software.
So you mentioned that it can handle things like overflows. Does this include all the things a fuzzer might find?
This article says "hacker-proof." Is that hyperbole (which implies 100% certainty in my mind) or is there a margin of error in this type of system. I'm just imagining things how large codebases with lots of maintainers still have bugs found every day from fuzzing. I would imagine if its near 100% that assumes the system that checks it is also free of bugs... quite fun to think about.
Getting started with SPARK, you'll see messages like "Can't prove that this variable won't overflow" (usually with corner cases like "when x = 4,294,967,295 and y = -1"). So it kind of makes you realize how error-prone code can be.
A statement like "x++" has the assumption baked into it that x isn't going to be INT_MAX. Fuzzers work by manipulating your control flow such that x _will_ be INT_MAX and cause an overflow or other bad stuff. Formal verification exposes all those assumptions and when people complain about slow development, it's because you're basically making the code "fuzzer-proof".
"Hacker-proof" is hyperbole, but not as much as some might have you believe. People have pointed out that the specification has to be correct. My code in the pastebin proves every element in the output array is even, but if the code is supposed to produce an array of odd numbers, then obviously that's still a bug, even though it's been "formally verified".
I wouldn't use the term "hacker-proof", but I would say "hacker-resistant". FV _can_ eliminate whole classes of vulnerabilities that attackers could otherwise use. A common trope is "well there's still hardware bugs or the spec could be wrong, so why bother?" I mean, sure, a hacker could cut the power to the datacenter, too, but IMO that's not a reason to ignore tools that can make the software we write much more robust.
One issue that can crop up is that you can't always prove what you're trying to specify. The state space can grow too big and the solver can't figure it out in a timely fashion, so you have to make assumptions and hope your tests give you enough confidence to deploy the system. This is basically the halting problem - it doesn't say that it's impossible to prove termination (or any other property) of some code, it just says that you can't _always_ prove them.
nVidia recently began using SPARK in some of their work, the video does a good job explaining some of the bugs that FV eliminates: https://www.youtube.com/watch?v=DZSSyWlsb28
Fuzzing still helps a lot in those cases! Especially if you focus on those kinds of problems.
In Coq you may define a set in terms of constructors of that set, for instance the set of natural numbers is:
Inductive nat : Set :=
| O : nat
| S : nat -> nat
The language is dependently typed, which means that expressions may be used as types. If you'd like to construct an "int" in C you may give an example such as "4". If you'd like to construct a value with "x < y" type in Coq, you must provide an example, either building it through theorems. As a programmer, it's a process similar to looking through an API manual, you know you have an object of one type and you know the type of the object you need, and you're trying to find the path that gets you one from the other. Often times the function you need won't already exist and you'll have to define a new function in code, then use that function in your proof.
For flavour, here's what that looks like in Coq. This is my attempt at defining natural numbers as Church Numerals, then defining multiplication on them:
Definition nat := ∀ X : Type, (X → X) → X → X.
Definition mult (n m : nat) : natIf you can build up value 'z' whose type is "x < y" then it's important that when you use it, it still be true that x is less than y later. For this reason, Coq is a functional programming language without mutability.
Dependent types have implications across the language. For instance you could have a record (like a C struct) whose three members are a numerator, a denominator, and a proof that the denominator != 0. Another cool thing is that it lets you write more expressive APIs such as a "pop()" function on a queue. In most languages your options are to make it undefined behaviour to pop an empty queue, or return a result type that may contain an error, or use exceptions if your language supports them. In Coq, you may define pop() as a function which takes a parameter whose type is a proof that the queue is not empty when called. (Due to Coq being pure functional, pop() also returns the whole post-pop queue.)
When proving, you have the goal to prove some statement, and some hypotheses that are known true in your current state. You may apply any theorems previously proven to transform your goal or hypothesis. Generally this means breaking the problem down into stages, such as splitting on 'and' and 'or', or performing induction on a variable. This proofing language is different from the programming language.
The best tutorial I've found online is for Lean prover, not Coq, but the concept is the same. (Indeed, other than lean using "rw" where Coq uses "rewrite", I can't recall any differences at all): https://news.ycombinator.com/item?id=22801607
The main problem I have with Coq is its lack of automation. If I understand the history, that's a bit of an ironic statement because Coq's main feature was its automation. The statements to "rewrite based on this theorem" or "split on 'and' and form two goals" are tactics, and Coq allows you to write your own tactics. There's no need for tactics to be proven correct, they can be full of bugs, either they show a path to produce a value with the right type in which case you have a proof, or they do not. My problem is that the Coq developers seem to share an opinion that the user is a mathematician who has considered the problem, developed a proof, attempted to formalize the proof on their own paper, and is as a last step entering their formalized proof into Coq. As a non-mathematician, I have done none of those things. I understand that they avoid doing things that may consume CPU time like trying every combination for a variable, but the "auto" tactic won't try 'true' and 'false' for a single boolean variable.
The one last step is that you can "extract" running code from Coq proofs. I've never done this myself, so I can't speak to it, but the idea is that you want to remove the concern that the code you've proven isn't the code you actually run. Coq can emit OCaml or Haskell.
The obvious flaw in that approach is that clearly the 'proof checker' can itself be vulnerable to human error. Any complex program is going to have many 'proof checkers' which depend on each other to verify different parts of the system; if any assumption about what constitutes a valid proof for any segment of the logic is wrong, then that would introduce a vulnerability in the same way as a regular programming bug would.
So then the real question about the effectiveness of formal verification would be; given the same amount of development time, are incorrect assumptions introduced when writing the 'proof checkers' less likely than bugs introduced when writing regular programming code?
Aren't programming bugs always caused by incorrect assumptions? What is it about formal verification which frees a complex system from the evils of incorrect assumptions?
Incorrect assumptions about the proof or incorrect assumptions about the logic, what is the real practical difference?
However, in terms of security, usually the loopholes come from those parts or in those ways people didn't see them coming - so how do people write specifications about what they don't know?
Use widely in the industry. With such a system you can also generate test cases automatically to verify the assertions. Such as with cbmc for the C language if one cares, and the manager doesn't trust the proof system.
If the input satisfies and happens to be the output in this case, why is article saying this to be a bug? Why "just not the sorted list we were probably hoping for"?
Because the human meant "sort this list", not just "return a sorted list". They put in [7, 3, 5] and got back [1, 2]. Then they realized their specification was incomplete.
What would be the model example for the correct formal definition? When I hear "sort", there are implied constraints/parameters so [1,2] would not have even been a possible solution.
You might imagine trying to have an argument with a person trying to sell you a list sorter. The salesman is just going on and on about how "but look, each element of the list I gave you is in the right order! So you should buy my very nice list sorter!". I would want to yell "but you didn't include any of the numbers from the input list! You just forgot about 7, 3, and 5."
So, another formal constraint might be something like this:
for each element, i, in the input list, the element i must be in the output list.
for each element, j, of the output list, the element j must be in the input list.
What's unclear about it?
You can. Look at seL4. This is an area of ongoing research.
> you can't verify the network connection between your apps
In what sense? You can verify the crypto, and the networking stack.
> you can't account for poor business requirements that result in formally verified hackable code
Not sure what you're saying here. Are you referring to the possibility that the formal specification might not be adequate to guarantee security, even discounting side-channel attacks?
lazy example : a hardware-level side-channel attack is not rendered impossible simply because the software was made with formal verification methods.