5 ms·

This is a gap in this kind of verification work. Systems like coq get around this by having a facility to "extract" code from the proof itself. You would define

by munin 9y ago

This is a gap in this kind of verification work. Systems like coq get around this by having a facility to "extract" code from the proof itself. You would define your algorithm as a Fixpoint, prove properties of that Fixpoint, then extract that Fixpoint into some ocaml code and use it directly in your real programs. This closes the loop you describe, insamuch as you trust the extraction process and the ocaml compiler and runtime (but other work is ongoing to close that loop as well).

chrisseaton 9y ago
The loop is always open though. Who verifies your verification code? Who verifies the processor implementation? All you can do is reduce the gap in the loop surely?
- nickpsecurity 9y ago
  It's been done down to the hardware. Originally by Computational Logic Inc for FM9001 whose prover became ACL2. Then Verisoft went from apps to OS to C subset to VAMP processor (DLX-style). Recently people are doing HOL to hardware that will integrate with HOL/Light whose core is a few hundred or thousand lines to trust. Those people eliminated trust requirements in everything from extraction mechanisms to provers to assembly generation: http://www.cse.chalmers.se/~myreen/ http://www.cse.chalmers.se/~myreen/ Follow he and his colleagues work for all that. Especially Milawa and CakeML. If you want a starting point, a small, Forth-like processor verifiable by hand on a node verifiable by eye could run the initial interpreter and prover for the first, real CPU. Plus, common practice is to split work into untrusted generation of artifacts with traces that are verified by a trusted checker that's comparatively tiny and simple. The little CPU would just run the checkers. You can run the generation on anything you like with the speed benefit. :)
  - unboxed_type 9y ago
    What about real CPUs (much more complex than 'Forth CPU'), network adapters (has its own CPU), memory controllers, real OS kernels, POSIX library (which is sometimes loosely specified) and so on? As far as I understand modern truly reliable system (commerical avionics-like) still must be relatively simple to be verified up to hardware level.
    - nickpsecurity 9y ago
      Real CPU's are formally verified for certain properties with rigorous tests. That's why they have only 100-300 errors in something with a billion transistors. That practice started after a recall. Now, for examples of full, mathematical verification of about every aspect you're looking at VAMP and AAMP7G. http://www.spbguga.ru/files/Formal_Verification_of_a_Processor.pdf http://www.spbguga.ru/files/Formal_Verification_of_a_Process... http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf VAMP is a pretty-complex, DLX-style CPU. I think they extended it to multicore or concurrency of some kind in another work. Original was single core, though. Passed all the FPGA tests. The AAMP7G combines a stack machine, over a hundred instructions, microcode engine, and separation kernel into one CPU. It was first in recent times in high-assurance security to use microcoding. I tell everyone to do that since it lets us easily change the behavior of the hardware without reverifying everything. Their tools also let you verify software semi-automatically against a model of the hardware ISA. Main stuff is paywalled but this is best free one I could get you. On availability side, they also run three units at once with a voter to reduce the odds the chip will fail. Truly high-assurance exemplar in availability and security. The prover is ACL2. You can do a trusted checker for that in few lines of code. You might need a lot of RAM and CPU time, though. Even all that can be a few blocks verified by eye and hand that you just plaster over a bunch of silicon then verify correctness automatically. There's also techniques where a partial failure can be magnified into total, visible failure. Tandem/HP NonStop does stuff like that to catch and replace failed components before system downtime happens. So, you can be reasonably sure the components are working even if defects happen during fabrication.
- deleted 9y ago
  [deleted]
