@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@article{harris-fmsd17,
author = {William R. Harris and
Somesh Jha and
Thomas W. Reps and
Sanjit A. Seshia},
title = {Program Synthesis for Interactive-Security Systems},
journal = {Formal Methods in System Design},
volume = {51},
number = {2},
pages = {362--394},
year = {2017},
abstract = {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.},
}