AstraVer Toolset » Deductive Verification Tools for Linux Kernel

h1. AstraVer Toolset

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

*AstraVer* is a successor of the "Jessie":http://krakatoa.lri.fr/ plug-in for "Frama-C":http://www.frama-c.com/ that allows deductive verification of C programs annotated with "ACSL":http://frama-c.com/acsl.html and is primarily targeted at source code of Linux kernel modules. It uses the language and tools of the "Why3 verification platform":http://why3.lri.fr/. Unlike Jessie, AstraVer is not distributed as part of the "Why2 verification platform":http://why.lri.fr/ and is compiled/installed separately.

*Note*: This fork requires modified version of the __Frama-C__ source code analysis platform, that is based on the @Argon (18.0)@ version of the original platform. The modifications don't affect other plugins. Thus WP, EVA, RTE of this forked version can be used the same way as in vanilla version. If it is required to keep 2 versions of Frama-C (the original one and this one) different switches can be used.

h2. Installation

h3. Using OPAM

  * Install recommended OPAM external (system) dependencies — @gcc@, @m4@, @make@, @git@. For example, on Ubuntu:

    <pre><code class="bash">

    sudo apt-get install gcc m4 make git

    </code></pre>

  * Install "OPAM":https://opam.ocaml.org/ as described in the OPAM "documentation":https://opam.ocaml.org/doc/Install.html.

    For example (installing to @/usr/local/bin@ unsing the binary installer):

    <pre><code class="bash">

    wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh

    sh install.sh

    </code></pre>

  * Initialize OPAM to use the OCaml @4.07.1@ compiler. On Ubuntu you can use @--disable-sandboxing@ to avoid installation of "bubblewrap":https://github.com/projectatomic/bubblewrap, although this is not recommended.

    <pre><code class="bash">

    opam init -c 4.07.1 --disable-sandboxing

    </code></pre>

  * Configure current shell environment to use the newly created OPAM switch (may not be needed if OPAM shell hooks were installed successfully during @opam init@):

    <pre><code class="bash">

    eval $(opam env)

    </code></pre>

  * Add ISPRAS OPAM repository at @https://forge.ispras.ru/git/astraver.opam-repository.git@ with AstraVer and modified Frama-C v18.0 packages to the OPAM installation

    (@ispras@ is just an arbitrary name of the new repository):

    <pre><code class="bash">

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

    opam update

    </code></pre>

  * Install OPAM @depext@ plug-in for easy extraction and installation of external (system) dependencies for OPAM packages:

    <pre><code class="bash">

    opam install depext

    </code></pre>

  * Install external dependencies for the AstraVer and Frama-C build e. g. Gtk2 development files:

    <pre><code class="bash">

    opam depext astraver

    </code></pre>

  * Build and install the AstraVer plugin for Frama-C with OPAM (the patched versions of Frama-C and Why3 platforms will be built and installed automatically).

    <pre><code class="bash">

    opam install astraver

    </code></pre>

  * The one using AstraVer would also likely need SMT solvers e.g. "Alt-Ergo":http://alt-ergo.ocamlpro.com/ (also "Z3":https://github.com/Z3Prover/z3, "CVC4":http://cvc4.cs.stanford.edu/web/ and others). Alt-Ergo can be installed via OPAM:

    <pre><code class="bash">

     opam install alt-ergo altgr-ergo

    </code></pre>

  * The Why3 IDE should be configured to detect available provers (and plugins):

    <pre><code class="bash">

    why3 config --detect

    </code></pre>

h2. Our Repositories

  * "AstraVer":/projects/astraver/repository (@git clone https://forge.ispras.ru/git/astraver.git@) has the following branches:

    -- "@18.0@":/projects/astraver/repository/ -- references the latest released version of the AstraVer plugin

  * "QA":/projects/astraver/repository/qa (@git clone https://forge.ispras.ru/git/astraver.qa.git@) is a submodule of the "AstraVer":/projects/astraver/repository repository. It contains several new test sets and the corresponding new testing script (in OCaml) that is based on the "Why3 proof replayer":http://why3.lri.fr/doc/manpages.html#sec62.

  * "Frama-C":/projects/astraver/repository/framac (@git clone https://forge.ispras.ru/git/astraver.frama-c.git@) has two branches:

    -- "@master@":/projects/astraver/repository/framac -- this is a dummy branch with each commit corresponding to an upstream release of Frama-C starting from "@Sodium 20150201@" (commit:framac|1db5542e)

    -- "@18.0@":/projects/astraver/repository/framac?utf8=✓&rev=18.0 -- references patched version of Frama-C @Argon v18.0@ required by the latest AstraVer 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":/projects/astraver/repository/why3 (@git clone https://forge.ispras.ru/git/astraver.why3.git@) has two branches:

    -- "@master@":/projects/astraver/repository/why3 -- a periodically updated mirror of the INRIA official Why3 Git repository's "master branch":https://gitlab.inria.fr/why3/why3

    -- "@bv_and_lemma_functions_stable-4.07@":/projects/astraver/repository/why3?utf8=✓&rev=bv_and_lemma_functions_stable-4.07 -- patched version of the Why3 platform (version 0.87.3) with several small unmerged changes

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