- munin 9y ago
  You can close all of those. You can have large amounts of your verifier itself be verified. You can verify the CPU design (hardware people tell me this used to be standard, and a lot of the formal methods community has roots in verifying hardware). What you can't close is the language that you use to do all the verification in, itself. You wind up with a core calculus that you have to stare at really hard and trust / prove via other means.
  - DanWaterworth 9y ago
    You always have to make assumptions in any formal system able to express arithmetic as proved by Gödel.
  - roblabla 9y ago
    Isn't this susceptible to a trusting trust[0] attack, where your verifier has a bug that makes it verify itself, even though it shouldn't ? It's always possible there is a loop somewhere. The best you can hope for is make it infinitesimally small. [0]: http://wiki.c2.com/?TheKenThompsonHack http://wiki.c2.com/?TheKenThompsonHack
    - mcguire 9y ago
      A trusting trust attack cannot be eliminated, only be made prohibitively expensive. One way to do that is by using multiple verifier back-ends.
    - seagreen 9y ago
      There's been a simple counter to trusting trust attacks since 2009: https://www.dwheeler.com/trusting-trust/ https://www.dwheeler.com/trusting-trust/
      - nonsince 9y ago
        If I understand the abstract correctly, that relies on having a trusted compiler, which assumably would have to be bootstrapped ultimately from a trusted hand-written compiler in machine code. This effectively counters malicious trusting trust attacks but does not effectively counter trusting trust attacks due to error, because your entire trusted stack has to be correct. That's not to say there's no way to close the loop here, simply that I don't know that this is it.
- samth 9y ago
  Right, the concept of the TCB (trusted computing base) is the important thing. Good discussions of remaining TCB in verified code are in the seL4 work, or in this paper: https://www.cs.princeton.edu/~appel/papers/verif-sha-2.pdf https://www.cs.princeton.edu/~appel/papers/verif-sha-2.pdf
  - nickpsecurity 9y ago
    See my link to Myreen's page and follow all those people's publications. Much of the TCB functions in papers like that has been eliminated in other work. It just needs to be cross-checked, integrated, and applied.
    - samth 9y ago
      Right, that's one of the nice things about Appel's paper: he shows how to integrate a few different pieces to significantly reduce the TCB (ie, it doesn't include anything about C the language at all).
      - nickpsecurity 9y ago
        I think the one you're talking about got the TCB down to a few hundred lines of C. Done in Twelf.
        samth 9y ago
        No, I'm talking about the one I linked to, which is done in Coq.
        nickpsecurity 9y ago
        Oh my bad. I just saw work such as seL4 then assumed it was a seL4 reference. I actually didn't have this one by Appel. Thanks for the paper! :) Here's the one I was referencing with the tiny TCB: https://www.cs.princeton.edu/~appel/papers/flit.pdf https://www.cs.princeton.edu/~appel/papers/flit.pdf OK. So, it was a few Kloc. Still smaller than Coq. They could probably get it even smaller with recent work given translation validation knocks compilers out of TCB. So, in between 803-2668loc.
- joshuata 9y ago
  An interesting solution to this problem is verification witnesses[1]. A witness is a machine readable record of a verification task. Several different programs can read the witness and verify it independently. It is especially useful for counterexamples, where it can be a simple program trace to the error state. Given the input program and witness another can check whether the error state is reached. [1] https://www.sosy-lab.org/~dbeyer/verification-witnesses/ https://www.sosy-lab.org/~dbeyer/verification-witnesses/
dronemallone 9y ago
That "facility" is the Curry-Howard correspondence!
- mafribe 9y ago
  Not necessarily. Isabelle/HOL, an prover not based on CH but on the LCF-architecture, can also do program extraction, see e.g. Program extraction in Isabelle: https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides....
- samth 9y ago
  Extraction of terms written using Fixpoint isn't really the Curry-Howard correspondence. Instead, the correspondence is between (for example) proofs of correctness and terms in the Calculus of Constructions. [Fixpoint terms are also CIC programs, so there's a sense in which they're related, but it's not really about Curry-Howard.]
