4 ms·

seL4 has a Haskell implementation. It only runs under a simulator (as opposed to on real hardware). Their main proof strategy is to prove the Haskell version co

seL4 has a Haskell implementation. It only runs under a simulator (as opposed to on real hardware). Their main proof strategy is to prove the Haskell version correct; then prove the C version matches the Haskell version.

tsimionescu 1y ago
I admit that I was not aware of their use of Haskell, so thanks for bringing this up! It motivated me to go and actually read (parts of) their paper [0]. > Their main proof strategy is to prove the Haskell version correct; then prove the C version matches the Haskell version. However, I don't think this is right. By my understanding of the paper, the Haskell implementation isn't proven to be correct, it's more of a prototyping tool. The Haskell version is used as an intermediate representation that can be automatically translated into Isabelle/HOL and quickly proven to have various properties. If the proofs don't work at this level, it's easy to change, re-translate, and re-check. To make it easily tramslatable to Isabelle/HOL, they forego many Haskell features, such as typeclasses, or making use of laziness. The Haskell program is also designed to match the eventual C implementation, so it's using C-like data types, pointers, etc - not native Haskell data structures,nor making use of the Haskell GC. The proofs achieved at this level apply to the auto-generated Isabelle/HOL translation of the Haskell code. The Haskell runtime is not modeled here in any way, and as such the proofs do not hold for the Haskell executable code that you can run on the simulator. The Haskell prototype was then translated manually to C, trying to keep as close to a 1:1 translation as possible, while still allowing various micro-optimizations. Then, the exact C code was manually translated back to Isabelle/HOL, where they also had a complete model of the semantics of every C statement that they used (they use a subset of C, with the biggest missing feature being references to local variables - you can't use &x if x is a local variable in their C code). Isabelle/HOL was then used to check that this manually written implementation implemented the abstract specification with all of the proven guarantees. So, the Haskell part was ultimately a convenience, not a fully necessary part of the proof (though the whole thing would probably not have been feasible had they not used it). It was a decent middle ground between being possible for the kernel devs to define the code in it, and the formal verification guys to translate it to Isabelle and verify it. If they had tried to write the C code directly, the cost of translating any change to the C code back to Isabelle for verification would have been too high. Conversely, having the kernel devs learn enough Isabelle to define the prototype code directly in Isabelle would have also been too complicated as well - and I believe the Isabelle code could not be easily executed to be able to do more regular debugging on it during the development process, the way the Haskell code could be run on the simulator. [0] https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-...

tsimionescu 1y ago

I admit that I was not aware of their use of Haskell, so thanks for bringing this up! It motivated me to go and actually read (parts of) their paper [0]. > Their main proof strategy is to prove the Haskell version correct; then prove the C version matches the Haskell version. However, I don't think this is right. By my understanding of the paper, the Haskell implementation isn't proven to be correct, it's more of a prototyping tool. The Haskell version is used as an intermediate representation that can be automatically translated into Isabelle/HOL and quickly proven to have various properties. If the proofs don't work at this level, it's easy to change, re-translate, and re-check. To make it easily tramslatable to Isabelle/HOL, they forego many Haskell features, such as typeclasses, or making use of laziness. The Haskell program is also designed to match the eventual C implementation, so it's using C-like data types, pointers, etc - not native Haskell data structures,nor making use of the Haskell GC. The proofs achieved at this level apply to the auto-generated Isabelle/HOL translation of the Haskell code. The Haskell runtime is not modeled here in any way, and as such the proofs do not hold for the Haskell executable code that you can run on the simulator. The Haskell prototype was then translated manually to C, trying to keep as close to a 1:1 translation as possible, while still allowing various micro-optimizations. Then, the exact C code was manually translated back to Isabelle/HOL, where they also had a complete model of the semantics of every C statement that they used (they use a subset of C, with the biggest missing feature being references to local variables - you can't use &x if x is a local variable in their C code). Isabelle/HOL was then used to check that this manually written implementation implemented the abstract specification with all of the proven guarantees. So, the Haskell part was ultimately a convenience, not a fully necessary part of the proof (though the whole thing would probably not have been feasible had they not used it). It was a decent middle ground between being possible for the kernel devs to define the code in it, and the formal verification guys to translate it to Isabelle and verify it. If they had tried to write the C code directly, the cost of translating any change to the C code back to Isabelle for verification would have been too high. Conversely, having the kernel devs learn enough Isabelle to define the prototype code directly in Isabelle would have also been too complicated as well - and I believe the Isabelle code could not be easily executed to be able to do more regular debugging on it during the development process, the way the Haskell code could be run on the simulator. [0] https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-...