DocumentCode :
154268
Title :
The Pitfalls of Protocol Design: Attempting to Write a Formally Verified PDF Parser
Author :
Bogk, Andreas ; Schopl, Marco
Author_Institution :
Principal Security Architect, HERE, Berlin, Germany
fYear :
2014
fDate :
17-18 May 2014
Firstpage :
198
Lastpage :
203
Abstract :
Parsers for complex data formats generally present a big attack surface for input-driven exploitation. In practice, this has been especially true for implementations of the PDF data format, as witnessed by dozens of known vulnerabilities exploited in many real world attacks, with the Acrobat Reader implementation being the main target. In this report, we describe our attempts to use Coq, a theorem prover based on a functional programming language making use of dependent types and the Curry-Howard isomorphism, to implement a formally verified PDF parser. We ended up implementing a subset of the PDF format and proving termination of the combinator-based parser. Noteworthy results include a dependent type representing a list of strictly monotonically decreasing length of remaining symbols to parse, which allowed us to show termination of parser combinators. Also, difficulties showing termination of parsing some features of the PDF format readily translated into denial of service attacks against existing PDF parsers-we came up with a single PDF file that made all the existing PDF implementations we could test enter an endless loop.
Keywords :
document handling; functional programming; grammars; security of data; theorem proving; Acrobat Reader implementation; Coq; Curry-Howard isomorphism; PDF data format; combinator-based parser; complex data formats; denial of service attacks; formally verified PDF parser; functional programming language; input-driven exploitation; parser combinators; protocol design; theorem prover; Indexes; Portable document format; Privacy; Security; Software; Syntactics; Writing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Security and Privacy Workshops (SPW), 2014 IEEE
Conference_Location :
San Jose, CA
Type :
conf
DOI :
10.1109/SPW.2014.36
Filename :
6957304
Link To Document :
بازگشت