Copyright (C) 2022
This software is licensed under a dual BSD and GPL v2 license. See LICENSE file at the root folder of the project.
- Arnaud EBALARD (mailto:arnaud.ebalard@ssi.gouv.fr)
- Ryad BENADJILA (mailto:ryad.benadjila@ssi.gouv.fr)
- Patricia MOUY (mailto:patricia.mouy@ssi.gouv.fr)
This software implements a X.509 certificate parser, annotated using ACSL annotations for verification with Frama-C (version 18/Argon).
The main Makefile is in the root directory, and compiling is as simple as executing:
$ make
This will compile different elements in the build directory:
- the x509-parser.o object file
- the x509-parser binary, which can be used on a DER certificate (or a concatenation of such elements)
The main Makefile has targets to run several static analyzers.
To verify the project with Frama-C, use the frama-c
target:
$ make frama-c
Frama-C must have been installed prior to calling that target. Installing Frama-C can be done using OPAM. More details can be found on Frama-C project website. Frama-C may also be available as a common package on your distribution.
To verify the project with IKOS, use the
ikos
target:
$ make ikos
IKOS must have been installed prior to calling that target. See the installation instructions.