15 ms·

Formal Verification Creates Hacker-Proof Code

69 points by azuajef 10y ago

no_protocol 10y ago
[Audio] Edit: Link was originally a podcast that auto-played. Has since been updated to a written content link.
StyloBill 10y ago
Here is the readable version. https://www.quantamagazine.org/20160920-formal-verification-creates-hacker-proof-code/ https://www.quantamagazine.org/20160920-formal-verification-...
- sctb 10y ago
  Thank you, we've updated the link from https://www.quantamagazine.org/?powerpress_pinw=29937-podcast&utm_source=Quanta+Magazine&utm_campaign=2f0887e749-Quanta_Newsletter_Feb_27_2015&utm_medium=email&utm_term=0_f0cb61321c-2f0887e749-389523389 https://www.quantamagazine.org/?powerpress_pinw=29937-podcas...
rhinoceraptor 10y ago
Code can still be exploited through vulnerable hardware, though.
ahelwer 10y ago
Worth noting formally verified programs are unhackable to the extent three things hold true: 1) Your model of the world corresponds to the world in which the program runs - for example, hardware is usually assumed to be bug-free. 2) The properties you've proven the program to hold are sufficient to stop the hacker from accomplishing their goals. 3) No bugs exist in your theorem prover.
- JackFr 10y ago
  Exactly. Even assuming (3) is true you've just pushed the problem down to your spec.
  - zzzcpan 10y ago
    Think of it as a double checking your code. If you had a bug per 100 LOCs you can reduce that to a bug per 1000-10000 LOCs. Which is achievable with other methods too, without the burden of formal verification.
    - philipkglass 10y ago
      Are the other methods for reducing errors to one bug per 10000 LOCs measured to be less burdensome? I've read with interest about how Jet Propulsion Laboratory produces code with low defect rates for spacecraft (without formal verification), but it appears to be a pretty drastic departure from ordinary commercial practice too.
      - nickpsecurity 10y ago
        I know of at least three: Hamilton's 001 Tool Suite http://htius.com/ http://htius.com/ Cleanroom Software Methodology http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html Praxis Correct-by-Construction http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf All three have some upfront time in specification with Praxis doing refinements, too. However, they all knock out tons of debugging and integration problems since errors don't slip in at all. Altran/Praxis charges 50% premium on top of normal contract so the extra labor is probably less than 50% given they're profitable. Cleanroom anecdotes showed the reduced debugging and maintenance issues meant it actually barely cost anything extra in time or money. A few outliers had it saving time. There's also a number of people and companies that are encoding business logic into specs that they implement with logic programming languages. This eliminates mismatch between business requirements and code with quite a bit of productivity and safety advantages if it works in one's use-case. I haven't evaluated their effectiveness but here's two: http://www.missioncriticalit.com/technology.html http://www.missioncriticalit.com/technology.html https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf
- hinkley 10y ago
  > 3) No bugs exist in your theorem prover Seems to me that at some point we want theorem provers to be self hosting, as it were. That of course won't fix problems with bugs in hardware, and hardware that behaves like analog devices (rowhammer, cold boot, data recovery, stray gamma rays...)
  - CGamesPlay 10y ago
    If there's a bug in the theorem prover and it proves itself, it still has that bug.
    - spott 10y ago
      Only if the bug in the prover allows the bug in the prover, which seems unlikely (unless the bug is pretty huge).
      - timjver 10y ago
        "seems unlikely" isn't really cutting it, when we're talking about formal systems.
      - mekaj 10y ago
        Trivial, small example: the bug is the prover accepts all inputs.
    - burke 10y ago
      Yep. Imagine a prover that accepts all statements. It would accept a buggy program, and it would accept itself. It would obviously help reduce errors but it wouldn't categorically eliminate them.
    - nabla9 10y ago
      It would have to be kind of fixed point of bugs (like finding cryptographic hash that equal to the input value). It wold be incredibly unlikely.
  - simondedalus 10y ago
