Project

General

Profile

Actions

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.

Updated by Pavel Putro 12 months ago ยท 5 revisions