I don’t understand what “hacker-proof code means”, but yes IOHK (who develop Cardano) do use formal methods such as Isabelle and Coq alongside some process specification languages.
Code can’t confer immunity to attacks outside the scope of verification methods as implemented. As another poster mentioned above, side channel attacks or hardware vulnerabilities are outside the scope and capabilities of formal verification methods’ ability to mitigate or mediate directly. Which is not to say be verification could be improved to account for this. But if you knew there were no bugs already due to formal verification I guess at least these unknown bugs are likewise much more limited in scope and offset by entire classes of bugs determined to not be present.
You can't verify the OS, you can't verify the network connection between your apps, you can't account for poor business requirements that result in formally verified hackable code, etc...
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?
Can someone explain how this works from a 7/10 technical perspective? I hate reading articles that talk to you like youre five when trying to explain advanced concepts. I just want to know how it works in 1 paragraph and thats it.
I understand your frustration with Quanta on this, and agree completely. I often times make it through about 2/3 of an article and just give up - just get to the point (and preferably open with that point)!
Preach! It's a little surprising to me how often Quanta articles hit the front page here. They are always about a very exciting subject, but they very rarely tell you anything much about that subject.
Rather than knowing your program will work in the sense that a successful compile/execution will tell you, using formal verification you know your program will work in the sense that it will do what you want it to do. It's basically programming via logic proofs.
Careful there. Not "what you want it to". It will work in the sense that it will do what the formal specification says it will. That may or may not be what you actually want it to do. (MCAS, for example, did what the specification said.)
Short version: Write algorithms using mathematically-sound logic whose correctness and properties can be _proven_ the way you might prove the correctness of a math formula.
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.
Wow, that's actually really cool. Thank you so much for such an awesome answer, I learned a lot from your pastebin.
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.
Flow analysis and SMT solvers are mathematically-sound, so if done correctly, a fuzzer would have no luck finding a path through the code where any undefined behavior (or behavior that violates the contracts you've specified) could take place.
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
Dude -- awesome. Thank you so much for writing all that, it was extremely fascinating to read. I'll watch the video now... thanks again. And also that makes perfect sense.
To me fuzzing still helps finding problems the Formal method of choice doesn't cover. Typically my favorite example is stack use or runtime-duration. I can write a parser guaranteed to have no runtime error (bounds, over/underflow, divide by zero) and still make it crash because of stack or heap exhaustion. Or I can find tortuous cases of denial if service. Because the tool doesn't handle (at the moment) stack or heap size, or execution duration.
Fuzzing still helps a lot in those cases! Especially if you focus on those kinds of problems.
I've been trying to teach myself Coq, one of the formal provers mentioned in the article, so I'll try to explain how Coq works, and I'll send you to another website with a tutorial instead of trying to explain how to use it.
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
which is saying that natural numbers may be made in one of two ways, you may take the constructor O at any time, or you may take the constructor S which takes a natural number. O is zero, and S is "successor", meaning +1, so that S(O) is 1 and S(S(S(O))) is 3.
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) : nat
:= fun (X : Type) (f : X → X) (x : X) => n X (m X f) x.
If 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, ...
For equal time and effort, I'm not at all convinced that it's slower. It's easy to underestimate how much time gets spent on debugging, you just don't see it in the up-front cost.
When the rate of bugs coming in from test goes below some threshold that your boss is comfortable with.
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)
But how do you know you have the right proof obligations? It's very easy to discharge a massive number of proof obligations while proving nothing of interest.
Formal methods don't just make bugs and debugging disappear, they just move it to a different domain - the development of the proofs.
I can't make sense of what you're saying. You've completed the proofs when you've discharged all proof obligations. The proof obligations will depend on the formal modelling system you use (Event-B, say), and of course on your formal model. You aren't left in a state of uncertainty as to whether you've finished discharging the proof obligations.
Are you referring to the possibility of errors in your model? That's not the same thing.
> 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?"
> It is very easy to complete a proof on the wrong model
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.)
You have an automatic tool that tells you. Your program won't "compile" unless the proof is correct.
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.
> Formal methods don't make bugs or debugging disappear. They move it to different domain - the development of the proof.
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.
> 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.
But you have access to everything at every stage. There's no need to figure out what the data is or how it got that way - the hard part of debugging - because there is no data, no state, no user input. It's more like fixing a compilation error than debugging.
Do you mean it's miserable to develop the seL4 microkernel or do you mean it's miserable to develop applications on top of seL4? If the latter, is it any different from any other microkernel?
You don't have to jump in 100%, you can just add formal methods to the things that require it. Cryptographic algorithms, network protocols, distributed protocols, etc, could all be completed in Isabelle or Coq and then generate Haskell from the formal spec. For less-critical parts of the system you could use property based testing and various other "semi-formal" techniques which take less time but still add to the overall quality.
I actually work in an agile environment that uses formal methods and it is possible!
SEL4 found the opposite. They could formally verify away run time checks.
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.
I still see your point but quoting the How Amazon Web Services Uses Formal Methods paper:
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.
Type checking, borrow checking and unit testing are similar albeit weaker tools that allow rapid development by providing a safety net.
I'm on the "yes type checking" side of the perennial "which is more efficient" programming language debate, but when we talk about "formal methods" in the context of eradicating security vulnerabilities, the subtext is "formally proving correctness", not simply any tool that increases rigor. I agree, boringly, that there are PL tools that apply rigor to increase development speed.
The belief that software could be affordably proven correct was pervasive in the 70s, it led to a research winter, and now formal methods is very much about adding rigor and catching more bugs (some of the most promising directions in contemporary formal methods research revolve around reducing soundness to help find more bugs more quickly).
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.
The most interesting thing I've seen as far as this is concerned is Taint Analysis. You can label functions as returning user input, some functions take user input and turn it into sanitized input, and there are functions that should never take non-sanitized input.
FWIW the first practical application of input tainting that comes to mind is Perl's circa 2001, although I wouldn't be surprised to hear Smalltalk went there before.
I'm not familar with pyre, but i have experimented with some security static analysis tools. The one's i have experimented with take some normal program and try to analyse it. The analysis is usually far from complete, and as a result has so many false positives that its difficult to adopt.
Anyways, i would say those are rather different from systems where you give an actual proof of correctness.
I hear this claim a lot but I question it's truth. I'm faster with formal tools than without.
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.
You can easily convince me that formal methods are more efficient for complex distributed systems problems, or for cryptographic protocols, or things like that. But even in systems whose whole premise is algorithmic, the hairy stuff provers are designed against are a small part of the overall coding task.
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.
TLA+ doesn't prove anything to be "correct" or "flawless", I find it extremely worrisome that you claim as much. It failed to exhibit traces that violated your invariants, which says something completely different.
I've never actually used TLA+, but my understanding is that it does exhaustive model checking (presumably using some suitable simulation relation), so in this case failure to find a violating trace indicates that no such trace exists, and the invariants always hold.
Correctness might well be defined solely by a set of invariants, so I don't quite understand your point here?
This is correct: the TLA+ model checker (TLC) will check all possible behaviors for the finite model. As the GP said, they were only working with a finite number of workers, but within those constraints it guarantees the spec always satisfies the invariants.
(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.)
exactly. I've proven that in a scenario with a certain number of zones and workers, the invariants and temporal properties cannot be violated.
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.)
Imagine the following scenario, you have encountered an actual bug in concurrent code, and you think it would be great to work on a model and invariants that lets TLA+ find the bug (as an exercise).
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".
I mean, specific to my scenario, my invariant was "only one zone at a time" and the liveness property was "everyone who wants a zone eventually gets one", so respectively:
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?
1. TLA+ doesn't "find" or not find anything. It is a mathematical language for describing systems and assertions about them. There is a proof assistant for TLA+ that checks your formal proofs of theorems that say that your assertions follow from the description, and model checkers that verify your theorems automatically.
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.
There's some truth in that. They force you to scrutinize every line of code. This creates a focus on minimizing attack surface but also produces code with significantly less bugs.
- 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.
> Anyway, formal methods can only help you to protect against attacks that you are already aware.
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.
It depends on what you mean by "formal methods". Fully verifying code is fully correct is extremely expensive. Partially verifying code is somewhat correct is a lot less expensive. Verifying the _design_ you intend to code is less expensive than that, and is actually pretty economical. I wrote about this in-depth here: https://www.hillelwayne.com/post/why-dont-people-use-formal-...
> One of those verified building blocks comes with a proof guaranteeing that someone with access inside one partition won’t be able to escalate their privileges and get inside other partitions.
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.
> "just not the sorted list we were probably hoping for ...
> "For every item j in a list, ensure that the element j ≤ j+1 ... Yet the list [1, 2] also satisfies the definition since it is a sorted list, just not the sorted list we were probably hoping for.
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"?
> That is, given the list [7, 3, 5], she expects that the program will return [3, 5, 7] and satisfy the definition. Yet the list [1, 2] also satisfies the definition since “it is a sorted list, just not the sorted list we were probably hoping for,” Parno said.
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.
Thank you to help point out. I read the specification differently _because_ it we want a sorted list (a lot of implied definitions about input and output). I see how this complements the next paragraph how ambiguous and difficult in can be to write such formal definitions which includes all such cases.
> For every item j in a list, ensure that the element j ≤ j+1
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.
To find the missing constraints, you can try asking what's wrong with the list [1, 2].
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.
Then, you might again try putting in [7,3,5] and get back a list like this: [1,2,3,4,5,6,7]. Again, imagine arguing with the pushy salesman. The salesman says "Look, you wanted a list with the numbers 7, 3, and 5, and you wanted a list in order, this is both of those things, so you have to pay me for my fine list-sorter now!" And again, I would want to object and say something like "but wait a second, I want ONLY the numbers that I gave you in the input list in the output list!". So, you end up with something like:
for each element, j, of the output list, the element j must be in the input list.
Now, you try putting in [7,3,5] again. What's the worst thing that might come out the other end that's still following all of these 3 rules? Can you spot the next problem?
Even 100% formally verified code could be vulnerable to side channel and other hardware attacks. There could also be bugs in the verification system, the compiler, the spec that they’re verifying, nothing is hacker-proof.
Yes, a formal proof shows that a system does not have a specified class of bugs, subject to specific assumptions. This is very valuable, but it is better to think of it as another (very powerful) bug finding technology than a complete assurance that nothing can go wrong.
You're partly right, formal methods don't catch problems that you assume does not happen in your assumptions (herein, the "operational semantics").
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.
I'd like to see a few "hard nuts" created, formally verified secure all the way down to the instruction level on a somewhat simple CPU (i.e. not x86). A BGP server and a DNS server would be a good start. Those have a specific task and a well defined external interface that changes little.
Note that existence of a formal proof for security is no silver bullet. A real world example of this is the WPA2 key exchange's formal proofs not catching the KRACK vulnerability.
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.
There are formal methods both for specs (e.g. TLA+ checked by TLC and TLAPS) and for implementations (e.g. ADA-Spark checked by GNAT). The spec can indeed be checked that invariants or liveness properties are honored.
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.
May I take "I write my specs for machines" to mean that you simply omit the parts of the specification that are not expressible in the formalism at hand?
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.
No, I didn't mean that. in my particular domain (a distributed systems library) I have a collection of specifications for things like commands, locks and collections, which are compact enough that I feel I can describe them fully. There has been one case where I had to simplify the model, which I consider a great failure, since that was the one time I had bugs appear that I didn't catch during model testing.
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?
I agree that you can usefully, formally specify certain behaviors by choosing to ignore, e.g., implementation details. There are a lot of implementation details: stack depth, instruction mix, power consumption, timing fluctuation, memory placement. Incorporate too many, and you lose clarity, even usability.
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.
That's not entirely true. Synthesis is a popular topic within the "formal verification" umbrella.
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.
It's an attractive, succinct way to mislead people about the value of formal methods and their potential.
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.
formal verification continues to come up, but it has the issue that you can only formally verify problem domains you already expect -- and the advanced threat actors for which formal verification is necessary have the toolkit to go off-script to find vulnerabilities.
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.
Type systems can encode invariants even on the protocol level. For example you can hand-write or generate (multi party) session types to avoid deadlocks etc.
this is an interesting approach that I hope we see more of! but i specifically meant to refer to security components of a protocol: e.g. that whether a party can impersonate another with access to some information that is public or can be disclosed via some attack.
>> You’re writing down a mathematical formula that describes the program’s behavior and using some sort of proof checker that’s going to check the correctness of that statement
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?
The idea of formal verification of code is kafkaesque. Its popularity is proportional to the inefficiency and irrationality of the economic system within which it exists.
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.
The difference is that code with bugs can still compile, but proofs that are unsound won't check. Now granted, you can still prove the wrong thing or _not_ prove the thing that is supposed to make your system robust is taking place, so it's still very much a human endeavor with all that entails.
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_.
> 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".
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.
From my shallow understanding, formal verification usually proves the given program always satisfies some properties/specifications. It's pretty good when you expect the software to fully behave in the way you want it to be.
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?
Nobody mentioned Ada/Spark yet? This is doing exactly that, but in a real programming language, not with a seperate proof system. You only write code once.
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.
111 comments
[ 4.1 ms ] story [ 188 ms ] threadWhat's unclear about it?
lazy example : a hardware-level side-channel attack is not rendered impossible simply because the software was made with formal verification methods.
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?
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:
which is saying that natural numbers may be made in one of two ways, you may take the constructor O at any time, or you may take the constructor S which takes a natural number. O is zero, and S is "successor", meaning +1, so that S(O) is 1 and S(S(S(O))) is 3.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:
:= fun (X : Type) (f : X → X) (x : X) => n X (m X f) x.If 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, ...
Look at how little functionality seL4 provides, compared to hobbyist operating systems.
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)
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...
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.
"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.
I actually work in an agile environment that uses formal methods and it is possible!
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...
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.
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.
Correctness might well be defined solely by a set of invariants, so I don't quite understand your point here?
(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.)
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?
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.
- 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.
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...
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:
Then, you might again try putting in [7,3,5] and get back a list like this: [1,2,3,4,5,6,7]. Again, imagine arguing with the pushy salesman. The salesman says "Look, you wanted a list with the numbers 7, 3, and 5, and you wanted a list in order, this is both of those things, so you have to pay me for my fine list-sorter now!" And again, I would want to object and say something like "but wait a second, I want ONLY the numbers that I gave you in the input list in the output list!". So, you end up with something like: Now, you try putting in [7,3,5] again. What's the worst thing that might come out the other end that's still following all of these 3 rules? Can you spot the next problem?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.
This sounds like an interesting idea.
Not all the way down to the instruction level, but it's a start.
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.
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.
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.
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.
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
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?
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.
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.