package caisar
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=f41febdf9faa14c6ed1504791e7e96172997ca0bc26f421ad68a6c18893e92c4
sha512=364bc4d3a8dd7c8245ace10118c48db30a10749040bd655092e79c323c10bcdfc660a9b687335800988da0308d5fa1f1a8cb822eb8bcf857092e583bf94cce4d
Description
Published: 14 Jul 2022
README
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.
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:
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,
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.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.
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/.
Dependencies (22)
-
caisar-onnx
= version
-
caisar-ovo
= version
-
caisar-nnet
= version
-
re
>= "1.10.4" & < "1.12.0"
-
why3
>= "1.5.0" & < "1.6~"
-
csv
>= "2.4"
-
ppx_deriving_yojson
>= "3.6.1"
-
menhirLib
>= "20210310"
-
yojson
>= "1.7.0"
-
ppx_deriving
>= "5.1"
-
logs
>= "0.7.0"
-
fmt
>= "0.8.9"
-
cmdliner
>= "1.1.1"
-
stdio
>= "v0.14.0"
-
base
>= "v0.14.0" & < "v0.17"
-
ocplib-endian
>= "1.0"
-
zarith
>= "1.7"
-
piqilib
>= "0.6.14"
-
piqi
>= "0.7.6"
-
dune-site
>= "2.9.0"
-
ocaml
>= "4.13"
-
dune
>= "2.9"
Dev Dependencies (1)
-
odoc
with-doc
Used by
None
Conflicts
None