@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@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.},
}