While our open-source L4Re Operating System Framework was originally developed more than a decade ago, our system engineers are steadily working to improve it. One of our most important future projects is formal verification of the correctness of the L4Re Operating System Framework. With formal methods we aim to improve the quality of L4Re for use in safety and security-critical systems.
This is where we want to introduce our colleague Hendrik Tews, who has been with us since 2017. He has a long scientific history in the field of formal methods; he studied the subject both as a researcher and on the market, working for several software manufacturers.
At Kernkonzept, Hendrik is mainly working at preparing and realizing safety and security certifications for our open-source L4Re technology. Certification and formal verification are tightly connected, as both are aiming to prove that a given software is reliably doing what it is supposed to do.
Hendrik helps us to pursue a long-term plan to formally specify the properties of the L4Re Operating System Framework and to formally prove its correctness. Formal verification of a real-world software is a costly and time-consuming endeavour, even it is a microkernel with a minimal code base. Therefore, many companies feel that it is not worth the effort, especially because formal verification on the software market is still almost nonexistent.
Nevertheless, we believe it can make a difference in the future – especially because L4Re is used for lots of safety and security critical applications with highest quality requirements. With the help of formal methods, we can further improve the quality and safety of the L4Re Operating System Framework.
What can you prove with formal methods – and what not?
Formal methods refers to a collection of techniques that permit to prove the correctness of software in the mathematical sense. In the same way as there are no triangles whose angles sum up to something different than two right angles, there is no formally proven software that fails.
Of course, there are triangles where the angles sum up to much more than two right angles, for instance on a sphere in non-euclidean geometry. And so, a formally proven program can show bugs, for instance because the specification did not rule out the wrong behavior, because the program runs on hardware which has not been formally verified, or because some parts of the program have been left out during formal verification.
However, experience shows that the formally verified parts of a program are bug free with respect to properties that have been considered during formal verification.
How we will achieve formal verification of L4Re
Our long-term goal, a formally verified variant of L4Re, requires a huge amount of effort. So we are taking small steps: First we want to develop an abstract model of the L4Re core, to prove a meaningful separation property about this model and to provide evidence that the real L4Re behaves as specified by the model.
We will scrutinize L4Re and its abstract model by model-based testing and check the equivalence of both with a 6-digit number of tests. Model-based testing can reveal a lot of buggy or unexpected behavior, even in parts of the system that have been abstracted away and are thus not present in the model.
The result can be understood as a formally verified design of L4Re, similar to what the Common Criteria scheme requires for higher assurance levels.
Do we need formal verification?
Not yet! Most software companies today do not invest in formal verification. But certain market segments could actually move to require formal methods in the near future; it is absolutely possible that formal methods could be officially required someday for software certification and accreditation.
Kernkonzept wants to be prepared for this future, and we are talking to appropriate stakeholders to push these developments. Current trends in the software industry encourage us to stay on our chosen path.
