Cryptographic Protocol Logic Fuzz Testing – ProtoFuzz

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.