8 ms·

Lets say you model-checked some distributed algorithm with TLA+. You then implement it in Rust. How are you going to check that your implementation implements e

Lets say you model-checked some distributed algorithm with TLA+. You then implement it in Rust. How are you going to check that your implementation implements exactly the algorithm you have checked and not some other algorithm which looks very similar? I think the phrase 'reliable systems' is more appropriate to what you are up to, as opposed to the phrase 'correct systems' which usually corresponds to formal verification.

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
nickpsecurity 9y ago
That's why you implement it in Ada 2012 w/ SPARK 2014. You can encode the verification conditions as contracts. All the basic ones should be proven automatically. Those that aren't can be turned into runtime checks. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) http://www.electronicdesign.com/industrial/rust-and-spark-software-reliability-everyone http://www.electronicdesign.com/industrial/rust-and-spark-so... Here's an example of combining Event-B with SPARK to split overall verification between tools with each handling what they're good at: https://pdfs.semanticscholar.org/481c/d4d2409115429f4b824f370eb08fa338d67a.pdf https://pdfs.semanticscholar.org/481c/d4d2409115429f4b824f37...
- unboxed_type 9y ago
  How well Ada/SPARK suits distributed control algorithms I wonder? As far as I understand contracts are good enough for sequential code, but not well suited for parallel/distributed computation? Runtime checks are good as to prevent something from happening, but they are not able to guarantee the absence of an error in the first place, right?
  - oconnore 9y ago
    Huh? The whole point of distributed algorithms is that a set of local algorithms create a global behavior. I received this message so I send that message, etc. The SPARK contracts you write would check that local behavior, and the TLA+ would check that that local behavior results in some global behavior.
    - unboxed_type 9y ago
      Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.
pron 9y ago
In principle, you could translate your code -- or even the generated machine code -- back to TLA+ and check it there. This has been done as research projects for C[1] and Java bytecode[2]. But the reality of formal verification is that we simply do not yet have the capability -- with any tool -- to formally specify and verify a large, complex software system end-to-end (namely, from high-level global correctness properties and all the way down to machine code). There are two options: either use tools that can do end-to-end verification like Coq and Isabelle and limit yourself to small software, and even then expend an inordinate amount of effort (like seL4 or CompCert, small programs that have been verified end-to-end, taking years), or use any verification tool (be it Coq or TLA+) for a high-level specification and verification without extending it end-to-end, for a lowered confidence. If you like, you can augment that with code-level specification -- like JML (Java), ACSL (C), SPARK (Ada) etc.. [1]: https://link.springer.com/chapter/10.1007/978-3-319-17581-2_14 https://link.springer.com/chapter/10.1007/978-3-319-17581-2_... [2]: http://ieeexplore.ieee.org/document/6042069/ http://ieeexplore.ieee.org/document/6042069/
- nickpsecurity 9y ago
  "In principle, you could translate your code -- or even the generated machine code -- back to TLA+ and check it there. This has been done as research projects for C[1] and Java bytecode[2]." There's also ASM's and equational methods that allowed specification or verification of instructions or their use to happen in days when the tooling was already adequate. I wouldn't use TLA+ for this unless we're talking about concurrency. Even then, I'd be using it in combination with something else. You might also find it interesting that one group embedded TLA+ in a sound prover (HOL?) for making the TLA+ analysis sound. They extended it in some way, too. Anyway, the got the benefits of both with that combination. So, some weaknesses in the tooling can be knocked out over time if more people just put labor in.
  - pron 9y ago
    It all depends on your precise requirements and aesthetic preferences. I personally find TLA+ more elegant than any other high-level specification language, and very few projects actually require end-to-end verification. Those that do, must be kept small as we simply do not have the ability to do end-to-end verification of large software, no matter what tools or combination of tools we have. We don't even have a theoretical breakthrough to point us at a likely method of achieving that. If you need end-to-end verification, you must accept that the software (or component) verified will be small, and the process arduous. Then again, if you really need end-to-end verification, you must be ready to make that sacrifice. Moreover, to the best of my knowledge, no significant end-to-end verification was ever done in industry without close assistance from expert researchers, except in specialized niches where model-checkers give you sufficient coverage. Supplementing a high-level verification with code-level specification tools is always possible, but, again, everything here is a matter of the required confidence vs. affordable cost. Additional confidence always comes with additional cost.
codemac 9y ago
As Lamport says: why do we always use blueprints before constructing a building? I agree there are some missing links, but checking your model before doing detailed implementation is a good idea regardless
- unboxed_type 9y ago
  Absolutely. Anyway this gap is worth mentioning for deeper understanding of a verification problem.
