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 \(\grave{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.
This research was supported by NSF CAREER Award 00017806, US Naval Research Laboratory Contract 1302-08-015S, and by the U.S. Department of Education GAANN grant no. P200A100053.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Banerjee, A., Heintze, N., Riecke, J.: A core calculus of dependency. In: 26th ACM Symp. on Principles of Programming Languages, pp. 147–160 (1999)
Allwein, G., Harrison, W.L.: Partially-ordered modalities. In: Advances in Modal Logic, pp. 1–21 (2010)
Barham, P., Dragovic, B., Fraser, K., Hand, S., Harris, T., Ho, A., Neugebauer, R., Pratt, I., Warfield, A.: Xen and the art of virtualization. In: Proceedings of the 19th ACM Symposium on Operating Systems Principles, pp. 164–177 (2003)
Bartolett, M., Degano, P., Ferrari, G.-L.: History-Based Access Control with Local Policies. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 316–332. Springer, Heidelberg (2005)
Bartoletti, M., Degano, P., Ferrari, G.L.: Types and effects for secure service orchestration. In: 19th IEEE Computer Security Foundations Workshop (2006)
Bauer, L., Ligatti, J., Walker, D.W.: Types and Effects for Non-interfering Program Monitors. In: Okada, M., Babu, C.S., Scedrov, A., Tokuda, H. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 154–171. Springer, Heidelberg (2003)
Benton, N., Hur, C.-K., Kennedy, A., McBride, C.: Strongly Typed Term Representations in Coq. Journal of Automated Reasoning, 1–19 (to appear)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer (2004)
Chlipala, A.: Certified programming with dependent types Book draft of April 12 (2012), http://adam.chlipala.net/cpdt/
Cock, D., Klein, G., Sewell, T.: Secure Microkernels, State Monads and Scalable Refinement. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 167–182. Springer, Heidelberg (2008)
Goguen, J., Meseguer, J.: Security policies and security models. In: Symposium on Security and Privacy, pp. 11–20. IEEE (1982)
Goncharov, S., Schröder, L.: A Coinductive Calculus for Asynchronous Side-Effecting Processes. In: Owe, O., Steffen, M., Telle, J.A. (eds.) FCT 2011. LNCS, vol. 6914, pp. 276–287. Springer, Heidelberg (2011)
Harrison, W.L.: The Essence of Multitasking. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 158–172. Springer, Heidelberg (2006)
Harrison, W.L., Hook, J.: Achieving information flow security through monadic control of effects. Journal of Computer Security 17(5), 599–653 (2009)
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proc. 22nd ACM Symposium on Operating Systems Principles (SOSP), pp. 207–220 (2009)
Kobayashi, S.: Monad as modality. Theor. Computer Science 175(1), 29–74 (1997)
Lampson, B.: A note on the confinement problem. CACM 16(10), 613–615 (1973)
Liang, S.: Modular Monadic Semantics and Comp. PhD thesis, Yale Univ. (1998)
Mantel, H., Sudbrock, H.: Flexible Scheduler-Independent Security. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 116–133. Springer, Heidelberg (2010)
Martin, W., White, P., Taylor, F.S., Goldberg, A.: Formal construction of the mathematically analyzed separation kernel. In: Proceedings of the 15th IEEE International Conference on Automated Software Engineering, pp. 133–141 (2000)
Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). The MIT Press (1997)
Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (1991)
Nanevski, A.: A Modal Calculus for Exception Handling. In: Intuitionistic Modal Logics and Applications Workshop (IMLA 2005) (June 2005)
Nielson, F., Nielson, H., Hankin, C.: Principles of Program Analysis (1999)
Peyton Jones, S. (ed.): Haskell 98 Language and Libraries, the Revised Report. Cambridge University Press (2003)
Russo, A., Sabelfeld, A.: Securing interaction between threads and the scheduler. In: Proc. of the 19th IEEE Workshop on Comp. Sec. Found., pp. 177–189 (2006)
Sabelfeld, A., Myers, A.C.: Language-based information flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Swierstra, W., Altenkirch, T.: Beauty in the beast. In: Proceedings of the ACM SIGPLAN Haskell Workshop (Haskell 2007), pp. 25–36 (2007)
Wadler, P.: The marriage of effects and monads. In: Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming, pp. 63–74 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harrison, W.L., Procter, A., Allwein, G. (2012). The Confinement Problem in the Presence of Faults. In: Aoki, T., Taguchi, K. (eds) Formal Methods and Software Engineering. ICFEM 2012. Lecture Notes in Computer Science, vol 7635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34281-3_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-34281-3_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34280-6
Online ISBN: 978-3-642-34281-3
eBook Packages: Computer ScienceComputer Science (R0)