- LoSboccacc 10y ago
  is the compiler for the language also formally verified? can't find this in the article, and well, it'd be a huge open door for bugs.
  - munin 10y ago
    frequently, yes, if it uses compcert or cakeML or something.
  - nickpsecurity 10y ago
    It's in the picture: http://deepspec.org/ http://deepspec.org/
    - LoSboccacc 10y ago
      thanks. very interesting project. they also have their own kernel and all
- deegles 10y ago
  > hardware is usually assumed to be bug-free I feel like exploits like Rowhammer really threw a wrench into this. Now one would also have to specify allowable interactions with the hardware?
  - thingexplainer 10y ago
    I think the solution is to formally verify your hardware with a prover that is aware of electromagnetic forces. Software has to assume correctness of hardware (rad-hard applications have to assume ridiculous hardware faults are possible, but that's to prevent solar flares from corrupting firmware, not Rowhammer). Thought experiment; you are some sort of intrusion prevention system. You've detected that your hardware is untrustworthy. Now what?
  - nickpsecurity 10y ago
    It's always been there. The messiness & limitations of analog were actually main the reasons for digital being invented in the first place. Then the digital stuff had issues but way easier to surmount with formal methods. Or just computationally like heuristic placement of parts. Each problem that was found could be dealt with using known algorithms or verification techniques. There's been many correct-by-construction methods to building stuff. So, we just apply that without the weird, over-complicated additions that happened largely for marketing reasons. The result is a highly-correct, reference implementation there for verification or checking the optimized ones. Now, the analog and RF portions are The Devil. These will be a (censored) to get correct with automated means. Already are with manual methods. There's been some progress in synthesizing and verifying them. Still mostly ad-hoc, manual work. Best bet is analog portions... much as one can use... happen with simple components on as old a process node as you can use. Less design rules, less weird physics, more reliability due to maturity of processes, and more synthesis results. Either whole thing is done on old nodes or we can pull a Tekmos doing old (eg 350nm) for analog with new (eg 90nm) for digital part with careful integration. EDIT: To address other commenter, put it behind EMSEC shielding to address that. The analog components can also be designed for fault-tolerance against things like cosmic rays or voting configuration used to correct errors.
- abecedarius 10y ago
  Technically, 3) No bugs in your proof checker. A bug-infested theorem prover can still be useful. As long as I'm well-actuallying, 2) The proven properties establish my own informal goals. If a hacker's goals are also satisfied, well, maybe they want to DDoS the internet but it's Not My Problem.
CiPHPerCoder 10y ago
Formal verification doesn't mean your design can't be flawed in other ways that your theorem prover can't identify. See also: Software AES with cache-timing information leaks.
- AnimalMuppet 10y ago
  See: Microsoft Outlook deciding that executable attachments were a good idea. The feature worked according to spec (I assume), but wow did that ever open the door to a whole lot of hacking...
  - CiPHPerCoder 10y ago
    See: https://github.com/w3c/svgwg/issues/266 https://github.com/w3c/svgwg/issues/266
    - nickpsecurity 10y ago
      Well-written report. I agree with the recommendation.
- nickpsecurity 10y ago
  It's true but that's a specification problem. The hardware should be in the model since it's in the TCB. The earliest tools used for high-assurance security, like Gypsy Verification Environment, had information-flow analysis for detecting covert channels. Today, we have information flow control, distributed version of it, and hardware versions of non-interference that go to the gates. We're actually past being able to handle that with current tooling if ultra-high-performance is a non-goal. https://www.usenix.org/system/files/conference/usenixsecurity13/sec13-paper_doychev.pdf https://www.usenix.org/system/files/conference/usenixsecurit... http://www-bcf.usc.edu/~wang626/pubDOC/EldibWS14_TOSEM.pdf http://www-bcf.usc.edu/~wang626/pubDOC/EldibWS14_TOSEM.pdf It's analog and RF side channels that's going to screw them. DOD et al did decades of cat and mouse games under that with their TEMPEST activities. Open research just getting started. Just waiting for The Flood. :)