pron 9y ago
It's not "getting around", and one could write an extraction tool like that for TLA+, too. The difficulty is simply verifying any system, by whatever method, end-to-end, namely verifying that the high-level global correctness properties are preserved all the way down to machine code. We simply have no idea how to do it for real-world, large software, and in those cases it's been done for small, simple software (seL4, CompCert), the process was extremely expensive.
nonsince 9y ago
If the OCaml code is Standard ML-compliant you could run it on Cake, then you only have to trust the conversion

by munin 9y ago

chrisseaton 9y ago

The loop is always open though. Who verifies your verification code? Who verifies the processor implementation? All you can do is reduce the gap in the loop surely?

nickpsecurity 9y ago
It's been done down to the hardware. Originally by Computational Logic Inc for FM9001 whose prover became ACL2. Then Verisoft went from apps to OS to C subset to VAMP processor (DLX-style). Recently people are doing HOL to hardware that will integrate with HOL/Light whose core is a few hundred or thousand lines to trust. Those people eliminated trust requirements in everything from extraction mechanisms to provers to assembly generation: http://www.cse.chalmers.se/~myreen/ http://www.cse.chalmers.se/~myreen/ Follow he and his colleagues work for all that. Especially Milawa and CakeML. If you want a starting point, a small, Forth-like processor verifiable by hand on a node verifiable by eye could run the initial interpreter and prover for the first, real CPU. Plus, common practice is to split work into untrusted generation of artifacts with traces that are verified by a trusted checker that's comparatively tiny and simple. The little CPU would just run the checkers. You can run the generation on anything you like with the speed benefit. :)
- unboxed_type 9y ago
  What about real CPUs (much more complex than 'Forth CPU'), network adapters (has its own CPU), memory controllers, real OS kernels, POSIX library (which is sometimes loosely specified) and so on? As far as I understand modern truly reliable system (commerical avionics-like) still must be relatively simple to be verified up to hardware level.
  - nickpsecurity 9y ago
    Real CPU's are formally verified for certain properties with rigorous tests. That's why they have only 100-300 errors in something with a billion transistors. That practice started after a recall. Now, for examples of full, mathematical verification of about every aspect you're looking at VAMP and AAMP7G. http://www.spbguga.ru/files/Formal_Verification_of_a_Processor.pdf http://www.spbguga.ru/files/Formal_Verification_of_a_Process... http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf VAMP is a pretty-complex, DLX-style CPU. I think they extended it to multicore or concurrency of some kind in another work. Original was single core, though. Passed all the FPGA tests. The AAMP7G combines a stack machine, over a hundred instructions, microcode engine, and separation kernel into one CPU. It was first in recent times in high-assurance security to use microcoding. I tell everyone to do that since it lets us easily change the behavior of the hardware without reverifying everything. Their tools also let you verify software semi-automatically against a model of the hardware ISA. Main stuff is paywalled but this is best free one I could get you. On availability side, they also run three units at once with a voter to reduce the odds the chip will fail. Truly high-assurance exemplar in availability and security. The prover is ACL2. You can do a trusted checker for that in few lines of code. You might need a lot of RAM and CPU time, though. Even all that can be a few blocks verified by eye and hand that you just plaster over a bunch of silicon then verify correctness automatically. There's also techniques where a partial failure can be magnified into total, visible failure. Tandem/HP NonStop does stuff like that to catch and replace failed components before system downtime happens. So, you can be reasonably sure the components are working even if defects happen during fabrication.
deleted 9y ago
[deleted]
munin 9y ago
You can close all of those. You can have large amounts of your verifier itself be verified. You can verify the CPU design (hardware people tell me this used to be standard, and a lot of the formal methods community has roots in verifying hardware). What you can't close is the language that you use to do all the verification in, itself. You wind up with a core calculus that you have to stare at really hard and trust / prove via other means.
- DanWaterworth 9y ago
  You always have to make assumptions in any formal system able to express arithmetic as proved by Gödel.
