Newer
Older
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.
The latest release of CAISAR is available as an [opam](https://opam.ocaml.org/)
package or a [Docker](https://www.docker.com/) image on GNU/Linux.
CAISAR is available on Windows either under the [Windows
Subsystem Linux](https://learn.microsoft.com/en-us/windows/wsl/install)
(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.
**Please note:** CAISAR requires the OCaml package manager [opam](https://opam.ocaml.org/),
v2.1 or higher, which is typically avaible in all major GNU/Linux distributions.
To install CAISAR via [opam](https://opam.ocaml.org/), do the following:
```
```
### Docker image
Michele Alberti
committed
A ready-to-use [Docker](https://www.docker.com/) image of CAISAR is available on
[Docker Hub](https://hub.docker.com). To retrieve such an image, do the
following:
```
Michele Alberti
committed
```
Alternatively, a [Docker](https://www.docker.com/) image for CAISAR can be
created locally by proceeding as follows:
git clone https://git.frama-c.com/pub/caisar
cd caisar
make docker
Michele Alberti
committed
To run the CAISAR [Docker](https://www.docker.com/) image, do the following:
```
Michele Alberti
committed
```
### 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](https://nixos.wiki/wiki/Flakes#Temporary) 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](https://nixos.org/manual/nix/stable/command-ref/new-cli/nix3-develop.html).
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
```
**Please note:** building CAISAR from source requires the OCaml package manager [opam](https://opam.ocaml.org/),
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:
```
## Documentation
The CAISAR user manual is available on the [platform website](https://caisar-platform.com/documentation/).
It is possible to generate it locally. This operation requires the documentation generator
[Sphinx](https://www.sphinx-doc.org/en/master/index.html), 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:
```
```
### Property verification
CAISAR can be used to verify properties on neural networks and support-vector
machines (SVM).
The prototype command is:
```
```
`FILE` defines the property to verify, and it must be
written in the [WhyML](https://why3.lri.fr/doc-0.80/manual004.html) language.
Examples of [WhyML](https://why3.lri.fr/doc-0.80/manual004.html) files (`.why`)
can be found in the [examples](https://git.frama-c.com/pub/caisar/-/tree/master/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:
```
```
The following are the provers for which a support is provided in CAISAR:
* [Marabou](https://github.com/NeuralNetworkVerification/Marabou)
* [nnenum](https://github.com/stanleybak/nnenum)
* [alpha-beta-CROWN](https://github.com/Verified-Intelligence/alpha-beta-CROWN)
* [SAVer](https://github.com/abstract-machine-learning/saver)
Moreover, CAISAR supports the [SMT-LIB](https://smtlib.cs.uiowa.edu/) format
which is used by many satisfiability modulo theories solvers (e.g.
[Alt-Ergo](https://alt-ergo.ocamlpro.com/), [cvc5](https://cvc5.github.io/),
[Z3](https://github.com/Z3Prover/z3/wiki),
[Colibri](https://colibri.frama-c.com/), 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/](https://git.frama-c.com/pub/caisar/-/tree/master/config/drivers).**
A driver is a series of [WhyML](https://why3.lri.fr/doc-0.80/manual004.html) modules
describing the theories the solver is able to understand as provided by [Why3](https://why3.lri.fr/).
Directives for letting [Why3](https://why3.lri.fr/) interpret the solver outputs should also be provided here.
2. **Add a new record in [config/caisar-detection-data.conf](https://git.frama-c.com/pub/caisar/-/blob/master/config/caisar-detection-data.conf).** The name of the
solver executable should be provided , as well as a command-line template that
[Why3](https://why3.lri.fr/) will use for executing the solver. Such a template may specify several
[Why3](https://why3.lri.fr/) 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.
3. **Write a [Why3](https://why3.lri.fr/) printer.** The solver should be recognized by CAISAR by
now. However, a printer for the solver may be needed for transforming [Why3](https://why3.lri.fr/)
specifications into something the solver can understand. Printers should be
placed in [src/printers/](https://git.frama-c.com/pub/caisar/-/tree/master/src/printers).