Back to Search
Start Over
A Logic of Programs with Interface-Confined Code
- Source :
- CSF
- Publication Year :
- 2015
- Publisher :
- IEEE, 2015.
-
Abstract
- 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.
Details
- Database :
- OpenAIRE
- Journal :
- 2015 IEEE 28th Computer Security Foundations Symposium
- Accession number :
- edsair.doi...........7c69cd88ff93096eb8a58d5d47f15044