Abstract
Secure multi-execution (SME) is a dynamic technique to ensure secure information flow. In a nutshell, SME enforces security by running one execution of the program per security level, and by reinterpreting input/output operations w.r.t. their associated security level. SME is sound, in the sense that the execution of a program under SME is non-interfering, and precise, in the sense that for programs that are non-interfering in the usual sense, the semantics of a program under SME coincides with its standard semantics. A further virtue of SME is that its core idea is language-independent; it can be applied to a broad range of languages. A downside of SME is the fact that existing implementation techniques require modifications to the runtime environment, e.g. the browser for Web applications. In this article, we develop an alternative approach where the effect of SME is achieved through program transformation, without modifications to the runtime, thus supporting server-side deployment on the web. We show on an exemplary language with input/output and dynamic code evaluation (modeled after JavaScript’s eval) that our transformation is sound and precise. The crux of the proof is a simulation between the execution of the transformed program and the SME execution of the original program. This proof has been machine-checked using the Agda proof assistant. We also report on prototype implementations for a small fragment of Python and a substantial subset of JavaScript.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. In: CSF, pp. 43–59 (2009)
Austin, T., Flanagan, C.: Multiple facets for dynamic information flow. In: POPL (2012)
Austin, T.H., Flanagan, C.: Permissive dynamic information flow analysis. In: PLAS (2010)
Barthe, G., Crespo, J.M., Devriese, D., Piessens, F., Rivas, E.: Secure multi-execution through static program transformation: extended version. Technical Report CW620, Department of Computer Science, Katholieke Universiteit Leuven (2012)
Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: CSFW, pp. 100–114 (2004)
Bielova, N., Devriese, D., Massacci, F., Piessens, F.: Reactive non-interference for a browser model. In: NSS (2011)
Birgisson, A., Russo, A., Sabelfeld, A.: Capabilities for information flow. In: PLAS (2011)
Capizzi, R., Longo, A., Venkatakrishnan, V.N., Prasad Sistla, A.: Preventing information leaks through shadow executions. In: ACSAC (2008)
Cavadini, S.: Secure slices of insecure programs. In: ASIACCS, pp. 112–122 (2008)
Chudnov, A., Naumann, D.A.: Information flow monitor inlining. In: CSF, pp. 200–214 (2010)
Chugh, R., Meister, J.A., Jhala, R., Lerner, S.: Staged information flow for Javascript. In: PLDI (2009)
Cristiá, M., Mata, P.: Runtime enforcement of noninterference by duplicating processes and their memories. In: WSEGI 2009 (2009)
Crockford, D.: Adsafe (December 2009), http://www.adsafe.org/
Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: IEEE Symposium on Security and Privacy, pp. 109–124 (2010)
Facebook. Fbjs (2011), http://developers.facebook.com/docs/fbjs/
Le Guernic, G.: Confidentiality Enforcement Using Dynamic Information Flow Analyses. PhD thesis, Kansas State University (2007)
Heintze, N., Riecke, J.G.: The SLam calculus: programming with secrecy and integrity. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 365–377 (January 1998)
Jaskelioff, M., Russo, A.: Secure multi-execution in haskell. In: PSI (2011)
Kashyap, V., Wiedermann, B., Hardekopf, B.: Timing- and termination-sensitive secure information flow: Exploring a new approach. In: Proceedings of the 2011 IEEE Symposium on Security and Privacy, SP 2011, pp. 413–428. IEEE Computer Society, Washington, DC (2011)
Louw, M.T., Ganesh, K.T., Venkatakrishnan, V.N.: Adjail: Practical enforcement of confidentiality and integrity policies on web advertisements. In: USENIX Security Symposium, pp. 371–388 (2010)
Maffeis, S., Mitchell, J.C., Taly, A.: Isolating JavaScript with Filters, Rewriting, and Wrappers. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 505–522. Springer, Heidelberg (2009)
Maffeis, S., Mitchell, J.C., Taly, A.: Object capabilities and isolation of untrusted web applications. In: IEEE Symposium on Security and Privacy, pp. 125–140 (2010)
Miller, M.S., Samuel, M., Laurie, B., Awad, I., Stay, M.: Caja: Safe active content in sanitized javascript (January 2008), http://google-caja.googlecode.com/files/caja-spec-2008-01-15.pdf
Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 228–241 (January 1999)
Richards, G., Hammer, C., Burg, B., Vitek, J.: The Eval That Men Do. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 52–78. Springer, Heidelberg (2011)
Russo, A., Sabelfeld, A.: Securing timeout instructions in web applications. In: CSF, pp. 92–106 (2009)
Russo, A., Sabelfeld, A., Chudnov, A.: Tracking Information Flow in Dynamic Tree Structures. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 86–103. Springer, Heidelberg (2009)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. JSAC 21, 5–19 (2003)
Sabelfeld, A., Russo, A.: From Dynamic to Static and Back: Riding the Roller Coaster of Information-Flow Control Research. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 352–365. Springer, Heidelberg (2010)
Taly, A., Erlingsson, U., Miller, M.S., Mitchell, J.C., Nagra, J.: Automated analysis of security-critical javascript apis. In: IEEE Symposium on Security and Privacy (2011)
Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. Journal of Computer Security 4(2/3), 167–188 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Barthe, G., Crespo, J.M., Devriese, D., Piessens, F., Rivas, E. (2012). Secure Multi-Execution through Static Program Transformation. In: Giese, H., Rosu, G. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2012 2012. Lecture Notes in Computer Science, vol 7273. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30793-5_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-30793-5_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30792-8
Online ISBN: 978-3-642-30793-5
eBook Packages: Computer ScienceComputer Science (R0)