CE48 - Fondements du numérique : informatique, automatique, traitement du signal

Cryptographic Protocol Logic Fuzz Testing – ProtoFuzz

Submission summary

Today's information society crucially relies on cryptographic protocols, which are distributed programs that leverage cryptographic primitives to achieve various security goals such as confidentiality or integrity. Any attack in these protocols can have dramatic consequences, amplified by their ubiquity and our dependence on them for example in finance, business, and communication. Yet, critical and widely used protocol designs and implementations have been repeatedly found to be vulnerable to protocol logic attacks. At the design level, these attacks can be found and fixed by formal methods such as symbolic verification. However, those methods provide no guarantee on implementations, which are the end products that must be secure. Testing, especially fuzzing operates on implementations and has been very successful at finding low-level flaws but is unable to capture logical attacks. Therefore, effective techniques to preclude logical attacks from protocol implementations are desperately lacking.

To fill this gap, we will develop the foundations, the design, and the implementation of an innovative hybrid, synergetic framework combining symbolic verification and fuzzing. In particular, we will:
(a) devise a simple protocol language and model extractor that enable extracting formal models from lightly annotated implementations and then refining those models based on functional correctness counter-
examples and
(b) develop a novel testing methodology, symbolic-model-guided fuzzing, that, assisted by symbolic verifiers, efficiently captures logical attacks. The former will leverage a novel hybrid framework where symbolic formal models and implementations are tied together and can animate each other via dual executions.

This project's ambitions are to significantly advance fuzzing and to establish hybrid frameworks combining fuzzing and symbolic verification as a new research topic, as well as to attack and improve the security of real-world cryptographic protocols.

Project coordination

Lucca Hirschi (Centre de Recherche Inria Nancy - Grand Est)

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.


Centre de Recherche Inria Nancy - Grand Est

Help of the ANR 280,805 euros
Beginning and duration of the scientific project: March 2023 - 36 Months

Useful links

Explorez notre base de projets financés



ANR makes available its datasets on funded projects, click here to find more.

Sign up for the latest news:
Subscribe to our newsletter