Software Contracts for Security

Abstract

Component-based software engineering facilitates the design of complex systems by subdividing the programming task into separate components that interact via clearly defined interfaces. A component-based system is correct only when each component satisfies its specification and the interactions between different components satisfy their respective interfaces. "Design by Contract" is a programming methodology that enforces these requirements by attaching executable specifications to components. These contracts monitor the system's execution and interfere when a specification would be violated.

Designing a program this way gives assurance that the program is correct. It eliminates defensive programming by separating code that validates the correct use of a component from the component's implementation. It also simplifies debugging by localizing program errors within the component that violated its specification. However, existing work on software contracts focuses almost exclusively on contracts for functional correctness. This dissertation argues that higher-order software contracts are an effective mechanism to specify and enforce composable, easy-to-understand security properties. Whereas traditional software contracts describe what a component requires from its clients and provides in return, software contracts for security enforce limits on the contexts in which components can be used.

The first part of this dissertation shows how existing software contracts can be combined with language restrictions to write and enforce declarative security specifications. Based on this design, I develop a secure shell scripting language. The second part introduces authorization contracts, a new type of software contract that can implement a wide range of commonly used security mechanisms without requiring language modifications.