Linux Deductive Verification

Linux Deductive Verification project aims to improve open source deductive verification tools, so they can be used to prove properties of Linux kernel code. A target for the first round of the project is a custom LSM implementation that is a part of the Astra Linux Special Edition distribution. The follow-up target is a set of formally verified Linux kernel library functions with publicly available specifications and proof protocols.

We build our efforts on top of the 'Frama-C + Jessie + Why3 IDE' deductive verification toolchain. The toolchain was adapted, so it can be used to prove properties of Linux kernel code. The most of our modifications goes to the Jessie plugin, while the Frama-C front-end and the Why3 platform have got just minor fixes or improvements. Some of our modifications were already applied upstream, while the rest is available in our public repositories.

The main new features of the toolset includes:

  • Container_of construct support.
  • Function pointers support.
  • Expression-level support for bitwise arithmetic operations.
  • Support for pointer type reinterpretation between integer types, incl. types of different size.
  • Zero-sized arrays support.
  • String literals support.
  • Template specifications for standard library memory operations.
  • Control flow highlighting for verification conditions in Why3ide.

Additional information about our improvements is presented in the release notes:

Subscription to the user's mailing list of Linux Deductive Verification project is available here:
http://linuxtesting.org/cgi-bin/mailman/listinfo/astraver-project

Publications

Some details of the project results were presented at: