22 ms·

Formal Verification Creates Hacker-Proof Code (2016)

102 points by Alekhine 6y ago

dk8996 6y ago
I think this similar to what ADA is doing in crypto space.
- exdsq 6y ago
  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.
  - MaxBarraclough 6y ago
    > I don’t understand what “hacker-proof code means” What's unclear about it?
    - serf 6y ago
      it's not that it's unclear per se, it's just an untenable position to take. lazy example : a hardware-level side-channel attack is not rendered impossible simply because the software was made with formal verification methods.
    - aspenmayer 6y ago
      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.
    - exdsq 6y ago
      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...
      - MaxBarraclough 6y ago
        > You can't verify the OS 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?
Exuma 6y ago
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.
- dfee 6y ago
  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)! Here was a lengthier diatribe of mine on a former Quanta article: https://news.ycombinator.com/item?id=22549988 https://news.ycombinator.com/item?id=22549988
  - twic 6y ago
    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.
- blihp 6y ago
  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.
  - AnimalMuppet 6y ago
    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.)
- docandrew 6y ago
  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 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 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/ 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.
saithound 6y ago
Needs (2016) in the title.
tptacek 6y ago
Formal methods are a powerful security tool because they produce useful code so slowly that they necessarily minimize attack surface.
- exdsq 6y ago
  It doesn’t have to be that slow! The tooling has advanced quite significantly over the last few years.
  - MaxBarraclough 6y ago
    It's still fair to say that formal methods produces software far, far more slowly than ordinary methods. Look at how little functionality seL4 provides, compared to hobbyist operating systems.
    - lmm 6y ago
      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.
      - thanksforfish 6y ago
        If you don't use formal methods, how do you know when your work is done?
        im3w1l 6y ago
        When the checks clear.
        ternaryoperator 6y ago
        One of the finest puns I've seen on HN ever!
        6y ago
MaxBarraclough 6y ago
> 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. https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597724/ https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597724/ https://www.newscientist.com/article/mg22730392-600-unhackable-kernel-could-keep-all-computers-safe-from-cyberattack-2/ https://www.newscientist.com/article/mg22730392-600-unhackab... https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
jzer0cool 6y ago
> "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"?
- computerphage 6y ago
  > 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.
  - jzer0cool 6y ago
    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.
  - jzer0cool 6y ago
    > 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.
    - computerphage 6y ago
      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?
empath75 6y ago
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.
- not2b 6y ago
  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.
- aliceryhl 6y ago
  You might not ever reach 100% confidence, but formally verified code is a whole lot more likely to be correct than code that is not formally verified.
sesutton 6y ago
Doesn't the KRACK vulnerability undermine the idea that formally verified equals perfectly secure?
- jhanschoo 6y ago
  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.
deleted 6y ago
[deleted]
m3kw9 6y ago
And since that time what have they secured?
Animats 6y ago
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.
- miscPerson 6y ago
  Would you mind elaborating just a little? This sounds like an interesting idea.
- docandrew 6y ago
  Here's a formally-verified DNS Server: https://ironsides.martincarlisle.com/ https://ironsides.martincarlisle.com/ Not all the way down to the instruction level, but it's a start.
est31 6y ago
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. https://galois.com/blog/2017/10/formal-methods-krack-vulnerability/ 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.
- rrmm 6y ago
  Yeah the subtitle can be, "Formal Verification highlights the difficulty of specifications". Which wasn't a secret in the first place. But yeah, fewer bugs is better than more.
ncmncm 6y ago
Title is verifiably false. 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.
- sterlind 6y ago
  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.
  - ncmncm 6y ago
    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. This attitude is typical in formal specification.
    - sterlind 6y ago
      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?
zemnmez 6y ago
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.
- Klasiaster 6y ago
  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. For Rust there is https://crates.io/crates/session-types https://crates.io/crates/session-types from http://munksgaard.me/papers/laumann-munksgaard-larsen.pdf http://munksgaard.me/papers/laumann-munksgaard-larsen.pdf
  - zemnmez 6y ago
    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.
    - Jhsto 6y ago
      Are you aware of Pi-calculus and ProVerif? ProVerif sounds to address at least some of your requirements. Links: - https://en.wikipedia.org/wiki/%CE%A0-calculus https://en.wikipedia.org/wiki/%CE%A0-calculus - https://prosecco.gforge.inria.fr/personal/bblanche/proverif/ https://prosecco.gforge.inria.fr/personal/bblanche/proverif/
juskrey 6y ago
Formal verification only verifies assumptions made by verifier about the system.
cryptica 6y ago
>> 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?
cryptica 6y ago
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.
- docandrew 6y ago
  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_.
- tgflynn 6y ago
  > 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.
microtherion 6y ago
"Be careful about using the following code — I've only proven that it works, I haven't tested it." — Donald Knuth
namelosw 6y ago
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?
rurban 6y ago
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.

102 points by Alekhine 6y ago

dk8996 6y ago

I think this similar to what ADA is doing in crypto space.

exdsq 6y ago
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.
- MaxBarraclough 6y ago
  > I don’t understand what “hacker-proof code means” What's unclear about it?
  - serf 6y ago
    it's not that it's unclear per se, it's just an untenable position to take. lazy example : a hardware-level side-channel attack is not rendered impossible simply because the software was made with formal verification methods.
  - aspenmayer 6y ago
    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.
  - exdsq 6y ago
    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...
    - MaxBarraclough 6y ago
      > You can't verify the OS 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?

Exuma 6y ago

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.

dfee 6y ago
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)! Here was a lengthier diatribe of mine on a former Quanta article: https://news.ycombinator.com/item?id=22549988 https://news.ycombinator.com/item?id=22549988
- twic 6y ago
  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.
blihp 6y ago
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.
- AnimalMuppet 6y ago
  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.)
docandrew 6y ago
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 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 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/ 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.

saithound 6y ago

Needs (2016) in the title.

tptacek 6y ago

Formal methods are a powerful security tool because they produce useful code so slowly that they necessarily minimize attack surface.

exdsq 6y ago
It doesn’t have to be that slow! The tooling has advanced quite significantly over the last few years.
- MaxBarraclough 6y ago
  It's still fair to say that formal methods produces software far, far more slowly than ordinary methods. Look at how little functionality seL4 provides, compared to hobbyist operating systems.
  - lmm 6y ago
    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.
    - thanksforfish 6y ago
      If you don't use formal methods, how do you know when your work is done?
      - im3w1l 6y ago
        When the checks clear.
        ternaryoperator 6y ago
        One of the finest puns I've seen on HN ever!
      - 6y ago

MaxBarraclough 6y ago

> 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. https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597724/ https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597724/ https://www.newscientist.com/article/mg22730392-600-unhackable-kernel-could-keep-all-computers-safe-from-cyberattack-2/ https://www.newscientist.com/article/mg22730392-600-unhackab... https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...

jzer0cool 6y ago

> "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"?

computerphage 6y ago
> 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.
- jzer0cool 6y ago
  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.
- jzer0cool 6y ago
  > 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.
  - computerphage 6y ago
    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?

empath75 6y ago

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.

not2b 6y ago
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.
aliceryhl 6y ago
You might not ever reach 100% confidence, but formally verified code is a whole lot more likely to be correct than code that is not formally verified.

sesutton 6y ago

Doesn't the KRACK vulnerability undermine the idea that formally verified equals perfectly secure?

jhanschoo 6y ago
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.

deleted 6y ago

[deleted]

m3kw9 6y ago

And since that time what have they secured?

Animats 6y ago

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.

miscPerson 6y ago
Would you mind elaborating just a little? This sounds like an interesting idea.
docandrew 6y ago
Here's a formally-verified DNS Server: https://ironsides.martincarlisle.com/ https://ironsides.martincarlisle.com/ Not all the way down to the instruction level, but it's a start.

est31 6y ago

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. https://galois.com/blog/2017/10/formal-methods-krack-vulnerability/ 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.

rrmm 6y ago
Yeah the subtitle can be, "Formal Verification highlights the difficulty of specifications". Which wasn't a secret in the first place. But yeah, fewer bugs is better than more.

ncmncm 6y ago

Title is verifiably false. 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.

sterlind 6y ago
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.
- ncmncm 6y ago
  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. This attitude is typical in formal specification.
  - sterlind 6y ago
    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?

zemnmez 6y ago

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.

Klasiaster 6y ago
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. For Rust there is https://crates.io/crates/session-types https://crates.io/crates/session-types from http://munksgaard.me/papers/laumann-munksgaard-larsen.pdf http://munksgaard.me/papers/laumann-munksgaard-larsen.pdf
- zemnmez 6y ago
  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.
  - Jhsto 6y ago
    Are you aware of Pi-calculus and ProVerif? ProVerif sounds to address at least some of your requirements. Links: - https://en.wikipedia.org/wiki/%CE%A0-calculus https://en.wikipedia.org/wiki/%CE%A0-calculus - https://prosecco.gforge.inria.fr/personal/bblanche/proverif/ https://prosecco.gforge.inria.fr/personal/bblanche/proverif/

juskrey 6y ago

Formal verification only verifies assumptions made by verifier about the system.

cryptica 6y ago

>> 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?

cryptica 6y ago

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.

docandrew 6y ago
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_.
tgflynn 6y ago
> 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.

microtherion 6y ago

"Be careful about using the following code — I've only proven that it works, I haven't tested it." — Donald Knuth

namelosw 6y ago

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?

rurban 6y ago

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.