8 ms·

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 p

by 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
- nickpsecurity 10y ago
  Which is great given they're precise statements about what you want to do that are easier for humans and computers to analyze. They don't have the language-level problems either. Tools can then turn those into code or do much of the work from there.
- jfoutz 10y ago
  If your spec is wrong, your code will be wrong anyway. More often, people use the code as the spec which is IMHO (for this kind of programing) really bad.
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.

by ahelwer 10y ago

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
nickpsecurity 10y ago
Which is great given they're precise statements about what you want to do that are easier for humans and computers to analyze. They don't have the language-level problems either. Tools can then turn those into code or do much of the work from there.
jfoutz 10y ago
If your spec is wrong, your code will be wrong anyway. More often, people use the code as the spec which is IMHO (for this kind of programing) really bad.

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.