Generating Optimised and Formally Checked Packet Parsing Code

Abstract : While implementing distributed applications, the parsing of binary packets is a very difficult and error-prone task the developer has to face. Moreover, these programming mistakes are often the source of distant vulnerabilities. In this paper we present a code-generation library, called Promiwag, for creating optimised and safe packet parsing code. Its input is concise human-readable descriptions of the protocols and the interests of the application in specific pieces of information. Promiwag follows a dependency-based algorithm, and uses high-level optimisation techniques to generate minimal parsing automatons. These automatons can be compiled into C or OCaml code for efficient execution, and to annotatedWhy code. This latter output is then used to automatically prove that for any possible input packet, the generated code cannot perform any illegal memory access, and that no infinite loop can be triggered. We have used our code generator to implement a pretty-printer for Internet protocols, and we provide experimental results on the performance of the generated code.
Document type :
Conference papers
Jan Camenisch; Simone Fischer-Hübner; Yuko Murayama; Armand Portmann; Carlos Rieder. 26th International Information Security Conference (SEC), Jun 2011, Lucerne, Switzerland. Springer, IFIP Advances in Information and Communication Technology, AICT-354, pp.173-184, 2011, Future Challenges in Security and Privacy for Academia and Industry. 〈10.1007/978-3-642-21424-0_14〉
Liste complète des métadonnées

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-01567597
Contributor : Hal Ifip <>
Submitted on : Monday, July 24, 2017 - 10:40:18 AM
Last modification on : Monday, July 24, 2017 - 10:42:15 AM

File

978-3-642-21424-0_14_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Sebastien Mondet, Ion Alberdi, Thomas Plagemann. Generating Optimised and Formally Checked Packet Parsing Code. Jan Camenisch; Simone Fischer-Hübner; Yuko Murayama; Armand Portmann; Carlos Rieder. 26th International Information Security Conference (SEC), Jun 2011, Lucerne, Switzerland. Springer, IFIP Advances in Information and Communication Technology, AICT-354, pp.173-184, 2011, Future Challenges in Security and Privacy for Academia and Industry. 〈10.1007/978-3-642-21424-0_14〉. 〈hal-01567597〉

Share

Metrics

Record views

15

Document downloads

4