Fri 17 Jun 2016 11:30 - 12:00 at Grand Ballroom Santa Ynez - Security Chair(s): Andrew C. Myers

Hardware support for isolated execution (such as Intel SGX) enables development of applications that keep their code and data confidential even while running in a hostile or compromised host. However, automatically verifying that such applications satisfy confidentiality remains challenging. We present a methodology for designing such applications in a way that enables certifying their confidentiality. Our methodology consists of forcing the application to communicate with the external world through a narrow interface, compiling it with runtime checks that aid verification, and linking it with a small runtime that implements the narrow interface. The runtime includes services such as secure communication channels and memory management. We formalize this restriction on the application as Information Release Confinement (IRC), and we show that it allows us to decompose the task of proving confidentiality into (a) one-time, human-assisted functional verification of the runtime to ensure that it does not leak secrets, (b) automatic verification of the application’s machine code to ensure that it satisfies IRC and does not directly read or corrupt the runtime’s internal state. We present \confidential: a verifier for IRC that is modular, automatic, and keeps our compiler out of the trusted computing base. Our evaluation suggests that the methodology scales to real-world applications.

Fri 17 Jun
Times are displayed in time zone: Tijuana, Baja California change

10:30 - 12:00: SecurityResearch Papers at Grand Ballroom Santa Ynez
Chair(s): Andrew C. MyersCornell University
10:30 - 11:00
Precise, Dynamic Information Flow for Database-Backed Applications
Research Papers
Jean YangCarnegie Mellon University, Travis HanceDropbox, Thomas H. Austin, Armando Solar-LezamaMIT, Cormac FlanaganUC Santa Cruz, Stephen ChongHarvard University
Link to publication Media Attached
11:00 - 11:30
End-to-End Verification of Information-Flow Security for C and Assembly Programs
Research Papers
David CostanzoYale University, Zhong ShaoYale University, Ronghui GuYale University
Pre-print Media Attached
11:30 - 12:00
A Design and Verification Methodology for Secure Isolated Regions
Research Papers
Rohit SinhaUniversity of California, Berkeley, Manuel CostaMicrosoft Research, Akash LalMicrosoft Research India, Nuno P. LopesMicrosoft Research, Sriram RajamaniMicrosoft Research, Sanjit SeshiaUC Berkeley, Kapil VaswaniMicrosoft Research
Media Attached