- lmkg 10y ago
platz 10y ago
how would they anticipate timing attacks with this method?
- nickpsecurity 10y ago
  Lots of work in that area. Here's an example: http://www.cse.psu.edu/~dbz5017/pub/pltiming-pldi12.pdf http://www.cse.psu.edu/~dbz5017/pub/pltiming-pldi12.pdf
  - platz 10y ago
    Impressive!
jaibot 10y ago
"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth
- JadeNB 10y ago
  > "Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth "Beware of people slinging around the famous Knuth quote as if it invalidated progress in program proving." - Me (Not a reference to you personally, but I think that this quote is too often used to disparage all work on program provers, rather than as just—as I take it to be—pointing out that, no matter how good your prover is, you should still check your code.)
  - nickpsecurity 10y ago
    That and the Godel one above. For first point, they could link to a presentation on high-assurance systems showing one needs a combination of specs, proofs, testing, and human review for max assurance. For the second, the alternative is showing how the prover problem is greatly reduced by using simple, proof checkers and/or logics in the process that are easy to verify by hand.
- jonjacky 10y ago
  This "quote" is probably bogus. When I was at lunch with Knuth once (brag, brag), someone asked him where he said that. Knuth said he couldn't recall saying it and he doubted that he ever said it, because he would not attempt to prove code without also testing it. Then he said it might be a paraphrase (not a quote) from an analysis he made of an assembly language program where he did not have hardware with that instruction set available to him.
nixpulvis 10y ago
I wouldn't call anything unhackable.
- macawfish 10y ago
  Sometimes the best hack is to leave a unhackable program alone. And by unhackable I mean proprietary.
45h34jh53k4j 10y ago
pls warn podcast in title, i dislike podcasts
andybak 10y ago
Mods - please label this audio (and auto-playing)
nabla9 10y ago
No new breakthroughs in formal proofs or deriving programs, just incremental progress. The cost of formal methods stays high. The high cost means that it does not work well with iterative programming, or changes in specs. So far only some military and safety critical applications and parts of Intel's silicon have been worth of the cost. I took my first course in formal methods using the book Programming: The Derivation of Algorithms by A. Kaldewaij. It would be perfectly reasonable to implement something similar to Kaldewaij's guarded programming language today over some other programming language and use it to derive formally proven programs if someone really values the correctness. It would be also cool and fun but not for everyone.
- philipkglass 10y ago
  I hope that one of these days (years?) we might start seeing formally verified versions of code for dealing with standards that don't change rapidly and that have proved to be security problems in the past. I'm thinking of things like font rasterizers, TIFF readers, full PDF readers, and JavaScript engines intended for browsers.
  - nickpsecurity 10y ago
    The problem with many of these formats is they're Turing-Complete languages with input driving what they do. The input is also malicious. So, the solution so far is to isolate and mediate such things with verification going into the mechanisms for that. An example of one for exactly your types of programs is Microsoft's Xax: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/xax-osdi08.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... My preferred approach is the old-school method of highly-assured microkernels that just separate everything else from one another. Here's a browser OS based on that principle: https://www.usenix.org/legacy/event/osdi10/tech/full_papers/Tang.pdf https://www.usenix.org/legacy/event/osdi10/tech/full_papers/...
    - sliverstorm 10y ago
      Aren't microprocessors Turing-Complete machines that undergo formal verification?
shpat 10y ago
Worth noting that we've open sourced the toolset used to generate code for the Little Bird, available at http://ivorylang.org http://ivorylang.org
crypto5 10y ago
Curious if there is an opposite process: having some program, ask some prolog-like system if given program has any vulnerabilities, and how to exploit them?
- nickpsecurity 10y ago
  You're basically describing static analysis but with Prolog and a weaponize option. I haven't looked up bug-to-attack research in ages but last I did it was generating exploits from patches. That one was pretty evil if one is aware of why delaying patches often makes sense for mission-critical apps. They need testing as they can do damage themselves. So, instantly turning even a chunk of patches into exploits can give an attacker an advantage in that windows between release and application. Example: http://bitblaze.cs.berkeley.edu/papers/apeg.pdf http://bitblaze.cs.berkeley.edu/papers/apeg.pdf
