Abstract: “In this thesis, I propose a methodology for supporting the development of software that depends on parsers—such as anything connected to the Internet—to safely support any reasonably designed protocol: data structures to describe protocol messages; validation routines that check that data received from the wire conforms to the rules of the protocol; systems that allow a defender to inject arbitrary, crafted input so as to explore the effectiveness of the parser; and systems that allow for the observation of the parser code while it is being explored.
Then, I describe principled method of producing parsers that automatically generates the myriad parser-related software from a description of the protocol. This has many significant benefits: it makes implementing parsers simpler, easier, and faster; it reduces the trusted computing base to the description of the protocol and the program that compiles the description to runnable code; and it allows for easier formal verification of the generated code.
I demonstrate the merits of the proposed methodology by creating a description of the USB protocol using a domain-specific language (DSL) embedded in Haskell and integrating it with the FreeBSD operating system. Using the industry-standard umap test-suite, I measure the performance and efficacy of the generated parser. I show that it is stable, that it is effective at protecting a system from both accidentally and maliciously malformed input, and that it does not incur unreasonable overhead.”
Actually, the formal methods tag was wrong here: it doesn’t use formal methods. What I saw skimming it was that author wanted to do that later. It’s metaprogramming designed for easy verification with testing to confirm it works. To bad there’s not a suggest button for my own story to use when edit disappears. ;)
Also, after reading it, the author was talking about formally verifying the code that’s generated in a style like seL4. That might not be necessary given the verified meta-programming stuff I’ve been submitting. One might just prove the transformation primitives and their compositions correct. The author already builds types that are C compatible from what I saw in the code examples. The control flow can be made easy for mechanical verification if it isn’t easy enough already. I think verified meta-stages shouldn’t introduce much if any error past what developer already has in the specification. The specifications themselves are also highly intuitive and small. That should reduce those errors.