Deployment

Klever does not support standard deployment means because it consists of several components that may require complicating setup, e.g. configuring and running a web service with a database access, running system services that perform some preliminary actions with superuser rights, etc. Also, Klever will likely always require several specific addons that can not be deployed in a normal way. Please, be ready to spend quite much time if you follow this instruction first time.

Hardware Requirements

We recommend following hardware to run Klever:

  • x86-64 CPU with 4 cores
  • 16 GB of memory
  • 100 GB of free disk space

We do not guarantee that Klever will operate well if you will use less powerful machines. Increasing specified hardware characteristics in 2-4 times can reduce total verification time very considerably. To generate Klever Build Bases for large programs, such as the Linux kernel, you need 3-5 times more free disk space.

Software Requirements

Klever deployment is designed to work on Debian 9, Ubuntu 18.04 and Fedora 32. You can try it for other versions of these distributions, as well as for their derivatives on your own risk.

To deploy Klever one has to clone its Git repository (a path to a directory where it is cloned is referred to as $KLEVER_SRC):

git clone --recursive https://forge.ispras.ru/git/klever.git

Note

Alternatively one can use https://github.com/ldv-klever/klever.git.

Then you need to install all required dependencies.

First of all it is necessary to install packages listed at the following files:

  • Debian - klever/deploys/conf/debian-packages.txt from $KLEVER_SRC.
  • Fedora - klever/deploys/conf/fedora-packages.txt from $KLEVER_SRC.

Then you need to install Python 3.7 or higher and a corresponding development package. If your distribution does not have them you can get them from:

To install required Python packages we recommend to create a virtual environment using installed Python. For instance, you can run following commands within $KLEVER_SRC:

$ /usr/local/python3-klever/bin/python3 -m venv venv
$ source venv/bin/activate

To avoid some unpleasant issues during installation we recommend to upgrade PIP and associated packages:

$ pip install --upgrade pip wheel setuptools

Note

Later we assume that you are using the Klever Python virtual environment created in the way described above.

Then you need to install Python packages including the Klever one:

  • For production use it is necessary to run the following command within $KLEVER_SRC:

    $ pip install -r requirements.txt .

    Later to upgrade the Klever Python package you should run:

    $ pip install --upgrade -r requirements.txt .

  • If one is going to develop Klever one should install Klever Python package in the editable mode (with flag -e). To do it, run the following command within $KLEVER_SRC:

    $ pip install -r requirements.txt -e .

    In this case the Klever Python package will be updated automatically, but you may still need to upgrade its dependencies by running the following command:

    $ pip install --upgrade -r requirements.txt -e .

Note

Removing -r requirements.txt from the command will install latest versions of required packages. However, it is not guaranteed that they will work well with Klever.

Then one has to get Klever Addons and Klever Build Bases. Both of them should be described appropriately within Deployment Configuration File.

Note

You can omit getting Klever Addons if you will use default Deployment Configuration File since it contains URLs for all required Klever Addons.

Klever Addons

You can provide Klever Addons in various forms:

  • Local files, directories, archives or Git repositories.
  • Remote files, archives or Git repositories.

Deployment scripts will take care of their appropriate extracting. If Klever Addons are provided locally the best place for them is directory addons within $KLEVER_SRC (see Structure of Klever Git Repository).

Note

Git does not track addons from $KLEVER_SRC.

Klever Addons include the following:

CIF

One can download CIF binaries from here. These binaries are compatible with various Linux distributions since CIF is based on GCC that has few dependencies. Besides, one can clone CIF Git repository and build CIF from source using corresponding instructions.

Frama-C (CIL)

You can get Frama-C (CIL) binaries from here. As well, you can build it from this source (branch 18.0) which has several specific patches relatively to the mainline.

Consul

One can download appropriate Consul binaries from here. We are successfully using version 0.9.2 but newer versions can be fine as well. It is possible to build Consul from source.

Verification Backends

You need at least one tool that will perform actual verification of your software. These tools are referred to as Verification Backends. As verification backends Klever supports CPAchecker well. Some other verification backends are supported experimentally and currently we do not recommend to use them. You can download binaries of CPAchecker from here. In addition, you can clone CPAchecker Git or Subversion repository and build other versions of CPAchecker from source referring corresponding instructions.

