« BACK TO PROGRAM

Proving sequential properties of unmodified Linux kernel code

Alexey Khoroshilov - Linux Verification Center of ISPRAS

Verification of legacy code often means that you have no ability to fix the code to simplify its verification.As a result verification tools have to support many complex corner cases in semantics of the target programming platform, most notably in low-level platforms based on C programming language that lack well-defined semantics for many cases widely used in practice.

The talk presents the experience in proving sequential properties of Linux kernel code using Frama-C with AstraVer plugin that has appeared as an attempt to solve this problem by implementing support for C code used in Linux kernel. The first target for the AstraVer plugin was a custom implementation of Linux security module that is a component responsible for implementation of access control policy. Another target was a set of unmodified Linux kernel library functions implementing conventional memory and string operations.

Download this presentation

About Alexey Khoroshilov

Alexey works for Ivannikov Institute for System Programming of the Russian Academy of Sciences (ISPRAS) since 1999. His research interest includes formal methods for software and hardware systems, model based testing, verification of operating systems and design of safety critical embedded systems. Alexey was the lead architect of the LSB Infrastructure program run jointly by ISPRAS and the Linux Foundation. He is a director of the Linux Verification Center of ISPRAS, where a number of advanced verification techniques are developed and applied to Linux kernel and other real-time operating systems.