Hello everyone, I just started working on the verification of operating system kernels. During the process of learning seL4 verification, I don’t understand the role of Haskell models in the verification process. The c code of seL4 is manually written in Haskell, so why not just manually write the c code and then verify it? Why do we have to first establish a Haskell model?
Thank you very much.
You don’t really have to first establish a Haskell model, we just found it a convenient mid point between a pure specification and an actual implementation.
It is very hard to verify a larger piece of software from only a low-level C implementation, because the factors that make verification simpler and easier are not visible at that level. It is also hard to produce a good high-performance implementation from just a high-level verified specification, because at that level the performance details are not visible. So we used something that is executable and can support low-level details, but that also provides most of the features of a high-level specification language (strong typing, functional paradigm, code structuring mechanisms etc).
Haskell is just what worked for us. You could probably also start out at an executable specification level just in Isabelle/HOL (and possibly even generate code from there to experiment with it). Anything that lets you experiment, but forces you to respect types and structure, guides you to think abstractly and that translates easily (and usefully for verification) into Isabelle/HOL could work. If you are extremely good at predicting performance and data structure impacts, you could start with the specification, or if you can predict extremely well what C implementations will turn into nice, coherent abstract structures in HOL with reasonable invariants and if you have the discipline to never break them, then you could start with an implementation.
Depending on how deep you want your verification to go, the implementation is about 5-10 times cheaper to produce than the verification. That means, anything that will speed up the verification at the cost of making implementation speed (not execution speed) lower is easily worth it. You could even write a full new implementation from scratch twice or three times and still come out ahead in time and cost after verification if the last instance is significantly faster or cheaper to verify for some reason.
The following two papers talk a bit more about the initial idea of the Haskell model and the verification process:
1 Like