8 ms·

I'd be really happy to see seL4 thrive and I like that this blog-post shows that the people behind it understand what could potential hold it back - the infrast

I'd be really happy to see seL4 thrive and I like that this blog-post shows that the people behind it understand what could potential hold it back - the infrastructure around it. It needs what GNU and systemd are for Linux. And it needs an Arduino/Raspberry Pi - a halo platform that I can buy and play around with. What I wonder is how this formal verification works. seL4 is written in C and apparently the formal verification is done in a different language. Is it possible to have a programming language where the compiler does the formal verification?

saithound 7y ago
> Is it possible to have a programming language where the compiler does the formal verification? It is possible, but using separate languages (as seL4 does) has certain benefits. For example: - Kernel developers tend to have C experience. If the OS is writen in C, they have a much larger pool to hire from. - Any such language would have to be acceptable both for the people who develop the OS and for the people who do the verification: I suspect it's not easy to find something that pleases both crowds. - C compilers get better all the time. Every time someone improves the gcc code generator, seL4 automatically gets a bit faster. Less mainstream programming languages get better only if you maintain an expensive in-house team working on the compiler.
- MaxBarraclough 7y ago
  Formal methods aren't just an academic curiosity, they have been used for real-world OS work. https://en.wikipedia.org/wiki/SLAM_project https://en.wikipedia.org/wiki/SLAM_project > Less mainstream programming languages get better only if you have an expensive in-house team working on the compiler. Not if you defer optimisation to an external (and actively maintained) backend like LLVM. Rust and Zig do this.
  - antoinealb 7y ago
    "Better" is not only a compiler backend thing. Things like better static analysis could also matter. I believe some optimisations are also done by the front end but I don't know enough about compiler design to expand on that.
- cwzwarich 7y ago
  > C compilers get better all the time. Every time someone improves the gcc code generator, seL4 automatically gets a bit faster. Less mainstream programming languages get better only if you maintain an expensive in-house team working on the compiler. Doesn't SeL4 need -O1 codegen to make their extraction from the generated code (and the thus the rest of the formal proof) work out?
  - saithound 7y ago
    The 2017 paper [1] says that they "can handle most of seL4 even at optimisation level 2", presumably it got better in the meantime. Also, it's not like code generation is the only advantage of using a well-supported, externally developed compiler. It's just the one I picked as an illustrative example. GCC releases improve code generation, general usability, diagnostic format support, profilers, etc., at a rate that would be hard to match for a niche language, especially without hiring a dedicated compiler development team. [1] https://ts.data61.csiro.au/publications/nicta_full_text/6449.pdf https://ts.data61.csiro.au/publications/nicta_full_text/6449... [2] https://gcc.gnu.org/gcc-9/changes.html https://gcc.gnu.org/gcc-9/changes.html
- vbezhenar 7y ago
  How will it prove that this new optimization does not introduce bugs? It's not like GCC is verified compiler.
  - saithound 7y ago
    Great question. They don't have to trust the compiler: after compilation, they use an SMT-based proof process to establish that the resulting binary matches the semantics of the C source directly. See https://ts.data61.csiro.au/publications/nicta_full_text/6449.pdf https://ts.data61.csiro.au/publications/nicta_full_text/6449....
    - zingermc 7y ago
      Ah, it appears that is only done for ARM, but not x86. It would be great if x86 were more amenable to FM, or if we had faster formally-specified processors. Can't wait for a RISC-V workstation!
- hinkley 7y ago
  Probably an Unsolved Problem in computer programming: If you are trying to solve an old problem a new way, is it necessarily true that having a large pool of applicants is an advantage? It could be a liability. On the one hand, there could be more variance in a large pool, so you might find a lot of unconventional thinkers who think like you. On the other hand, large groups have social mores, and so the dogma might be difficult to overcome, like the old "people can write fortran in any language" problem.
