Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 14:00 - 14:30 at Sala XII - Research Papers: Program Verification Chair(s): Nicolas Tabareau

The code responsible for serializing and deserializing untrusted external data is a vital component of any software that communicates with the outside world, as any bugs in these components represent a key attack vector for remote attackers. This situation is particularly acute for verified systems, where any defects in the parsing code can invalidate any formal proofs about the system. One way to reduce the trusted code base of these systems is to use interface generators like Protocol Buffer and ASN.1 to generate serializers and deserializers from data descriptors. Of course, these generators are not immune from bugs.

In this work, we formally verify a compiler for a realistic subset of the popular Protocol Buffer serialization format using the Coq proof assistant, proving once and for all the correctness of every generated serializer and deserializer. One of the challenges we had to overcome was the extreme flexibility of the Protocol Buffer format: the same source data can be encoded in an infinite number of ways, and the deserializer must faithfully recover the original source value from each. We have validated our verified system using the official conformance tests.

Tue 15 Jan

14:00 - 15:30: CPP 2019 - Research Papers: Program Verification at Sala XII
Chair(s): Nicolas TabareauInria
CPP-201914:00 - 14:30
Research paper
Qianchuan YePurdue University, Benjamin DelawarePurdue University
CPP-201914:30 - 15:00
Research paper
Véronique BenzakenLRI, Université Paris-Sud, Evelyne Contejean
CPP-201915:00 - 15:30
Research paper
Susannah Mansky, Elsa GunterUniversity of Illinois