sklivvz1971 10y ago
Side-channel attacks, attacks that depend on physical characteristics of the system, are a thing [0] and formal correctness doesn't really prevent them. Also there's crazy stuff like Row Hammer [1] which depends on escaping the abstraction that memory bytes are independent entities. While these are maybe crazy or extreme attacks, they are still practical in some cases. Any abstraction can eventually be hacked simply because an abstraction is a simplification of a more complex system which can be manipulated. Reminds me of the joke of the junior functional programmer convinced that their code is side effects free and who then proceeds to crash the garbage collector because memory allocation is not considered a side effect... [0]: https://en.wikipedia.org/wiki/Side-channel_attack https://en.wikipedia.org/wiki/Side-channel_attack [1]: https://en.wikipedia.org/wiki/Row_hammer https://en.wikipedia.org/wiki/Row_hammer
- nickpsecurity 10y ago
  I addressed this here: https://news.ycombinator.com/item?id=12762323 https://news.ycombinator.com/item?id=12762323 The military, EE's, and even RAM suppliers knew about those issues. There are products in high-security (esp Defense) that try to counter as many as they can afford to. The problem was the knowledge was ignored or intentionally not applied. The first just keeps happening in general in so-called INFOSEC. The second is a result of market incentives where the suppliers' goal is to hit specific performance, energy, area, cost, etc targets to maximize market share and profit. On cost, they also want to minimize that in general for the executives and shareholders to pocket more income. This really affects RAM vendors as people involved in QA have said on various forums that they're basically just pushed to get shit out the door as quickly as possible since competition is intense. That they do this with ever-increasing complexity in designs and physics in shrinking nodes means problems can only go up. So, it's not a new discovery in terms of hardware correctness or even an accident. These problems are intentionally there to increase profits. Compare that to the design of things like 1802, NonStop, AAMP7G, rad-hard ASIC's... all that trade off marketable criteria at higher prices to get higher reliability. They exist but almost nobody buys them. That's why such practices aren't and won't be status quo. EDIT to add NonStop link to show what earlier systems accomplished with careful hardware and software design. Similar, even more clever, techniques were used inside ASIC's as well. http://www.hpl.hp.com/techreports/tandem/TR-86.2.pdf http://www.hpl.hp.com/techreports/tandem/TR-86.2.pdf