lawfulcactus 7y ago
So, I think what you're missing here is that the 'verification' is a formal specification about the behavior of the kernel, along with a set of proofs about that specification. This is vastly simplified (there are multiple levels of specification, last I checked), but that's the general idea. It's possible to have your compiler automatically derive the specification from your code (and, indeed, the seL4 people have written a Rust-like language called Cogent that does this), but formal verification inherently involves an understanding of what your code is /intended/ to do, and proving that it /does/. The compiler only has information about what it /does/, so it can only generate a specification that describes this. Information about your high-level intentions for the code has to be concretized somewhere, while ensuring that the spec conforms to it-- that's the job of the proof engineers.
- turbinerneiter 7y ago
  How does this formal specification look like? From my naive standpoint: input, output, side-effect, time [no_sideffect, 1ms] fn increment(int i) -> int: return i + 1 What this is missing is a formal statement that says "increases the value of the input by one" -> except you accept the function body as formal statement. Thanks for all the answers here, I guess I'm going to look for some more reading material.
  - logicchains 7y ago
    Here's a specification of an increment function in Isabelle/HOL, the theorem prover used for SeL4, plus some other random lemmas about it: theory Scratch imports Main begin fun increment :: "int ⇒ int" where "increment x = x + 1" lemma increment_increments: shows "increment x = x + 1" by simp lemma double_increment_adds_two: shows "increment (increment x) = x + 2" by simp lemma increment_sub_1_is_x: shows "increment x - 1 = x" by simp
  - shawnz 7y ago
    If you take the original code as the formal statement, how could it ever be wrong?
  - 7y ago
MaxBarraclough 7y ago
> What I wonder is how this formal verification works Curiously it involves Haskell for its specification. [0] They've also done some very impressive work verifying that the ARM machine code corresponds to the verified C code. They did this not by using a formally verified compiler, but by using GCC and then verifying the correspondence afterwards. > Is it possible to have a programming language where the compiler does the formal verification? Yes, but these languages are not all that approachable. There's SPARK, which is Ada-based and has seen real-world use in various life-or-death applications like military aviation. There's also ZZ, which is in early days, and which aims to be closer to C. [2] [3] There's also Perfect Developer, a proprietary payware product, which does impressive things adding formal verification machinery to C and C++. [4] [0] https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass... [1] https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) [2] https://github.com/aep/zz https://github.com/aep/zz [3] https://news.ycombinator.com/item?id=22245409 https://news.ycombinator.com/item?id=22245409 [4] https://www.eschertech.com/articles/index.php https://www.eschertech.com/articles/index.php
- wahern 7y ago
  How does Perfect Developer compare to Frama-C? Is it more capable or maybe simply more convenient for MISRA verification? For the unfamiliar, see http://frama-c.com/ http://frama-c.com/ and https://en.wikipedia.org/wiki/Frama-C https://en.wikipedia.org/wiki/Frama-C
h91wka 7y ago
> Is it possible to have a programming language where the compiler does the formal verification? Such compiler would require solving halting problem. Most problems related to search of formal proofs are undecidable.
- MaxBarraclough 7y ago
  This is true, but SPARK and ZZ do it anyway. Automatic deductive program-verification can work, but the halting problem means there will always be truths than cannot be automatically proved. This can still be good enough to get the job done. In the case of SPARK, it's necessary to use timeouts on the prover. Ugly, sure enough, but real work can still be done with it. https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial.html https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial....
  - simiones 7y ago
    If we want to go to extremes, it's even worse than the halting problem. Godel's incompleteness theorem shows that, assuming your system is consistent, there are truths that don't have a proof at all, which is even worse than not being able to compute that proof. Still, the only impact this has in practice is that it tells you languages or programming styles amenable to automatic verification must be very limited in their expresiveness/flexibility.
    - MaxBarraclough 7y ago
      > the only impact this has in practice is that it tells you languages or programming styles amenable to automatic verification must be very limited in their expresiveness/flexibility. This is a consequence of the state of current tooling, rather than an inescapable consequence of the relevant math. A concrete example: the SPARK language is a subset of Ada, but with each release it gets less claustrophobic. You can even go to the other end of the programming language spectrum, and use formal methods with functional programming languages. I don't think anyone develops real critical systems this way, but I believe it's an active area of research.
