Skip to content

Latest commit

 

History

History
75 lines (59 loc) · 2.8 KB

klever_bridge.md

File metadata and controls

75 lines (59 loc) · 2.8 KB
Raw

Klever bridge

This component allows to export results of Klever verification system into CV format for their visualization.

Here we use the following Klever terminology:

  • Verification task is a C file with a given entry point a set of error locations and configuration. Klever creates verification tasks based on a given Linux kernel module and checked properties (for example, memory safety).
  • Verification backend (for example, CPAchecker) solves a given task and provides verification result.
  • Verification result is:
    • a correctness witness (proof that error location cannot be reached from a given entry point) or
    • a set of violation witnesses (paths in source code from an entry point to an error location) or
    • a reason of incorrect verifier termination (may be along with violation witnesses).
  • Job is a set of solved verification tasks, grouped by some attributes.
  • Build base - source code of Linux kernel, which was prepared by Clade tool.

Klever bridge finds all solved verification tasks for a given job and export them for visualization.

Installation of Klever bridge

CVV web-interface should be deployed according to its instructions.

make install-klever-bridge DEPLOY_DIR=<path to deploy directory>

Usage

Create a configuration file klever.json in <deploy directory> with the following content:

{
  "Benchmark Launcher": {
    "tool": "CPAchecker",
    "job id": "<job id>",
    "output dir": "<path to directory with Klever solved tasks>",
    "tasks dir": "<path to directory with build base>/Storage/"
  },
  "uploader": {
    "upload results": true,
    "parent id": true,
    "identifier": "<parent report identifier>",
    "server": "<host>:<port>",
    "user": "<user name>",
    "password": "<user password>",
    "name": "<new report name>"
  }
}

Then launch the following command:

./scripts/bridge.py -c klever.json

Klever runner

Klever runner allows to create a build base for a Linux kernel, then to launch Klever and at last export results with Klever Bridge. You can find example of configuration files in configs/bridge directory. In order to launch a Klever runner from <deploy directory> run the following content:

sudo ./scripts/runner.py -c runner.json -d <path to Linux kernel>

Klever config

Klever job configuration should specify Keep intermediate files inside the working directory of Klever Core inside Other settings section in order to visualize generated files in the error trace.

If you need to visualise correctness witnesses in CV, the following options are required:

{"-setprop": "cpa.arg.proofWitness=witness.correctness.graphml"},
{"-setprop": "cpa.arg.export=true"},
{"-setprop": "cpa.arg.compressWitness=false"}