AstraVer Toolset » Deductive Verification Tools for Linux Kernel

Wiki » History » Revision 3

Revision 2 (Mikhail Mandrykin, 01/13/2015 07:00 PM) → Revision 3/27 (Alexey Khoroshilov, 01/18/2015 01:30 AM)

h1. Jessie2 
  (fork of the Jessie plugin for Frama-C) 

 *Jessie2* is a fork of the Jessie plug-in that allows deductive verification of C programs annotated with "ACSL":http://frama-c.com/acsl.html and is primarily targeted at Linux kernel modules source code. It uses the language and tools of the "Why3 verification platform":http://why3.lri.fr/. Unlike    original Jessie, Jessie2 is not distributed as a part of the "Why2 verification certification platform":http://why.lri.fr/ and is compiled/installed separately. 
 *Note*: For now, this This fork requires modified version of the __Frama-C__ source code analysis platform, based on the @Neon 20140301@ version of the original platform. 

 h2. Installation 

 h3. Using OPAM 

   * Install "OPAM":https://opam.ocaml.org/ as described on 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.github.com/ocaml/opam/master/shell/opam_installer.sh 
     chmod +x opam_installer.sh 
     sudo ./opam_installer.sh /usr/local/bin 
     </code></pre> 
   * Initialize OPAM to use the OCaml 4.02.1 compiler: 
     <pre><code class="bash"> 
     opam init --comp 4.02.1 
     eval `opam config env` 
     </code></pre> 
   * Install "Git":http://git-scm.com/. 
     For example on Ubuntu: 
     <pre><code class="bash"> 
     sudo apt-get install git 
     </code></pre> 
   * Add ISPRAS ISP RAS OPAM repository at @https://forge.ispras.ru/git/astraver.opam-repository.git@ with Jessie2 and modified Frama-C Neon 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 
     </code></pre> 
   * Install external dependencies for the Jessie2 and Frama-C build i.e. Autoconf, Gtk2 development files and M4. 
     Ubuntu example: 
     <pre><code class="bash"> 
     sudo apt-get install $(opam install -e ubuntu jessie2) 
     </code></pre> 
   * 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: 
     <pre><code class="bash"> 
     opam install -j 4 jessie2 
     </code></pre> 
   * Build and install either original or patched (negative assumption highlighting and minor explanation fixes) version of the Why3 verification platform: 
     <pre><code class="bash"> 
     sudo apt-get install $(opam install -e ubuntu why3) # Install GMP (external dependency) on Ubuntu 
     opam install -j 4 why3 
     </code></pre> 
   * The one using Jessie would also likely need SMT solvers e.g. "Alt-Ergo":http://alt-ergo.ocamlpro.com/ (also "Z3":http://http://z3.codeplex.com/, "CVC4":http://cvc4.cs.nyu.edu/web/ and others). Alt-Ergo can be installed via OPAM: 
     <pre><code class="bash"> 
      opam install alt-ergo altgr-ergo satML-plugin 
     </code></pre> 
   * The Why3 IDE should be initialized to detect available provers (and plugins): 
     <pre><code class="bash"> 
     why3 config --detect-provers --detect-plugins 
     </code></pre> 

 h2. Our Repositories