contingencies 10y ago
This comment on the page is insightful: Anecdote – Erlang designer Armstrong does contract work for formal verification with high-assurance applications. A widget-maker for a large European car manufacturer wanted to ensure their widget was fully compliant with all of the specifications as issued by the overseeing administrative authority (ISO, ANSI, whatever). He and his team of engineers sat down and took 1k +/- .2k pages of written specifications, translated them into invariant properties, and let 'er rip. Of the ~foo bugs they found, ~40% of the bugs were internally inconsistent bugs within the specification. [An average car of model year 2016 has somewhere between 500-800 MCUs within them. Scary prospect…] So, lets say LDAP's RFC has 3 'bugs' in them (a proposition: p in section one, then a proposition: ~p in section 3). Microsoft wants to implement Active Directory to have LDAP compliance to work with Kerberos, Apple devices, etc etc. By definition, this implementation will be buggy. These bugs are of a class which have no fix! ... if you want to read some formal proofs from the software and mathematics worlds, see https://www.isa-afp.org/ https://www.isa-afp.org/
- iheartmemcache 10y ago
  Haha, that was my comment! Glad you liked it. Never thought it'd show up on HN. I normally don't comment on Quanta, but there were so many half-informed remarks propagating misinformation that I felt compelled to make not one, but two, comments in that thread (and formal verification isn't even my domain of expertise!)

69 points by azuajef 10y ago

[Audio] Edit: Link was originally a podcast that auto-played. Has since been updated to a written content link.

Here is the readable version. https://www.quantamagazine.org/20160920-formal-verification-creates-hacker-proof-code/ https://www.quantamagazine.org/20160920-formal-verification-...

sctb 10y ago
Thank you, we've updated the link from https://www.quantamagazine.org/?powerpress_pinw=29937-podcast&utm_source=Quanta+Magazine&utm_campaign=2f0887e749-Quanta_Newsletter_Feb_27_2015&utm_medium=email&utm_term=0_f0cb61321c-2f0887e749-389523389 https://www.quantamagazine.org/?powerpress_pinw=29937-podcas...

rhinoceraptor 10y ago

Code can still be exploited through vulnerable hardware, though.

ahelwer 10y ago

Worth noting formally verified programs are unhackable to the extent three things hold true: 1) Your model of the world corresponds to the world in which the program runs - for example, hardware is usually assumed to be bug-free. 2) The properties you've proven the program to hold are sufficient to stop the hacker from accomplishing their goals. 3) No bugs exist in your theorem prover.

JackFr 10y ago
Exactly. Even assuming (3) is true you've just pushed the problem down to your spec.
- zzzcpan 10y ago
  Think of it as a double checking your code. If you had a bug per 100 LOCs you can reduce that to a bug per 1000-10000 LOCs. Which is achievable with other methods too, without the burden of formal verification.
  - philipkglass 10y ago
    Are the other methods for reducing errors to one bug per 10000 LOCs measured to be less burdensome? I've read with interest about how Jet Propulsion Laboratory produces code with low defect rates for spacecraft (without formal verification), but it appears to be a pretty drastic departure from ordinary commercial practice too.
    - nickpsecurity 10y ago
      I know of at least three: Hamilton's 001 Tool Suite http://htius.com/ http://htius.com/ Cleanroom Software Methodology http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html Praxis Correct-by-Construction http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf All three have some upfront time in specification with Praxis doing refinements, too. However, they all knock out tons of debugging and integration problems since errors don't slip in at all. Altran/Praxis charges 50% premium on top of normal contract so the extra labor is probably less than 50% given they're profitable. Cleanroom anecdotes showed the reduced debugging and maintenance issues meant it actually barely cost anything extra in time or money. A few outliers had it saving time. There's also a number of people and companies that are encoding business logic into specs that they implement with logic programming languages. This eliminates mismatch between business requirements and code with quite a bit of productivity and safety advantages if it works in one's use-case. I haven't evaluated their effectiveness but here's two: http://www.missioncriticalit.com/technology.html http://www.missioncriticalit.com/technology.html https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf
hinkley 10y ago
> 3) No bugs exist in your theorem prover Seems to me that at some point we want theorem provers to be self hosting, as it were. That of course won't fix problems with bugs in hardware, and hardware that behaves like analog devices (rowhammer, cold boot, data recovery, stray gamma rays...)
- CGamesPlay 10y ago
  If there's a bug in the theorem prover and it proves itself, it still has that bug.
  - spott 10y ago
    Only if the bug in the prover allows the bug in the prover, which seems unlikely (unless the bug is pretty huge).
    - timjver 10y ago
      "seems unlikely" isn't really cutting it, when we're talking about formal systems.
    - mekaj 10y ago
      Trivial, small example: the bug is the prover accepts all inputs.
  - burke 10y ago
    Yep. Imagine a prover that accepts all statements. It would accept a buggy program, and it would accept itself. It would obviously help reduce errors but it wouldn't categorically eliminate them.
  - nabla9 10y ago
    It would have to be kind of fixed point of bugs (like finding cryptographic hash that equal to the input value). It wold be incredibly unlikely.
