MicroVer¶

This tool is built on composition of MicroTESK tool and AstraVer versions of Frama-C and Why3 tools. The main purpose is deductive verification of the machine code by high-level language function contract specification.

Installation¶

This instruction uses RISC-V as example of target processor.

1. First, install MicroTesk (version from branch mir) tool using instruction [[https://forge.ispras.ru/projects/microtesk/wiki/Installation_Guide]] . Pay attention for setting up $MICROTESK_HOME environment variable and installing cvc4 1.6 smt-solver;
2. Download or clone RISC-V nml model from this repository [[https://forge.ispras.ru/projects/microtesk-riscv]]. Then compile and generate it using MicroTESK (see instruction above);
3. Add cvc4 to your $PATH;
4. Next, install AstraVer toolset using instruction [[https://forge.ispras.ru/projects/astraver/wiki]] . Following this instruction you will also install opam than would be used for installing other dependences;
5. Install grep:
   sudo apt-get install grep
6. Install readelf:
   sudo apt-get install binutils
7. Install Yojson :
   opam install Yojson
8. Install ocaml-containers :
   opam install containters
9. Optional install gcc for riscv form this repository: https://github.com/riscv/riscv-gnu-toolchain;
10. Next download source code of MicroVer modules:
    git clone https://forge.ispras.ru/git/microver.git
11. Use make for compiling source code;
12. Use make install for installing machine code specific Why3 modules, theories and drivers.

Running¶

• Use run.sh script for verification of the machine code.
  Script usage is .\run.sh model_id file_name.elf file_name.c func_name where:
  model_id is riscv
  file_name.elf - address of executable file that contains target machine code
  file_name.c - C file that contains C code + ACSL specification of the verification object
  func_name - name of the target function.

• Use run-reuse.sh script for reusing results of the previous run.
  Script usage is .\run-reuse.sh model_id func_name where:
  model_id is riscv
  func_name - name of the target function

Tests¶

Tests are placed into the "microver/tests" directory. File test.c contains some common functions, that can be used for running the system. File riscv.elf compiled from the test.c using gcc for RISC-V. For example you can run this:

for verification on abs function:
./run.sh riscv tests/riscv.elf tests/test.c abs_1

for verification on function with loop:
./run.sh riscv tests/riscv.elf tests/test.c x2

Results¶

1. The run.sh script creates a build dirrectory called "build_<func_name>". This dirrectory contains:
2. <func_name>.bin - function machine code
3. <func_name>.s - disassembled function
4. <func_name>.bin.json - function CFG
5. <func_name>.bin.smt2 - old version of smt-lib machine code representation
6. <func_name>.bin.bb_<x>.smt2 - smt-lib representation of function basic blocks
7. _current_machine.json - information about target architecture
8. Theory.mlw - WhyML representation of function specification
9. WP_parameter_<func_name>.smt2 - smt-lib representation of function specification
10. fun_info.json - information for merging representations
11. session.json - information about stack and positions of the local variables in machine code.
12. <func_name>_merged - targets for solving, verdicts and counterexamples if possible.