Lemma-functions and Abstract Axiomatics Support in Frama-C

Deductive verification lets you statically prove that a piece of code matches its contract (specification). This significantly helps with error prevention in critical software systems. At ISP RAS, the Frama-C static analysis platform with the AstraVer plugin is used for deductive verification of Linux kernel security modules. In order to increase the efficiency of verification in such large projects, this paper presents some modifications to Frama-C that extend its capabilities. When writing specifications, additional logical properties that must be proved are written separately as lemmas. Some lemmas can be difficult to prove using automatic theorem provers such as SMT solvers. A useful way to deal with that problem is replacing lemmas with equivalent functions (procedures) and their pre- and postconditions. The existence of a function body allows using proof by induction (via recursion or loops), intermediate local assertions, instantiation of the verification tool's built-in lemmas, etc. Proving lemmas as functions requires extending Frama-C with lemma-functions support. Also, in order to simplify proving the same set of properties on multiple data types or algorithms, it would be useful to have support for parameterizing specification modules (called "axiomatics" in ACSL, the specification language for Frama-C) by types and logical functions. This paper presents an implementation of lemma functions support (i.e. proving lemmas as functions) and abstract axiomatics support (i.e. an `include` statement and abstract lemmas) in the verification tool Frama-C.