- simondedalus 10y ago
LoSboccacc 10y ago
is the compiler for the language also formally verified? can't find this in the article, and well, it'd be a huge open door for bugs.
- munin 10y ago
  frequently, yes, if it uses compcert or cakeML or something.
- nickpsecurity 10y ago
  It's in the picture: http://deepspec.org/ http://deepspec.org/
  - LoSboccacc 10y ago
    thanks. very interesting project. they also have their own kernel and all
deegles 10y ago
> hardware is usually assumed to be bug-free I feel like exploits like Rowhammer really threw a wrench into this. Now one would also have to specify allowable interactions with the hardware?
- thingexplainer 10y ago
  I think the solution is to formally verify your hardware with a prover that is aware of electromagnetic forces. Software has to assume correctness of hardware (rad-hard applications have to assume ridiculous hardware faults are possible, but that's to prevent solar flares from corrupting firmware, not Rowhammer). Thought experiment; you are some sort of intrusion prevention system. You've detected that your hardware is untrustworthy. Now what?
- nickpsecurity 10y ago
  It's always been there. The messiness & limitations of analog were actually main the reasons for digital being invented in the first place. Then the digital stuff had issues but way easier to surmount with formal methods. Or just computationally like heuristic placement of parts. Each problem that was found could be dealt with using known algorithms or verification techniques. There's been many correct-by-construction methods to building stuff. So, we just apply that without the weird, over-complicated additions that happened largely for marketing reasons. The result is a highly-correct, reference implementation there for verification or checking the optimized ones. Now, the analog and RF portions are The Devil. These will be a (censored) to get correct with automated means. Already are with manual methods. There's been some progress in synthesizing and verifying them. Still mostly ad-hoc, manual work. Best bet is analog portions... much as one can use... happen with simple components on as old a process node as you can use. Less design rules, less weird physics, more reliability due to maturity of processes, and more synthesis results. Either whole thing is done on old nodes or we can pull a Tekmos doing old (eg 350nm) for analog with new (eg 90nm) for digital part with careful integration. EDIT: To address other commenter, put it behind EMSEC shielding to address that. The analog components can also be designed for fault-tolerance against things like cosmic rays or voting configuration used to correct errors.
abecedarius 10y ago
Technically, 3) No bugs in your proof checker. A bug-infested theorem prover can still be useful. As long as I'm well-actuallying, 2) The proven properties establish my own informal goals. If a hacker's goals are also satisfied, well, maybe they want to DDoS the internet but it's Not My Problem.

CiPHPerCoder 10y ago

Formal verification doesn't mean your design can't be flawed in other ways that your theorem prover can't identify. See also: Software AES with cache-timing information leaks.

AnimalMuppet 10y ago
See: Microsoft Outlook deciding that executable attachments were a good idea. The feature worked according to spec (I assume), but wow did that ever open the door to a whole lot of hacking...
- CiPHPerCoder 10y ago
  See: https://github.com/w3c/svgwg/issues/266 https://github.com/w3c/svgwg/issues/266
  - nickpsecurity 10y ago
    Well-written report. I agree with the recommendation.
nickpsecurity 10y ago
It's true but that's a specification problem. The hardware should be in the model since it's in the TCB. The earliest tools used for high-assurance security, like Gypsy Verification Environment, had information-flow analysis for detecting covert channels. Today, we have information flow control, distributed version of it, and hardware versions of non-interference that go to the gates. We're actually past being able to handle that with current tooling if ultra-high-performance is a non-goal. https://www.usenix.org/system/files/conference/usenixsecurity13/sec13-paper_doychev.pdf https://www.usenix.org/system/files/conference/usenixsecurit... http://www-bcf.usc.edu/~wang626/pubDOC/EldibWS14_TOSEM.pdf http://www-bcf.usc.edu/~wang626/pubDOC/EldibWS14_TOSEM.pdf It's analog and RF side channels that's going to screw them. DOD et al did decades of cat and mouse games under that with their TEMPEST activities. Open research just getting started. Just waiting for The Flood. :)
lmkg 10y ago

