package caisar

CAISAR

CAISAR (Characterizing AI Safety And Robustness) is a platform under active development at CEA LIST, aiming to provide a wide range of features to characterize the safety and robustness of artificial intelligence based software.

Getting CAISAR

The latest release of CAISAR is available as an opam package or a Docker image on GNU/Linux. CAISAR is available on Windows either under the Windows Subsystem Linux (WSL) or the aforementioned docker image.

The development version of CAISAR is available only by compiling the source code. CAISAR needs access to a python3 interpreter, which is a default in all major GNU/Linux distributions.

opam package

Please note: CAISAR requires the OCaml package manager opam, v2.1 or higher, which is typically avaible in all major GNU/Linux distributions.

To install CAISAR via opam, do the following:

opam install caisar

Docker image

A ready-to-use Docker image of CAISAR is available on Docker Hub. To retrieve such an image, do the following:

docker pull laiser/caisar:pub

Alternatively, a Docker image for CAISAR can be created locally by proceeding as follows:

git clone https://git.frama-c.com/pub/caisar
cd caisar
make docker

To run the CAISAR Docker image, do the following:

docker run -it laiser/caisar:pub sh

Nix flake

A CAISAR Nix flake allow for reproducible build, and setting up a development environment. It requires Nix version 2.15 or higher as well as enabling flakes. Please refer to the official Nix documentation to enable Nix flakes.

Assuming you have Nix installed and are at the CAISAR repository root, you can build CAISAR using the following command:

nix build

You can setup a development environment with all CAISAR dependencies included using nix develop. It will contain the ocaml toolchain already setup and installed, and the ocaml language server and formatter. You can thus compile and test CAISAR in an isolated shell using the following command:

nix develop

From source code

Please note: building CAISAR from source requires the OCaml package manager opam, v2.1 or higher, which is typically avaible in all major GNU/Linux distributions.

To build and install CAISAR, do the following:

git clone https://git.frama-c.com/pub/caisar
cd caisar
opam switch create --yes --no-install . 4.13.1
opam install . --deps-only --with-test --yes
make
make install

To run the tests:

make test

Documentation

The CAISAR user manual is available on the platform website.

It is possible to generate it locally. This operation requires the documentation generator Sphinx, which is typically avaible in all major GNU/Linux distributions.

To build the CAISAR manual, do the following:

make doc

Typically, this will produce two versions of the manual:

• HTML version, in doc/_build/html/index.html

• PDF version, in doc/_build/latex/manual.pdf

Usage

To start using CAISAR, please run the command:

caisar --help

Property verification

CAISAR can be used to verify properties on neural networks and support-vector machines (SVM).

The prototype command is:

caisar verify --prover=PROVER FILE

FILE defines the property to verify, and it must be written in the WhyML language. Examples of WhyML files (.why) can be found in the examples folder.

External provers detection

CAISAR relies on external provers to work. These must be installed first, then CAISAR must be instructed to point to their location. To do so, the path to the prover executables should appear in the environment variable PATH.

Run the following command to confirm that CAISAR detects the installed provers:

caisar config --detect

The following are the provers for which a support is provided in CAISAR:

• PyRAT

• Marabou

• nnenum

• alpha-beta-CROWN

• SAVer

Moreover, CAISAR supports the SMT-LIB format which is used by many satisfiability modulo theories solvers (e.g. Alt-Ergo, cvc5, Z3, Colibri, etc.).

Advanced usage

How to add a solver

Make sure the solver is installed in your system. Typically, the path to its executable should appear in the environment variable PATH. Then,

1. Create a solver.drv in config/drivers/. A driver is a series of WhyML modules describing the theories the solver is able to understand as provided by Why3. Directives for letting Why3 interpret the solver outputs should also be provided here.

2. Add a new record in config/caisar-detection-data.conf. The name of the solver executable should be provided , as well as a command-line template that Why3 will use for executing the solver. Such a template may specify several Why3 built-in identifiers:

   • %e stands for the executable

   • %f stands for a file to pass to the executable

Other custom identifiers have been added: %{nnet-onnx} and %{svm}. These identifiers are used for providing the solver with potential {nnet, onnx} and svm model filenames, respectively.

1. Write a Why3 printer. The solver should be recognized by CAISAR by now. However, a printer for the solver may be needed for transforming Why3 specifications into something the solver can understand. Printers should be placed in src/printers/.