Program Synthesis for Interactive-Security Systems
William R. Harris, Somesh Jha, Thomas W. Reps, and Sanjit A. Seshia
Developing practical but secure programs remains an important and
open problem.
Recently, the operating-system and architecture communities have
proposed novel systems, which we refer to as
interactive-security systems.
They provide primitives that a program can use to perform
security-critical operations, such as reading from and writing to
system storage by restricting some modules to execute with limited
privileges.
Developing programs that use the low-level primitives provided by such
systems to correctly ensure end-to-end security guarantees while
preserving intended functionality is a challenging problem.
This paper describes previous and proposed work on techniques and
tools that enable a programmer to generate programs automatically
that use such primitives.
For two interactive security systems, namely the Capsicum capability
system and the HiStar information-flow system, we developed languages
of policies that a programmer can use to directly express security and
functionality requirements, along with synthesizers that take a
program and policy in the language and generate a program that
correctly uses system primitives to satisfy the policy.
We propose future work on developing a similar synthesizer for novel
architectures that enable an application to execute different modules
in Secure Isolated Regions without trusting any other software
components on a platform, including the operating system.
(Click here to access the paper:
paper;
(c) Springer-Verlag.)