ANSSI x509 cert parser

This is a fantastic piece of software:

Arnaud Ebalard. x509-parser: a RTE-free X.509 parser. https://github.com/ANSSI-FR/x509-parser

This implements a X.509 parser, with profuse ACSL annotations so that the whole parser is verifiable with frama-c

• This guarantees the parser is free from run-time errors: invalid memory accesses, signed integer overflows, undefined behavior)
• It is suitable for embedded devices (no malloc, no floats, no dependencies)
• The current ACSL annotations cannot prove the code adheres to some specification (correctness) but nevertheless it’s a great piece of engineering
• It is a good resource to learn frama-c and ACSL in a non-trivial project.

This is an excerpt from the paper:

References:

• Arnaud Ebalard, Patricia Mouy, and Ryad Benadjila. Journey to a RTE-free X.509 parser. pretty didactical paper: https://www.sstic.org/media/SSTIC2019/SSTIC-actes/journey-to-a-rte-free-x509-parser/SSTIC2019-Article-journey-to-a-rte-free-x509-parser-ebalard_mouy_benadjila_3cUxSCv.pdf
• Presentation slides: https://www.sstic.org/media/SSTIC2019/SSTIC-actes/journey-to-a-rte-free-x509-parser/SSTIC2019-Slides-journey-to-a-rte-free-x509-parser-ebalard_mouy_benadjila.pdf
• Presentation at SSTIC 2019, with video (in french) https://www.sstic.org/2019/presentation/journey-to-a-rte-free-x509-parser/
• Code: https://github.com/ANSSI-FR/x509-parser

Related:

• Paper: https://iacr.org/submit/files/slides/2023/rwc/rwc2023/46/slides.pdf

Other projects from ANSSI:

• libdrbg (no frama-c verification) https://github.com/ANSSI-FR/libdrbg
• libecc (well engineered) https://github.com/libecc/libecc