NDLI: The Pitfalls of Protocol Design: Attempting to Write a Formally Verified PDF Parser

Content Provider	IEEE Xplore Digital Library
Author	Bogk, A. Schopl, M.
Copyright Year	2014
Description	Author affiliation: Principal Security Architect, HERE, Berlin, Germany (Bogk, A.) \|\| Inst. fur Inf. Humboldt-Univ. Berlin, Berlin, Germany (Schopl, M.)
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.
Starting Page	198
Ending Page	203
File Size	304178
Page Count	6
File Format	PDF
ISBN	9781479951031
DOI	10.1109/SPW.2014.36
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2014-05-17
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Privacy Writing Syntactics Portable document format Software Security Indexes
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

The pitfalls of protocol design Attempting to write a formally verified PDF parser

Masquerading as a Trustworthy Entity through Portable Document File (PDF) Format

Invisible Communication through Portable Document File (PDF) Format

Portable document format (pdf) security analysis and malware threats.

Privacy-Preserving Detection of Plagiarism in Scientific Documents

The TUG’2001 Portable Document Format (PDF)

Hiding new words in a PDF document

Portable Document Format (PDF): Standardizing Document Files for Publication

Portable Document Format (PDF) Security Analysis and Malware Threats

The Pitfalls of Protocol Design: Attempting to Write a Formally Verified PDF Parser

Similar Documents

The pitfalls of protocol design Attempting to write a formally verified PDF parser

Masquerading as a Trustworthy Entity through Portable Document File (PDF) Format

Invisible Communication through Portable Document File (PDF) Format

Portable document format (pdf) security analysis and malware threats.

Privacy-Preserving Detection of Plagiarism in Scientific Documents

The TUG’2001 Portable Document Format (PDF)

Hiding new words in a PDF document

Portable Document Format (PDF): Standardizing Document Files for Publication

Portable Document Format (PDF) Security Analysis and Malware Threats

The Pitfalls of Protocol Design: Attempting to Write a Formally Verified PDF Parser