Integrating Types and Specifications for Secure Software Development

Integrating Types and Specifications for Secure Software Development
Greg Morrisett
Harvard University,
Cambridge, Massachussetts, 02138, USA
greg@eecs.harvard.edu
http://www.eecs.harvard.edu/~greg
Abstract. Today, the majority of security errors in software systems
are due to implementation errors, as opposed to flaws in fundamental
algorithms (e.g., cryptography). Type-safe languages, such as Java, help
rule out a class of these errors, such as code-injection through buffer overruns.
But attackers simply shift to implementation flaws above the level
of the primitive operations of the language (e.g., SQL-injection attacks).
Thus, next-generation languages need type systems that can express and
enforce application-specific security policies.
Keywords: dependent types, verification, software-security.

Overview
In theory, there is no difference between theory and practice. But, in
practice, there is.
Jan L. A. van de Snepscheut