Abstract
Many important security problems in JavaScript, such as browser extension security, untrusted JavaScript libraries and safe integration of mutually distrustful websites (mash-ups), may be effectively addressed using an efficient implementation of information flow control (IFC). Unfortunately existing fine-grained approaches to JavaScript IFC require modifications to the language semantics and its engine, a non-goal for browser applications. In this work, we take the ideas of coarse-grained dynamic IFC and provide the theoretical foundation for a language-based approach that can be applied to any programming language for which external effects can be controlled. We then apply this formalism to server- and client-side JavaScript, show how it generalizes to the C programming language, and connect it to the Haskell LIO system. Our methodology offers design principles for the construction of information flow control systems when isolation can easily be achieved, as well as compositional proofs for optimized concrete implementations of these systems, by relating them to their isolated variants.
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
Zeldovich, N., Boyd-Wickizer, S., Kohler, E., Mazières, D.: Making information flow explicit in HiStar. In: OSDI (2006)
Hedin, D., Birgisson, A., Bello, L., Sabelfeld, A.: JSFlow: Tracking information flow in JavaScript and its APIs. In: SAC (2014)
Matthews, J., Findler, R.B.: Operational semantics for multi-language programs. In: POPL (2007)
Stefan, D., Yang, E.Z., Marchenko, P., Russo, A., Herman, D., Karp, B., Mazières, D.: Protecting users by confining JavaScript with COWL. In: OSDI (2014)
Heule, S., Stefan, D., Yang, E.Z., Mitchell, J.C., Russo, A.: Ifc inside: Retrofitting languages with dynamic information flow control (2015), http://cowl.ws/ifc-inside.pdf
Goguen, J., Meseguer, J.: Security policies and security Models. In: SP (1982)
Hritcu, C., Greenberg, M., Karel, B., Pierce, B.C., Morrisett, G.: All your IFCException are belong to us. In: SP (2013)
Stefan, D., Russo, A., Mitchell, J.C., Mazières, D.: Flexible dynamic information flow control in the presence of exceptions. Arxiv preprint arXiv:1207.1457 (2012)
Hedin, D., Sabelfeld, A.: Information-flow security for a core of javascript. In: CSF (2012)
Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. TCS 103 (1992)
Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19 (1976)
Stefan, D., Russo, A., Mitchell, J.C., Mazières, D.: Flexible dynamic information flow control in Haskell. In: Haskell (2011)
W3C: HTML5 web messaging (2012), http://www.w3.org/TR/webmessaging/
Stefan, D., Buiras, P., Yang, E.Z., Levy, A., Terei, D., Russo, A., Mazières, D.: Eliminating cache-based timing attacks with instruction-based scheduling. In: ESORICS (2013)
Buiras, P., Levy, A., Stefan, D., Russo, A., Mazières, D.: A library for removing cache-based attacks in concurrent information flow systems. In: TGC (2013)
Li, P., Zdancewic, S.: Arrows for secure information flow. TCS 411 (2010)
Russo, A., Claessen, K., Hughes, J.: A library for light-weight information-flow security in Haskell. In: Haskell (2008)
Stefan, D., Russo, A., Buiras, P., Levy, A., Mitchell, J.C., Mazières, D.: Addressing covert termination and timing channels in concurrent information flow systems. In: ICFP (2012)
Boudol, C.: Noninterference for concurrent programs. In: ICALP (2001)
Yang, E.Z., Mazières, D.: Dynamic space limits for Haskell. In: PLDI (2014)
Russo, A., Sabelfeld, A.: Securing Interaction between threads and the scheduler. In: CSFW (2006)
Barthe, G., Rezk, T., Russo, A., Sabelfeld, A.: Security of multithreaded programs by compilation. In: ESORICS (2007)
Askarov, A., Hunt, S., Sabelfeld, A., Sands, D.: Termination-insensitive noninterference leaks more than just a bit. In: ESORICS (2008)
Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: Jif: Java Information Flow. Software release (2001), Located at http://www.cs.cornell.edu/jif
Simonet, V.: The Flow Caml system (2003), Software release at http://cristal.inria.fr/~simonet/soft/flowcaml/
Ecma International: ECMAScript language specification (2014), http://www.ecma.org/
Taly, A., Mitchell, J.C., Miller, M.S., Nagra, J.: Automated analysis of security-critical javascript apis. In: SP (2011)
Belay, A., Bittau, A., Mashtizadeh, A., Terei, D., Mazières, D., Kozyrakis, C.: Dune: Safe user-level access to privileged CPU features. In: OSDI (2012)
Bittau, A., Marchenko, P., Handley, M., Karp, B.: Wedge: Splitting applications into reduced-privilege compartments. In: NSDI (2008)
Efstathopoulos, P., Krohn, M., VanDeBogart, S., Frey, C., Ziegler, D., Kohler, E., Mazières, D., Kaashoek, F., Morris, R.: Labels and event processes in the Asbestos operating system. In: SOSP (2005)
Krohn, M., Yip, A., Brodsky, M., Cliffer, N., Kaashoek, M.F., Kohler, E., Morris, R.: Information flow control for standard OS abstractions. In: SOSP (2007)
Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: POPL (1998)
Volpano, D., Smith, G.: Eliminating covert flows with minimum typings. In: CSFW (1997)
Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: SP (2010)
Rafnsson, W., Sabelfeld, A.: Secure multi-execution: fine-grained, declassification-aware, and transparent. In: CSF (2013)
Bielova, N., Devriese, D., Massacci, F., Piessens, F.: Reactive non-interference for a browser model. In: NSS (2011)
Zanarini, D., Jaskelioff, M., Russo, A.: Precise enforcement of confidentiality for reactive systems. In: CSF (2013)
Jacobs, B., Rutten, J.: A Tutorial on (Co)Algebras and (Co)Induction. EATCS 62 (1997)
Yip, A., Narula, N., Krohn, M., Morris, R.: Privacy-preserving browser-side scripting with BFlow. In: EuroSys (2009)
De Groef, W., Devriese, D., Nikiforakis, N., Piessens, F.: FlowFox: a web browser with flexible and precise information flow control. In: CCS (2012)
Armstrong, J.: Making reliable distributed systems in the presence of software errors (2003)
Papagiannis, I., Migliavacca, M., Eyers, D.M., Sh, B., Bacon, J., Pietzuch, P.: Enforcing user privacy in web applications using Erlang. In: W2SP (2010)
Abadi, M., Banerjee, A., Heintze, N., Riecke, J.: A Core Calculus of Dependency. In: POPL (1999)
Tse, S., Zdancewic, S.: Translating dependency into parametricity. In: ICFP (2004)
Broberg, N., Sands, D.: Paralocks: Role-based information flow control and beyond. In: POPL (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heule, S., Stefan, D., Yang, E.Z., Mitchell, J.C., Russo, A. (2015). IFC Inside: Retrofitting Languages with Dynamic Information Flow Control. In: Focardi, R., Myers, A. (eds) Principles of Security and Trust. POST 2015. Lecture Notes in Computer Science(), vol 9036. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46666-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-662-46666-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46665-0
Online ISBN: 978-3-662-46666-7
eBook Packages: Computer ScienceComputer Science (R0)