The Confinement Problem in the Presence of Faults
| Autor: | Adam Procter, Gerard Allwein, William L. Harrison |
|---|---|
| Rok vydání: | 2012 |
| Předmět: |
Soundness
Equational system Theoretical computer science Programming language Computer science business.industry Concurrency computer.software_genre Fault detection and isolation System a Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Software Asynchronous communication TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS business computer |
| Zdroj: | Formal Methods and Software Engineering ISBN: 9783642342806 ICFEM |
| DOI: | 10.1007/978-3-642-34281-3_15 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|