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.

Conference Day
Tue 15 Jan

Displayed time zone: Belfast change

14:00 - 15:30
Research Papers: Program VerificationCPP at Sala XII
Chair(s): Nicolas TabareauInria
14:00
30m
Research paper
A Verified Protocol Buffer Compiler
CPP
Qianchuan YePurdue University, Benjamin DelawarePurdue University
DOI
14:30
30m
Research paper
A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra
CPP
Véronique BenzakenLRI, Université Paris-Sud, Evelyne Contejean
DOI
15:00
30m
Research paper
Dynamic Class Initialization Semantics: a Jinja Extension
CPP
Susannah Mansky, Elsa GunterUniversity of Illinois
DOI