Biblio

Researchers interested in security often wish to introduce new primitives into a language. Extensible languages hold promise in such scenarios, but only if the extension mechanism is sufficiently safe and expressive. This paper describes several modifications to an extensible language motivated by end-to-end security concerns.

Web applications must ultimately command systems like web browsers and database engines using strings. Strings derived from improperly sanitized user input can thus be a vector for command injection attacks. In this paper, we introduce regular string types, which classify strings known statically to be in a specified regular language. These types come equipped with common operations like concatenation, substitution and coercion, so they can be used to implement, in a conventional manner, the portions of a web application or application framework that must directly construct com- mand strings. Simple type annotations at key interfaces can be used to statically verify that sanitization has been per- formed correctly without introducing redundant run-time checks. We specify this type system in a minimal typed lambda calculus, λRS.

To be practical, adopting a specialized type system like this should not require the adoption of a new programming language. Instead, we advocate for extensible type systems: new type system fragments like this should be implemented as libraries atop a mechanism that guarantees that they can be safely composed. We support this with two contribu- tions. First, we specify a translation from λRS to a language fragment containing only standard strings and regular ex- pressions. Second, taking Python as a language with these constructs, we implement the type system together with the translation as a library using atlang, an extensible static type system for Python being developed by the authors.