qznc 7y ago
Practically every compiler does formal verification. The type checking of C for example. The question is what properties you want to verify. It isn't a binary question but rather a continuum from C up to Isabelle/Coq.
- cwzwarich 7y ago
  Is it really formal verification if the type system is unsound? Due to undefined behavior, a "proven pointer-to-int" may not end up being a valid pointer-to-int at runtime. Even in Haskell, the type system is actually logically inconsistent (see http://okmij.org/ftp/Haskell/impredicativity-bites.html http://okmij.org/ftp/Haskell/impredicativity-bites.html).
skyde 7y ago
spark version of Ada is such a language but it use design by contract assertion only.
jiveturkey 7y ago
> systemd nobody needs systemd. nobody but RedHat. it is a step backwards, net net.
mycall 7y ago
I see Genode Operating System Framework as the infrastructure it needs.

saithound 7y ago

> Is it possible to have a programming language where the compiler does the formal verification? It is possible, but using separate languages (as seL4 does) has certain benefits. For example: - Kernel developers tend to have C experience. If the OS is writen in C, they have a much larger pool to hire from. - Any such language would have to be acceptable both for the people who develop the OS and for the people who do the verification: I suspect it's not easy to find something that pleases both crowds. - C compilers get better all the time. Every time someone improves the gcc code generator, seL4 automatically gets a bit faster. Less mainstream programming languages get better only if you maintain an expensive in-house team working on the compiler.

MaxBarraclough 7y ago
Formal methods aren't just an academic curiosity, they have been used for real-world OS work. https://en.wikipedia.org/wiki/SLAM_project https://en.wikipedia.org/wiki/SLAM_project > Less mainstream programming languages get better only if you have an expensive in-house team working on the compiler. Not if you defer optimisation to an external (and actively maintained) backend like LLVM. Rust and Zig do this.
- antoinealb 7y ago
  "Better" is not only a compiler backend thing. Things like better static analysis could also matter. I believe some optimisations are also done by the front end but I don't know enough about compiler design to expand on that.
cwzwarich 7y ago
> C compilers get better all the time. Every time someone improves the gcc code generator, seL4 automatically gets a bit faster. Less mainstream programming languages get better only if you maintain an expensive in-house team working on the compiler. Doesn't SeL4 need -O1 codegen to make their extraction from the generated code (and the thus the rest of the formal proof) work out?
- saithound 7y ago
  The 2017 paper [1] says that they "can handle most of seL4 even at optimisation level 2", presumably it got better in the meantime. Also, it's not like code generation is the only advantage of using a well-supported, externally developed compiler. It's just the one I picked as an illustrative example. GCC releases improve code generation, general usability, diagnostic format support, profilers, etc., at a rate that would be hard to match for a niche language, especially without hiring a dedicated compiler development team. [1] https://ts.data61.csiro.au/publications/nicta_full_text/6449.pdf https://ts.data61.csiro.au/publications/nicta_full_text/6449... [2] https://gcc.gnu.org/gcc-9/changes.html https://gcc.gnu.org/gcc-9/changes.html
vbezhenar 7y ago
How will it prove that this new optimization does not introduce bugs? It's not like GCC is verified compiler.
- saithound 7y ago
  Great question. They don't have to trust the compiler: after compilation, they use an SMT-based proof process to establish that the resulting binary matches the semantics of the C source directly. See https://ts.data61.csiro.au/publications/nicta_full_text/6449.pdf https://ts.data61.csiro.au/publications/nicta_full_text/6449....
  - zingermc 7y ago
    Ah, it appears that is only done for ARM, but not x86. It would be great if x86 were more amenable to FM, or if we had faster formally-specified processors. Can't wait for a RISC-V workstation!
hinkley 7y ago
Probably an Unsolved Problem in computer programming: If you are trying to solve an old problem a new way, is it necessarily true that having a large pool of applicants is an advantage? It could be a liability. On the one hand, there could be more variance in a large pool, so you might find a lot of unconventional thinkers who think like you. On the other hand, large groups have social mores, and so the dogma might be difficult to overcome, like the old "people can write fortran in any language" problem.

lawfulcactus 7y ago

So, I think what you're missing here is that the 'verification' is a formal specification about the behavior of the kernel, along with a set of proofs about that specification. This is vastly simplified (there are multiple levels of specification, last I checked), but that's the general idea. It's possible to have your compiler automatically derive the specification from your code (and, indeed, the seL4 people have written a Rust-like language called Cogent that does this), but formal verification inherently involves an understanding of what your code is /intended/ to do, and proving that it /does/. The compiler only has information about what it /does/, so it can only generate a specification that describes this. Information about your high-level intentions for the code has to be concretized somewhere, while ensuring that the spec conforms to it-- that's the job of the proof engineers.

turbinerneiter 7y ago
How does this formal specification look like? From my naive standpoint: input, output, side-effect, time [no_sideffect, 1ms] fn increment(int i) -> int: return i + 1 What this is missing is a formal statement that says "increases the value of the input by one" -> except you accept the function body as formal statement. Thanks for all the answers here, I guess I'm going to look for some more reading material.
- logicchains 7y ago
  Here's a specification of an increment function in Isabelle/HOL, the theorem prover used for SeL4, plus some other random lemmas about it: theory Scratch imports Main begin fun increment :: "int ⇒ int" where "increment x = x + 1" lemma increment_increments: shows "increment x = x + 1" by simp lemma double_increment_adds_two: shows "increment (increment x) = x + 2" by simp lemma increment_sub_1_is_x: shows "increment x - 1 = x" by simp
- shawnz 7y ago
  If you take the original code as the formal statement, how could it ever be wrong?
- 7y ago

MaxBarraclough 7y ago

> What I wonder is how this formal verification works Curiously it involves Haskell for its specification. [0] They've also done some very impressive work verifying that the ARM machine code corresponds to the verified C code. They did this not by using a formally verified compiler, but by using GCC and then verifying the correspondence afterwards. > Is it possible to have a programming language where the compiler does the formal verification? Yes, but these languages are not all that approachable. There's SPARK, which is Ada-based and has seen real-world use in various life-or-death applications like military aviation. There's also ZZ, which is in early days, and which aims to be closer to C. [2] [3] There's also Perfect Developer, a proprietary payware product, which does impressive things adding formal verification machinery to C and C++. [4] [0] https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass... [1] https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) [2] https://github.com/aep/zz https://github.com/aep/zz [3] https://news.ycombinator.com/item?id=22245409 https://news.ycombinator.com/item?id=22245409 [4] https://www.eschertech.com/articles/index.php https://www.eschertech.com/articles/index.php