platz 10y ago

how would they anticipate timing attacks with this method?

nickpsecurity 10y ago
Lots of work in that area. Here's an example: http://www.cse.psu.edu/~dbz5017/pub/pltiming-pldi12.pdf http://www.cse.psu.edu/~dbz5017/pub/pltiming-pldi12.pdf
- platz 10y ago
  Impressive!

jaibot 10y ago

"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth

JadeNB 10y ago
> "Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth "Beware of people slinging around the famous Knuth quote as if it invalidated progress in program proving." - Me (Not a reference to you personally, but I think that this quote is too often used to disparage all work on program provers, rather than as just—as I take it to be—pointing out that, no matter how good your prover is, you should still check your code.)
- nickpsecurity 10y ago
  That and the Godel one above. For first point, they could link to a presentation on high-assurance systems showing one needs a combination of specs, proofs, testing, and human review for max assurance. For the second, the alternative is showing how the prover problem is greatly reduced by using simple, proof checkers and/or logics in the process that are easy to verify by hand.
jonjacky 10y ago
This "quote" is probably bogus. When I was at lunch with Knuth once (brag, brag), someone asked him where he said that. Knuth said he couldn't recall saying it and he doubted that he ever said it, because he would not attempt to prove code without also testing it. Then he said it might be a paraphrase (not a quote) from an analysis he made of an assembly language program where he did not have hardware with that instruction set available to him.

nixpulvis 10y ago

I wouldn't call anything unhackable.

macawfish 10y ago
Sometimes the best hack is to leave a unhackable program alone. And by unhackable I mean proprietary.

45h34jh53k4j 10y ago

pls warn podcast in title, i dislike podcasts

andybak 10y ago

Mods - please label this audio (and auto-playing)

nabla9 10y ago

No new breakthroughs in formal proofs or deriving programs, just incremental progress. The cost of formal methods stays high. The high cost means that it does not work well with iterative programming, or changes in specs. So far only some military and safety critical applications and parts of Intel's silicon have been worth of the cost. I took my first course in formal methods using the book Programming: The Derivation of Algorithms by A. Kaldewaij. It would be perfectly reasonable to implement something similar to Kaldewaij's guarded programming language today over some other programming language and use it to derive formally proven programs if someone really values the correctness. It would be also cool and fun but not for everyone.

philipkglass 10y ago
I hope that one of these days (years?) we might start seeing formally verified versions of code for dealing with standards that don't change rapidly and that have proved to be security problems in the past. I'm thinking of things like font rasterizers, TIFF readers, full PDF readers, and JavaScript engines intended for browsers.
- nickpsecurity 10y ago
  The problem with many of these formats is they're Turing-Complete languages with input driving what they do. The input is also malicious. So, the solution so far is to isolate and mediate such things with verification going into the mechanisms for that. An example of one for exactly your types of programs is Microsoft's Xax: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/xax-osdi08.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... My preferred approach is the old-school method of highly-assured microkernels that just separate everything else from one another. Here's a browser OS based on that principle: https://www.usenix.org/legacy/event/osdi10/tech/full_papers/Tang.pdf https://www.usenix.org/legacy/event/osdi10/tech/full_papers/...
  - sliverstorm 10y ago
    Aren't microprocessors Turing-Complete machines that undergo formal verification?

shpat 10y ago

Worth noting that we've open sourced the toolset used to generate code for the Little Bird, available at http://ivorylang.org http://ivorylang.org

crypto5 10y ago

Curious if there is an opposite process: having some program, ask some prolog-like system if given program has any vulnerabilities, and how to exploit them?