- roblabla 9y ago
  Isn't this susceptible to a trusting trust[0] attack, where your verifier has a bug that makes it verify itself, even though it shouldn't ? It's always possible there is a loop somewhere. The best you can hope for is make it infinitesimally small. [0]: http://wiki.c2.com/?TheKenThompsonHack http://wiki.c2.com/?TheKenThompsonHack
  - mcguire 9y ago
    A trusting trust attack cannot be eliminated, only be made prohibitively expensive. One way to do that is by using multiple verifier back-ends.
  - seagreen 9y ago
    There's been a simple counter to trusting trust attacks since 2009: https://www.dwheeler.com/trusting-trust/ https://www.dwheeler.com/trusting-trust/
    - nonsince 9y ago
      If I understand the abstract correctly, that relies on having a trusted compiler, which assumably would have to be bootstrapped ultimately from a trusted hand-written compiler in machine code. This effectively counters malicious trusting trust attacks but does not effectively counter trusting trust attacks due to error, because your entire trusted stack has to be correct. That's not to say there's no way to close the loop here, simply that I don't know that this is it.
samth 9y ago
Right, the concept of the TCB (trusted computing base) is the important thing. Good discussions of remaining TCB in verified code are in the seL4 work, or in this paper: https://www.cs.princeton.edu/~appel/papers/verif-sha-2.pdf https://www.cs.princeton.edu/~appel/papers/verif-sha-2.pdf
- nickpsecurity 9y ago
  See my link to Myreen's page and follow all those people's publications. Much of the TCB functions in papers like that has been eliminated in other work. It just needs to be cross-checked, integrated, and applied.
  - samth 9y ago
    Right, that's one of the nice things about Appel's paper: he shows how to integrate a few different pieces to significantly reduce the TCB (ie, it doesn't include anything about C the language at all).
    - nickpsecurity 9y ago
      I think the one you're talking about got the TCB down to a few hundred lines of C. Done in Twelf.
      - samth 9y ago
        No, I'm talking about the one I linked to, which is done in Coq.
        nickpsecurity 9y ago
        Oh my bad. I just saw work such as seL4 then assumed it was a seL4 reference. I actually didn't have this one by Appel. Thanks for the paper! :) Here's the one I was referencing with the tiny TCB: https://www.cs.princeton.edu/~appel/papers/flit.pdf https://www.cs.princeton.edu/~appel/papers/flit.pdf OK. So, it was a few Kloc. Still smaller than Coq. They could probably get it even smaller with recent work given translation validation knocks compilers out of TCB. So, in between 803-2668loc.
joshuata 9y ago
An interesting solution to this problem is verification witnesses[1]. A witness is a machine readable record of a verification task. Several different programs can read the witness and verify it independently. It is especially useful for counterexamples, where it can be a simple program trace to the error state. Given the input program and witness another can check whether the error state is reached. [1] https://www.sosy-lab.org/~dbeyer/verification-witnesses/ https://www.sosy-lab.org/~dbeyer/verification-witnesses/

dronemallone 9y ago

That "facility" is the Curry-Howard correspondence!

mafribe 9y ago
Not necessarily. Isabelle/HOL, an prover not based on CH but on the LCF-architecture, can also do program extraction, see e.g. Program extraction in Isabelle: https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides....
samth 9y ago
Extraction of terms written using Fixpoint isn't really the Curry-Howard correspondence. Instead, the correspondence is between (for example) proofs of correctness and terms in the Calculus of Constructions. [Fixpoint terms are also CIC programs, so there's a sense in which they're related, but it's not really about Curry-Howard.]

pron 9y ago

It's not "getting around", and one could write an extraction tool like that for TLA+, too. The difficulty is simply verifying any system, by whatever method, end-to-end, namely verifying that the high-level global correctness properties are preserved all the way down to machine code. We simply have no idea how to do it for real-world, large software, and in those cases it's been done for small, simple software (seL4, CompCert), the process was extremely expensive.

nonsince 9y ago

If the OCaml code is Standard ML-compliant you could run it on Cake, then you only have to trust the conversion