Program Synthesis for Interactive-Security Systems

William R. Harris, Somesh Jha, Thomas W. Reps, and Sanjit A. Seshia. Program Synthesis for Interactive-Security Systems. Formal Methods in System Design, 51(2):362–394, 2017.

Download

[HTML] 

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.

BibTeX

@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.},
}

Generated by bib2html.pl (written by Patrick Riley ) on Tue Apr 24, 2018 09:06:48