AstraVer Toolset¶

AstraVer Toolset is built on top of 'Frama-C + Jessie plugin + Why3' deductive verification toolchain, so it can be used to prove properties of Linux kernel code.

Jessie2 is a fork of the Jessie plug-in for Frama-C that allows deductive verification of C programs annotated with ACSL and is primarily targeted at Linux kernel modules source code. It uses the language and tools of the Why3 verification platform. Unlike original Jessie, Jessie2 is not distributed as a part of the Why2 verification platform and is compiled/installed separately.
Note: For now, this fork requires modified version of the Frama-C source code analysis platform, that is based on the Sodium 20150201 version of the original platform.

Installation¶

Using OPAM¶

• Install OPAM as described on the OPAM documentation.
  For example (installing to /usr/local/bin unsing the binary installer):
  

      wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh
      chmod +x opam_installer.sh
      sudo ./opam_installer.sh /usr/local/bin
      

• Initialize OPAM to use the OCaml 4.03.0 compiler:
  

      opam init --comp 4.03.0
      eval `opam config env`
      

• Install Git.
  For example on Ubuntu:
  

      sudo apt-get install git
      

• Add ISPRAS OPAM repository at https://forge.ispras.ru/git/astraver.opam-repository.git with Jessie2 and modified Frama-C Sodium packages to the OPAM installation
  (ispras is just an arbitrary name of the new repository):
  

      opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git
      

• Install external dependencies for the Jessie2 and Frama-C build i.e. Autoconf, Gtk2 development files and M4.
  Ubuntu example:
  

      sudo apt-get install $(opam install -e ubuntu jessie2)
      

• Build and install the Jessie2 plugin for Frama-C with OPAM (the Frama-C itself will be built and installed automatically). One
  can use the -j option to speed-up compilation on a multi-core machine:
  

      opam install -j 1 jessie2
      

• Build and install either original or patched (search in task view, empty theory filtering) version of the Why3 verification platform:
  

      sudo apt-get install $(opam install -e ubuntu why3) # Install GMP (external dependency) on Ubuntu
      opam install -j 4 why3
      

• The one using Jessie would also likely need SMT solvers e.g. Alt-Ergo (also Z3, CVC4 and others). Alt-Ergo can be installed via OPAM:
  

       opam install alt-ergo altgr-ergo satML-plugin
      

• The Why3 IDE should be initialized to detect available provers (and plugins):
  

      why3 config --detect-provers --detect-plugins
      

Our Repositories¶

• Jessie2 (git clone https://forge.ispras.ru/git/astraver.jessie2.git) has the following branches:
  -- master -- references the latest released version of the Jessie2 plugin (currently `astraver-v1.1')

• QA (git clone https://forge.ispras.ru/git/astraver.qa.git) is a submodule of the Jessie2 repository. It contains several new test sets and the corresponding new testing script (in OCaml) that is based on the Why3 proof replayer.

• Frama-C (git clone https://forge.ispras.ru/git/astraver.frama-c.git) has two branches:
  -- master -- this is a dummy branch with each commit corresponding to an upstream release of Frama-C starting from "Sodium 20150201" (framac|1db5542e)
  -- 20150201 -- references patched version of Frama-C Sodium 20150201 required by the latest Jessie2 (astraver-v1.1) with some significant changes (wrap-around annotations and logic operations on bounded integers, annotation importing -- an order-independent merging of annotations from several C source files)

• Why3 (git clone https://forge.ispras.ru/git/astraver.why3.git) has two branches:
  -- master -- a periodically updated mirror of the INRIA official Why3 Git repository's master branch
  -- patched -- the periodically merged patched version of the Why3 platform with several small unmerged changes

• OPAM-repository (git clone https://forge.ispras.ru/git/astraver.opam-repository.git) is the above mentioned OPAM repository