wahern 7y ago
How does Perfect Developer compare to Frama-C? Is it more capable or maybe simply more convenient for MISRA verification? For the unfamiliar, see http://frama-c.com/ http://frama-c.com/ and https://en.wikipedia.org/wiki/Frama-C https://en.wikipedia.org/wiki/Frama-C

h91wka 7y ago

> Is it possible to have a programming language where the compiler does the formal verification? Such compiler would require solving halting problem. Most problems related to search of formal proofs are undecidable.

MaxBarraclough 7y ago
This is true, but SPARK and ZZ do it anyway. Automatic deductive program-verification can work, but the halting problem means there will always be truths than cannot be automatically proved. This can still be good enough to get the job done. In the case of SPARK, it's necessary to use timeouts on the prover. Ugly, sure enough, but real work can still be done with it. https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial.html https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial....
- simiones 7y ago
  If we want to go to extremes, it's even worse than the halting problem. Godel's incompleteness theorem shows that, assuming your system is consistent, there are truths that don't have a proof at all, which is even worse than not being able to compute that proof. Still, the only impact this has in practice is that it tells you languages or programming styles amenable to automatic verification must be very limited in their expresiveness/flexibility.
  - MaxBarraclough 7y ago
    > the only impact this has in practice is that it tells you languages or programming styles amenable to automatic verification must be very limited in their expresiveness/flexibility. This is a consequence of the state of current tooling, rather than an inescapable consequence of the relevant math. A concrete example: the SPARK language is a subset of Ada, but with each release it gets less claustrophobic. You can even go to the other end of the programming language spectrum, and use formal methods with functional programming languages. I don't think anyone develops real critical systems this way, but I believe it's an active area of research.

qznc 7y ago

Practically every compiler does formal verification. The type checking of C for example. The question is what properties you want to verify. It isn't a binary question but rather a continuum from C up to Isabelle/Coq.

cwzwarich 7y ago
Is it really formal verification if the type system is unsound? Due to undefined behavior, a "proven pointer-to-int" may not end up being a valid pointer-to-int at runtime. Even in Haskell, the type system is actually logically inconsistent (see http://okmij.org/ftp/Haskell/impredicativity-bites.html http://okmij.org/ftp/Haskell/impredicativity-bites.html).

skyde 7y ago

spark version of Ada is such a language but it use design by contract assertion only.

jiveturkey 7y ago

> systemd nobody needs systemd. nobody but RedHat. it is a step backwards, net net.

mycall 7y ago

I see Genode Operating System Framework as the infrastructure it needs.