ИСТИНА

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.