microcolonel 9y ago
For seL4, models were used to map all the way from the semantics of the instruction set to the high level model; this included a model of equivalence between the C source code and the machine code. Took them basically from 2006 to 2014 to do that (including the time to author and verify the kernel in particular).

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

nickpsecurity 9y ago

That's why you implement it in Ada 2012 w/ SPARK 2014. You can encode the verification conditions as contracts. All the basic ones should be proven automatically. Those that aren't can be turned into runtime checks. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) http://www.electronicdesign.com/industrial/rust-and-spark-software-reliability-everyone http://www.electronicdesign.com/industrial/rust-and-spark-so... Here's an example of combining Event-B with SPARK to split overall verification between tools with each handling what they're good at: https://pdfs.semanticscholar.org/481c/d4d2409115429f4b824f370eb08fa338d67a.pdf https://pdfs.semanticscholar.org/481c/d4d2409115429f4b824f37...

unboxed_type 9y ago
How well Ada/SPARK suits distributed control algorithms I wonder? As far as I understand contracts are good enough for sequential code, but not well suited for parallel/distributed computation? Runtime checks are good as to prevent something from happening, but they are not able to guarantee the absence of an error in the first place, right?
- oconnore 9y ago
  Huh? The whole point of distributed algorithms is that a set of local algorithms create a global behavior. I received this message so I send that message, etc. The SPARK contracts you write would check that local behavior, and the TLA+ would check that that local behavior results in some global behavior.
  - unboxed_type 9y ago
    Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.

pron 9y ago

In principle, you could translate your code -- or even the generated machine code -- back to TLA+ and check it there. This has been done as research projects for C[1] and Java bytecode[2]. But the reality of formal verification is that we simply do not yet have the capability -- with any tool -- to formally specify and verify a large, complex software system end-to-end (namely, from high-level global correctness properties and all the way down to machine code). There are two options: either use tools that can do end-to-end verification like Coq and Isabelle and limit yourself to small software, and even then expend an inordinate amount of effort (like seL4 or CompCert, small programs that have been verified end-to-end, taking years), or use any verification tool (be it Coq or TLA+) for a high-level specification and verification without extending it end-to-end, for a lowered confidence. If you like, you can augment that with code-level specification -- like JML (Java), ACSL (C), SPARK (Ada) etc.. [1]: https://link.springer.com/chapter/10.1007/978-3-319-17581-2_14 https://link.springer.com/chapter/10.1007/978-3-319-17581-2_... [2]: http://ieeexplore.ieee.org/document/6042069/ http://ieeexplore.ieee.org/document/6042069/

nickpsecurity 9y ago
"In principle, you could translate your code -- or even the generated machine code -- back to TLA+ and check it there. This has been done as research projects for C[1] and Java bytecode[2]." There's also ASM's and equational methods that allowed specification or verification of instructions or their use to happen in days when the tooling was already adequate. I wouldn't use TLA+ for this unless we're talking about concurrency. Even then, I'd be using it in combination with something else. You might also find it interesting that one group embedded TLA+ in a sound prover (HOL?) for making the TLA+ analysis sound. They extended it in some way, too. Anyway, the got the benefits of both with that combination. So, some weaknesses in the tooling can be knocked out over time if more people just put labor in.
- pron 9y ago
  It all depends on your precise requirements and aesthetic preferences. I personally find TLA+ more elegant than any other high-level specification language, and very few projects actually require end-to-end verification. Those that do, must be kept small as we simply do not have the ability to do end-to-end verification of large software, no matter what tools or combination of tools we have. We don't even have a theoretical breakthrough to point us at a likely method of achieving that. If you need end-to-end verification, you must accept that the software (or component) verified will be small, and the process arduous. Then again, if you really need end-to-end verification, you must be ready to make that sacrifice. Moreover, to the best of my knowledge, no significant end-to-end verification was ever done in industry without close assistance from expert researchers, except in specialized niches where model-checkers give you sufficient coverage. Supplementing a high-level verification with code-level specification tools is always possible, but, again, everything here is a matter of the required confidence vs. affordable cost. Additional confidence always comes with additional cost.

codemac 9y ago

As Lamport says: why do we always use blueprints before constructing a building? I agree there are some missing links, but checking your model before doing detailed implementation is a good idea regardless

unboxed_type 9y ago
Absolutely. Anyway this gap is worth mentioning for deeper understanding of a verification problem.

microcolonel 9y ago

For seL4, models were used to map all the way from the semantics of the instruction set to the high level model; this included a model of equivalence between the C source code and the machine code. Took them basically from 2006 to 2014 to do that (including the time to author and verify the kernel in particular).