I had the paper “Efficient Formal Verification for the Linux Kernel” at the 17th International Conference on Software Engineering and Formal Methods (SEFM 2019).
It has the following abstract:
Formal verification of the Linux kernel has been receiving increasing attention in recent years, with the development of many models, from memory subsystems to the synchronization primitives of the real-time kernel. The effort in developing formal verification methods is justified considering the large code-base, the complexity in synchronization required in a monolithic kernel and the support for multiple architectures, along with the usage of Linux on critical systems, from high-frequency trading to self-driven cars. Despite recent developments in the area, none of the proposed approaches are suitable and flexible enough to be applied in an efficient way to a running kernel. Aiming to fill such a gap, this paper proposes a formal verification approach for the Linux kernel, based on automata models. It presents a method to auto-generate verification code from an automaton, which can be integrated into a module and dynamically added into the kernel for efficient on-the-fly verification of the system, using in-kernel tracing features. Finally, a set of experiments demonstrate verification of three models, along with performance analysis of the impact of the verification, in terms of latency and throughput of the system, showing the efficiency of the approach.
Sincerely, this is the paper I most enjoyed writing. It has a very easy reading and good practical results. But the best thing is that, by having my approach recognized by the formal methods community, I feel more conformable about using the word “formal“, which is a very strong word. This is one of the cherries of my Ph.D. Now it is time to work in the second cherry…. and that we are done.
I am also curious to attend the conference, the list of paper is very interesting, and I need to deeper my knowledge in the area.