nickpsecurity 10y ago
You're basically describing static analysis but with Prolog and a weaponize option. I haven't looked up bug-to-attack research in ages but last I did it was generating exploits from patches. That one was pretty evil if one is aware of why delaying patches often makes sense for mission-critical apps. They need testing as they can do damage themselves. So, instantly turning even a chunk of patches into exploits can give an attacker an advantage in that windows between release and application. Example: http://bitblaze.cs.berkeley.edu/papers/apeg.pdf http://bitblaze.cs.berkeley.edu/papers/apeg.pdf

sklivvz1971 10y ago

Side-channel attacks, attacks that depend on physical characteristics of the system, are a thing [0] and formal correctness doesn't really prevent them. Also there's crazy stuff like Row Hammer [1] which depends on escaping the abstraction that memory bytes are independent entities. While these are maybe crazy or extreme attacks, they are still practical in some cases. Any abstraction can eventually be hacked simply because an abstraction is a simplification of a more complex system which can be manipulated. Reminds me of the joke of the junior functional programmer convinced that their code is side effects free and who then proceeds to crash the garbage collector because memory allocation is not considered a side effect... [0]: https://en.wikipedia.org/wiki/Side-channel_attack https://en.wikipedia.org/wiki/Side-channel_attack [1]: https://en.wikipedia.org/wiki/Row_hammer https://en.wikipedia.org/wiki/Row_hammer

nickpsecurity 10y ago
I addressed this here: https://news.ycombinator.com/item?id=12762323 https://news.ycombinator.com/item?id=12762323 The military, EE's, and even RAM suppliers knew about those issues. There are products in high-security (esp Defense) that try to counter as many as they can afford to. The problem was the knowledge was ignored or intentionally not applied. The first just keeps happening in general in so-called INFOSEC. The second is a result of market incentives where the suppliers' goal is to hit specific performance, energy, area, cost, etc targets to maximize market share and profit. On cost, they also want to minimize that in general for the executives and shareholders to pocket more income. This really affects RAM vendors as people involved in QA have said on various forums that they're basically just pushed to get shit out the door as quickly as possible since competition is intense. That they do this with ever-increasing complexity in designs and physics in shrinking nodes means problems can only go up. So, it's not a new discovery in terms of hardware correctness or even an accident. These problems are intentionally there to increase profits. Compare that to the design of things like 1802, NonStop, AAMP7G, rad-hard ASIC's... all that trade off marketable criteria at higher prices to get higher reliability. They exist but almost nobody buys them. That's why such practices aren't and won't be status quo. EDIT to add NonStop link to show what earlier systems accomplished with careful hardware and software design. Similar, even more clever, techniques were used inside ASIC's as well. http://www.hpl.hp.com/techreports/tandem/TR-86.2.pdf http://www.hpl.hp.com/techreports/tandem/TR-86.2.pdf

contingencies 10y ago

This comment on the page is insightful: Anecdote – Erlang designer Armstrong does contract work for formal verification with high-assurance applications. A widget-maker for a large European car manufacturer wanted to ensure their widget was fully compliant with all of the specifications as issued by the overseeing administrative authority (ISO, ANSI, whatever). He and his team of engineers sat down and took 1k +/- .2k pages of written specifications, translated them into invariant properties, and let 'er rip. Of the ~foo bugs they found, ~40% of the bugs were internally inconsistent bugs within the specification. [An average car of model year 2016 has somewhere between 500-800 MCUs within them. Scary prospect…] So, lets say LDAP's RFC has 3 'bugs' in them (a proposition: p in section one, then a proposition: ~p in section 3). Microsoft wants to implement Active Directory to have LDAP compliance to work with Kerberos, Apple devices, etc etc. By definition, this implementation will be buggy. These bugs are of a class which have no fix! ... if you want to read some formal proofs from the software and mathematics worlds, see https://www.isa-afp.org/ https://www.isa-afp.org/

iheartmemcache 10y ago
Haha, that was my comment! Glad you liked it. Never thought it'd show up on HN. I normally don't comment on Quanta, but there were so many half-informed remarks propagating misinformation that I felt compelled to make not one, but two, comments in that thread (and formal verification isn't even my domain of expertise!)