30-May-2017: AstraVer plugin was presented at Frama-C & SPARK Day 2017
Our experience in deductive verification of Linux kernel components using Frama-C with AstraVer plugin, including our combined model for bounded integers, was presented at Frama-C & SPARK Day 2017 held on May, 30th at Université Paris-Diderot, Paris, France. We also presented out new region-based memory model implemented in AstraVer at the seminar of TOCCATA team at LRI, where Why3 deductive verification platform is developed.
AstraVer is a Frama-C plugin for deductive verification of low-level C code built on top of Why3 deductive verification platform and based on the earlier Jessie front-end for Why. AstraVer plugin is being developed in the Linux Deductive Verification project as an attempt to improve open source SMT-based deductive verification tools so they can be used to prove properties of Linux kernel code. Currently AstraVer implements a combined bitwise/linear model for bounded integral types and preliminary support for proofs expressed as ghost code. A new region-based memory model with support for arbitrary pointer casts, arithmetic and aliasing is under development.
Verification of continuously evolving low-level kernel code poses several specific challenges to automated deductive verification tools. Ubiquitous use of low-level C features e.g. nested structures (in particular, the container_of macro), non-prefix pointer type casts, unions, bit-twiddling and intentional use of wrap-around arithmetic suggests usage of suitable low-level and precise models for memory and integer operations e.g. the theory of bit-vectors and low-level memory model with support for reinterpretation. But the use of such models significantly decreases performance of automatic provers, in particular, SMT solvers. In AstraVer we are implementing a class of approaches based on composite, mixed-level, though non-fully-automated models, requiring user guidance in the form of special additional annotations.
In our talk "Specifying and Proving Correctness of Linux Kernel Components with ACSL" on Frama-C & SPARK Day 2017 (May, 30th) we presented our experience in deductive verification of Linux kernel components using Frama-C with AstraVer plugin and our composite model for integers, which allows to prove properties of non-trivial bit-manipulating code fragments with the use of special annotations, ghost code and lemma functions.
On the day before (May, 29th) we gave a talk on a local seminar organized by TOCCATA team of Laboratoire de recherche en informatique at INRIA Saclay, where Why3 platform for deductive verification is being developed. In this talk titled "A Memory Model and Other Extensions of ACSL Made for Deductive Verification of Linux Kernel Modules" we presented our region-based memory model with reinterpretation, whose region analysis is unsound in general and therefore the proof may soundly fail in some cases expecting user intervention in the form of special annotations. Through possible additional user guidance the model is able to efficiently support arbitrary pointer aliasing, pointer casts and arithmetic.