28-Jun-2018: Linux Verification Center at Sound Static Analysis for Security Workshop

Alexey Khoroshilov presented the experience of Linux Verification Center in proving sequential properties of unmodified Linux kernel code using Frama-C with AstraVer plugin at Sound Static Analysis for Security Workshop held at the National Institute of Standards and Technology (NIST) in Gaithersburg, Maryland, USA, on June 27-28, 2018.

Sound Static Analysis for Security is a two-day workshop focused on decreasing software security vulnerabilities by orders of magnitude, using the strong guarantees that only sound static analysis can provide. The program features experts on sound static analysis applied to security, around three theme topics:

• Analysis of legacy code,
• Use in new developments,
• Accountable software quality.

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.

That was the reason for building AstraVer plugin to Frama-C that tries 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.