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.

Installation

No binaries are provided at the moment. Installation must be done by either
compiling the source code or using a Docker image.

From source code

Please note: CAISAR 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

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

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 (.mlw)
can be found in the tests
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 (to be released)

• Marabou

• SAVer

Under active development is the support for the SMT-LIB which
is used by many satisfiability modulo theories solvers (e.g. Alt-Ergo,
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/.