Visible to the public A Logic of Programs with Interface-Confined CodeConflict Detection Enabled

TitleA Logic of Programs with Interface-Confined Code
Publication TypeConference Paper
Year of Publication2015
AuthorsLimin Jia, Shayak Sen, Deepak Garg, Anupam Datta
Conference Name2015 IEEE 28th Computer Security Foundations Symposium (CSF)
Date Published07/2015
Conference LocationItaly
KeywordsCMU, July'15

Interface-confinement is a common mechanism that secures untrusted code by executing it inside a sandbox. The sandbox limits (confines) the code's interaction with key system resources to a restricted set of interfaces. This practice is seen in web browsers, hypervisors, and other security-critical systems. Motivated by these systems, we present a program logic, called System M, for modeling and proving safety properties of systems that execute adversary-supplied code via interface-confinement. In addition to using computation types to specify effects of computations, System M includes a novel invariant type to specify the properties of interface-confined code. The interpretation of invariant type includes terms whose effects satisfy an invariant. We construct a step-indexed model built over traces and prove the soundness of System M relative to the model. System M is the first program logic that allows proofs of safety for programs that execute adversary-supplied code without forcing the adversarial code to be available for deep static analysis. System M can be used to model and verify protocols as well as system designs. We demonstrate the reasoning principles of System M by verifying the state integrity property of the design of Memoir, a previously proposed trusted computing system.

Citation Keynode-24940

Other available formats:

Jia_Logic_of_Programs_AD.pdfPDF document427.81 KBDownloadPreview