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:[email protected])

• Ryad BENADJILA (mailto:[email protected])
• Patricia MOUY (mailto:[email protected])

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.