The Confinement Problem in the Presence of Faults

William L.  Harrison; Adam Procter; Gerard Allwein

doi:10.1007/978-3-642-34281-3_15

The Confinement Problem in the Presence of Faults

William L. Harrison
, Adam Procter
, Gerard Allwein

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

8 Scopus citations

Abstract

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.

Original language	Undefined/Unknown
Title of host publication	Proceedings of the 2012 International Conference on Formal Engineering Methods
DOIs	https://doi.org/10.1007/978-3-642-34281-3_15
State	Published - 2012
Externally published	Yes

Access to Document

10.1007/978-3-642-34281-3_15

Cite this

@inproceedings{e9fb339dd24b4ae0b01a415404780baf,

title = "The Confinement Problem in the Presence of Faults",

abstract = "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.",

author = "Harrison, \{William L.\} and Adam Procter and Gerard Allwein",

year = "2012",

doi = "10.1007/978-3-642-34281-3\_15",

language = "Undefined/Unknown",

booktitle = "Proceedings of the 2012 International Conference on Formal Engineering Methods",

}

TY - GEN

T1 - The Confinement Problem in the Presence of Faults

AU - Harrison, William L.

AU - Procter, Adam

AU - Allwein, Gerard

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-34281-3_15

DO - 10.1007/978-3-642-34281-3_15

M3 - Conference contribution

BT - Proceedings of the 2012 International Conference on Formal Engineering Methods

ER -

The Confinement Problem in the Presence of Faults

Abstract

Access to Document

Fingerprint

Cite this