Optional Addons

If you are going to solve verification tasks using VerifierCloud, you should get an appropriate client. Most likely one can use the client from the CPAchecker verification backend.

Note

For using VerifierCloud you need appropriate credentials. But anyway it is an optional addon, one is able to use Klever without it.

Klever Build Bases

In addition to Klever Addons one should provide Klever Build Bases obtained for software to be verified. Klever Build Bases should be obtained using Clade. All Klever Build Bases should be provided as directories, archives or links to remote archives. The best place for Klever Build Bases is the directory build bases within $KLEVER_SRC (see Structure of Klever Git Repository).

Note

Git does not track build bases from $KLEVER_SRC.

Note

Content of Klever Build Bases is not modified during verification.

Deployment Configuration File

After getting Klever Addons and Klever Build Bases one needs to describe them within Deployment Configuration File. By default deployment scripts use klever/deploys/conf/klever.json from $KLEVER_SRC. We recommend to copy this file somewhere and adjust it appropriately.

There are 2 pairs within Deployment Configuration File with names Klever Addons and Klever Build Bases. The first one is a JSON object where each pair represents a name of a particular Klever addon and its description as a JSON object. There is the only exception. Within Klever Addons there is Verification Backends that serves for describing Verification Backends.

Each JSON object that describes a Klever addon should always have values for version and path:

  • Version gives a very important knowledge for deployment scripts. Depending on values of this pair they behave appropriately. When entities are represented as files, directories or archives deployment scripts remember versions of installed/updated entities. So, later they update these entities just when their versions change. For Git repositories versions can be anything suitable for a Git checkout, e.g. appropriate Git branches, tags or commits. In this case deployment scripts checkout specified versions first. Also, they clone or clean up Git repositories before checkouting, so, all uncommited changes will be ignored. To bypass Git checkouting and clean up you can specify version CURRENT. In this case Git repositories are treated like directories.
  • Path sets either a path relative to $KLEVER_SRC or an absolute path to entity (binaries, source files, configurations, etc.) or an entity URL.

For some Klever Addons it could be necessary to additionally specify executable path or/and python path within path if binaries or Python packages are not available directly from path. For Verification Backends there is also name with value CPAchecker. Keep this pair for all specified Verification Backends.

Besides, you can set copy .git directory and allow use local Git repository to True. In the former case deployment scripts will copy directory .git if one provides Klever Addons as Git repositories. In the latter case deployment scripts will use specified Git repositories for cleaning up and checkouting required versions straightforwardly without cloning them to temporary directories.

Warning

Setting allow use local Git repository to True will result in removing all your uncommited changes! Besides, ignore rules from, say, .gitignore will be ignored and corresponding files and directories will be removed!

Klever Build Bases is a JSON object where each pair represents a name of a particular Build Base and its description as a JSON object. Each such JSON object should always have some value for path: it should be either an absolute path to the directory that directly contains Build Base, or an absolute path to the archive with a Build Base, or a link to the remote archive with a Build Base. Particular structure of directories inside such archive doesn’t matter: it is only required that there should be a single valid Build Base somewhere inside. In job.json you should specify the name of the Build Base.

Note

You can prepare multiple deployment configuration files, but be careful when using them to avoid unexpected results due to tricky intermixes.

Note

Actually there may be more Klever Addons or Klever Build Bases within corresponding locations. Deployment scripts will consider just described ones.

Structure of Klever Git Repository

After getting Klever Addons and Klever Build Bases the Klever Git repository can look as follows:

$KLEVER_SRC
├── addons
│   ├── cif-1517e57.tar.xz
│   ├── consul
│   ├── CPAchecker-1.6.1-svn ea117e2ecf-unix.tar.gz
│   ├── CPAchecker-35003.tar.xz
│   ├── toplevel.opt.tar.xz
│   └── ...
├── build bases
│   ├── linux-3.14.79.tar.xz
│   └── linux-4.2.6
│       ├── allmodconfig
│       └── defconfig
└── ...

Deployment Variants

There are several variants for deploying Klever: