3 ms·

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 c

by Exuma 7y 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 7y 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 7y 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 7y 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 7y 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 7y 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.
- Exuma 7y ago
  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.
  - docandrew 7y ago
    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 https://www.youtube.com/watch?v=DZSSyWlsb28
nlewycky 7y ago
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 https://news.ycombinator.com/item?id=22801607 The main problem I have with Coq is its lack of automation. If I understand the history, that's a bit of an ironic statement because Coq's main feature was its automation. The statements to "rewrite based on this theorem" or "split on 'and' and form two goals" are tactics, and Coq allows you to write your own tactics. There's no need for tactics to be proven correct, they can be full of bugs, either they show a path to produce a value with the right type in which case you have a proof, or they do not. My problem is that the Coq developers seem to share an opinion that the user is a mathematician who has considered the problem, developed a proof, attempted to formalize the proof on their own paper, and is as a last step entering their formalized proof into Coq. As a non-mathematician, I have done none of those things. I understand that they avoid doing things that may consume CPU time like trying every combination for a variable, but the "auto" tactic won't try 'true' and 'false' for a single boolean variable. The one last step is that you can "extract" running code from Coq proofs. I've never done this myself, so I can't speak to it, but the idea is that you want to remove the concern that the code you've proven isn't the code you actually run. Coq can emit OCaml or Haskell.

by Exuma 7y ago

dfee 7y 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 7y 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 7y 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 7y 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 7y 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.

Exuma 7y ago
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.
- docandrew 7y ago
  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 https://www.youtube.com/watch?v=DZSSyWlsb28

nlewycky 7y ago

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 https://news.ycombinator.com/item?id=22801607 The main problem I have with Coq is its lack of automation. If I understand the history, that's a bit of an ironic statement because Coq's main feature was its automation. The statements to "rewrite based on this theorem" or "split on 'and' and form two goals" are tactics, and Coq allows you to write your own tactics. There's no need for tactics to be proven correct, they can be full of bugs, either they show a path to produce a value with the right type in which case you have a proof, or they do not. My problem is that the Coq developers seem to share an opinion that the user is a mathematician who has considered the problem, developed a proof, attempted to formalize the proof on their own paper, and is as a last step entering their formalized proof into Coq. As a non-mathematician, I have done none of those things. I understand that they avoid doing things that may consume CPU time like trying every combination for a variable, but the "auto" tactic won't try 'true' and 'false' for a single boolean variable. The one last step is that you can "extract" running code from Coq proofs. I've never done this myself, so I can't speak to it, but the idea is that you want to remove the concern that the code you've proven isn't the code you actually run. Coq can emit OCaml or Haskell.