AstraVer Toolset. Deductive verification of Linux kernel modules and security policy models
Software plays a key role in many systems, e.g., safety-, security-, and missioncritical systems. Bugs in such software can lead to catastrophic consequences. As a result development of critical software is regulated by certification standards/guidelines (like DO-178С, ISO/IEC 15408, etc) that require following best practices in development process.
For example, ISO/IEC 15408 "Information technology -- Security techniques -- Evaluation criteria for IT security" requires including of the following activities:
- formal security policy modelling (ADV_SPM);
- formal verification of internal consistency of a security policy model;
- formal proof that the target system cannot reach an unsecure state;
- development of formal and semi-formal functional specification;
- formal proof of correspondence between the security policy model and the functional specification;
- formal proof of correspondence between different representations of target software like functional specification, design and source code.
ISPRAS has developed methods and tools implementing these activities. The approach has been applied for verification of security module of Astra Linux Special Edition operating system developed by RusBITech.
The approach suggests using two specification languages with corresponding toolsets:
- security policy models and formal functional specifications are specified in Event-B;
- formal specification of critical implementation components is done in ACSL.
Event-B and Rodin
Event-B specification consists of contexts and machines. Contexts contain the static part of a specification: constants, carrier sets, axioms. Machines contain the dynamic part: variables, invariants, events. The current state of a specification is formed by means of variables whose values are constrained by invariants and changed by events.
State invariants allow both ensuring the internal consistency of a machine and formalizing the notion of a "safe" state required by ISO/IEC 15408-3, ADV_SPM.1.2C.
Each event consists of parameters, guards, actions. Guards restrict the values of event parameters and machine variables reducing the number of states in which the event can occur. Actions modify the current state by assigning new values to the variables. Event-B also allows us to decompose specifications using the refinement technique to simplify the development, verification and support processes.
Event-B specifications are developed and verified using the Rodin platform (developed under open source license by ETH Zurich, Systerel, Clearsy, University of Newcastle and University of Southampton) and its plug-ins. Rodin automatically generates proof obligations for each case that requires proof: invariant preservation; well-defined axioms, invariants, guards, actions; refinement correctness. To fully verify the model all generated proof obligations need to be proved. To do this, Rodin allows using various automatic provers (for example, SMT solvers) as well as performing interactive proof.
ACSL and AstraVer Toolset
Formal specifications of component interfaces in C language are proposed to be described in a special language called ACSL (ANSI/ISO C Specification Language).
ACSL is a C programs behavior specification language that supports contract specifications from the most low-level, such as "this function requires a valid initialized pointer to int as an input", to high-level, for example: "this function requires a non-empty linked list of int values as an input and returns maximum of these values". Expressive power of ACSL language is enough to fully specify various functions, and it can also be used to write partial specifications.
Deductive verification is based on the translation of C source code annotated with specifications of checked properties into a set of logical formulae, which general significance is equivalent to the source program being correct in accordance with given properties (if a precondition holds when function is called, then function will finish and its result fulfills its post-condition). These logic formulae, known as verification conditions, can be checked for satisfiability with many different tools: automatic, such as Z3, CVC, Alt-Ergo, Vampire, E-Prover etc., or requiring user participation, for example, interactive theorem provers such as Coq and PVS.
Existing deductive verification tools don't support all the features of C language used in operating system kernels. As a result Astraver Toolset, a new deductive verification toolset, was developed by ISPRAS. The toolset is based on an open C program verification platform Frama-C (CEA-LIST, France) and deductive verification system Why3 (INRIA, France), and includes the following new features:
- 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.
More information can be found here.