The confinement problem in the presence of faults
2012
In this paper, we establish a semantic foundation for the safe execution of untrusted code. Our approach extends Moggi's computational λ-calculus in two dimensions with operations for asynchronous concurrency, shared state and software faults and with an effect type system a la Wadler providing fine-grained control of effects. An equational system for fault isolation is exhibited and its soundness demonstrated with a semantics based on monad transformers. Our formalization of the equational system in the Coq theorem prover is discussed. We argue that the approach may be generalized to capture other safety properties, including information flow security.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
42
References
9
Citations
NaN
KQI