Biblio

For over two decades the OpenPGP format has provided the mainstay of email confidentiality and authenticity, and is currently being relied upon to provide authenticated package distributions in open source Unix systems. In this work, we provide the first language theoretical analysis of the OpenPGP format, classifying it as a deterministic context free language and establishing that an automatically generated parser can in principle be defined. However, we show that the number of rules required to describe it with a deterministic context free grammar is prohibitively high, and we identify security vulnerabilities in the OpenPGP format specification. We identify possible attacks aimed at tampering with messages and certificates while retaining their syntactical and semantical validity. We evaluate the effectiveness of these attacks against the two OpenPGP implementations covering the overwhelming majority of uses, i.e., the GNU Privacy Guard (GPG) and Symantec PGP. The results of the evaluation show that both implementations turn out not to be vulnerable due to conser- vative choices in dealing with malicious input data. Finally, we provide guidelines to improve the OpenPGP specification

Programming languages have long incorporated type safety, increasing their level of abstraction and thus aiding programmers. Type safety eliminates whole classes of security-sensitive bugs, replacing the tedious and error-prone search for such bugs in each application with verifying the correctness of the type system. Despite their benefits, these protections often end at the process boundary, that is, type safety holds within a program but usually not to the file system or communication with other programs. Existing operating system approaches to bridge this gap require the use of a single programming language or common language runtime. We describe the deep integration of type safety in Ethos, a clean-slate operating system which requires that all program input and output satisfy a recognizer before applications are permitted to further process it. Ethos types are multilingual and runtime-agnostic, and each has an automatically generated unique type identifier. Ethos bridges the type-safety gap between programs by (1) providing a convenient mechanism for specifying the types each program may produce or consume, (2) ensuring that each type has a single, distributed-system-wide recognizer implementation, and (3) inescapably enforcing these type constraints.