LWeb: information flow security for multi-tier web applications

Abstract

This paper presents LWeb, a framework for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enforcement library with the Yesod web programming framework. The implementation has two parts. First, we extract the core of LIO into a monad transformer (LMonad) and then apply it to Yesod’s core monad. Second, we extend Yesod’s table definition DSL and query functionality to permit defining and enforcing label-based policies on tables and enforcing them during query processing. LWeb’s policy language is expressive, permitting dynamic per-table and per-row policies. We formalize the essence of LWeb in the λ_LWeb calculus and mechanize the proof of noninterference in Liquid Haskell. This mechanization constitutes the first metatheoretic proof carried out in Liquid Haskell. We also used LWeb to build a substantial web site hosting the Build it, Break it, Fix it security-oriented programming contest. The site involves 40 data tables and sophisticated policies. Compared to manually checking security policies, LWeb imposes a modest runtime overhead of between 2% to 21%. It reduces the trusted code base from the whole application to just 1% of the application code, and 21% of the code overall (when counting LWeb too).

References

1. Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick McDaniel. 2014. FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps. In PLDI.
2. Thomas H. Austin and Cormac Flanagan. 2012. Multiple Facets for Dynamic Information Flow. In POPL.
3. Thomas H. Austin, Jean Yang, Cormac Flanagan, and Armando Solar-Lezama. 2013. Faceted execution of policy-agnostic programs. In PLAS.
4. D. Elliott Bell and Leonard J. LaPadula. 1973. Secure Computer Systems: Mathematical Foundations. MITRE Technical Report 2547 1 (1973).
5. Pablo Buiras, Joachim Breitner, and Alejandro Russo. 2017. Securing concurrent lazy programs against information leakage. In CSF.
6. Pablo Buiras, Dimitrios Vytiniotis, and Alejandro Russo. 2015. HLIO: Mixing Static and Dynamic Typing for Information-flow Control in Haskell. In ICFP.
7. Adam Chlipala. 2010. Static Checking of Dynamically-varying Security Policies in Database-backed Applications. In OSDI.
8. Stephen Chong, Jed Liu, Andrew C. Myers, Xin Qi, K. Vikram, Lantian Zheng, and Xin Zheng. 2007a. Secure Web Applications via Automatic Partitioning. In SOSP.
9. Stephen Chong, K. Vikram, and Andrew C. Myers. 2007b. SIF: Enforcing Confidentiality and Integrity in Web Applications. In USENIX Security Symposium.
10. Andrey Chudnov and David A. Naumann. 2015. Inlined Information Flow Monitoring for JavaScript. In CCS.
11. Brian J. Corcoran, Nikhil Swamy, and Michael Hicks. 2009. Cross-tier, Label-based Security Enforcement for Web Applications. In SIGMOD.
12. Dorothy E. Denning. 1976. A Lattice Model of Secure Information Flow. Commun. ACM 19, 5 (1976).
13. Petros Efstathopoulos, Maxwell Krohn, Steve VanDeBogart, Cliff Frey, David Ziegler, Eddie Kohler, David Mazières, Frans Kaashoek, and Robert Morris. 2005. Labels and Event Processes in the Asbestos Operating System. In SOSP.
14. Esqueleto 2018. Esqueleto: Type-safe EDSL for SQL queries on persistent backends. https://github.com/bitemyapp/esqueleto/ blob/master/docs/blog_post_2012_08_06 .
15. Daniel Giffin, Amit Levy, Deian Stefan, David Terei, David Mazieres, John Mitchell, and Alejandro Russo. 2017. Hails: Protecting data privacy in untrusted web applications. Journal of Computer Security 25, 4 (2017).
16. Daniel B. Giffin, Amit Levy, Deian Stefan, David Terei, David Mazières, John C. Mitchell, and Alejandro Russo. 2012. Hails: Protecting Data Privacy in Untrusted Web Applications. In OSDI.
17. Joseph A. Goguen and JosÃľ Meseguer. 1982. Security Policies and Security Models. In S&P.
18. Christian Hammer and Gregor Snelting. 2009. Flow-sensitive, Context-sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs. International Journal of Information Security 8, 6 (2009).
19. Daniel Hedin, Luciano Bello, and Andrei Sabelfeld. 2016. Information-flow security for JavaScript and its APIs. Journal of Computer Security 24, 2 (2016).
20. Stefan Heule, Deian Stefan, Edward Z. Yang, John C. Mitchell, and Alejandro Russo. 2015. IFC Inside: Retrofitting Languages with Dynamic Information Flow Control. In POST.
21. Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong. 2015. Exploring and Enforcing Security Guarantees via Program Dependence Graphs. In PLDI.
22. Dave King, Boniface Hicks, Michael Hicks, and Trent Jaeger. 2008. Implicit Flows: Can’t live with ’em, can’t live without ’em. In International Conference on Information Systems Security (ICISS) (Lecture Notes in Computer Science), R. Sekar and Arun K. Pujari (Eds.), Vol. 5352.
23. Maxwell Krohn, Alexander Yip, Micah Brodsky, Natan Cliffer, M. Frans Kaashoek, Eddie Kohler, and Robert Morris. 2007. Information Flow Control for Standard OS Abstractions. In SOSP.
24. K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR.
25. Peng Li and Steve Zdancewic. 2010. Arrows for Secure Information Flow. Theoretical Computer Science 411, 19 (2010).
26. Luísa Lourenço and Luís Caires. 2014. Information Flow Analysis for Valued-Indexed Data Security Compartments. In International Symposium on Trustworthy Global Computing - Volume 8358 .
27. Luísa Lourenço and Luís Caires. 2015. Dependent Information Flow Types. In POPL.
28. Aastha Mehta, Eslam Elnikety, Katura Harvey, Deepak Garg, and Peter Druschel. 2017. Qapla: Policy compliance for database-backed systems. In USENIX Security Symposium.
29. Divya Muthukumaran, Dan O’Keeffe, Christian Priebe, David Eyers, Brian Shand, and Peter Pietzuch. 2015. FlowWatcher: Defending Against Data Disclosure Vulnerabilities in Web Applications. In CCS.
30. Andrew C. Myers. 1999. JFlow: Practical Mostly-static Information Flow Control. In POPL.
31. François Pottier and Vincent Simonet. 2003. Information Flow Inference for ML. ACM Trans. Program. Lang. Syst. 25, 1 (2003).
32. Indrajit Roy, Donald E. Porter, Michael D. Bond, Kathryn S. McKinley, and Emmett Witchel. 2009. Laminar: Practical Fine-grained Decentralized Information Flow Control. In PLDI.
33. Andrew Ruef, Michael Hicks, James Parker, Dave Levin, Michelle L. Mazurek, and Piotr Mardziel. 2016. Build It, Break It, Fix It: Contesting Secure Development. In CCS.
34. Alejandro Russo. 2015. Functional Pearl: Two Can Keep a Secret, if One of Them Uses Haskell. In ICFP.
35. Alejandro Russo, Koen Claessen, and John Hughes. 2008. A library for light-weight information-flow security in haskell. In Haskell Symposium .
36. Andrei Sabelfeld and Andrew C. Myers. 2003. Language-based information-flow security. Selected Areas in Communications, IEEE Journal on 21, 1 (2003).
37. Andrei Sabelfeld and David Sands. 2009. Declassification: Dimensions and Principles. Journal of Computer Security 17, 5 (2009).
38. Daniel Schoepe, Daniel Hedin, and Andrei Sabelfeld. 2014. SeLINQ: Tracking Information Across Application-database Boundaries. In ICFP.
39. David Schultz and Barbara Liskov. 2013. IFDB: Decentralized Information Flow Control for Databases. In EuroSys.
40. Tim Sheard and Simon Peyton Jones. 2002. Template Meta-programming for Haskell. In Haskell Workshop.
41. Michael Snoyman. 2018. Yesod Web Framework for Haskell. http://www.yesodweb.com/.
42. Deian Stefan, Alejandro Russo, David Mazières, and John C. Mitchell. 2012. Disjunction Category Labels. In NordSec.
43. Deian Stefan, Alejandro Russo, David Mazières, and John C. Mitchell. 2017. Flexible Dynamic Information Flow Control in the Presence of Exceptions. Journal of Functional Programming 27, E5 (2017).
44. Deian Stefan, Alejandro Russo, John C. Mitchell, and David Mazières. 2011. Flexible Dynamic Information Flow Control in Haskell. In Haskell Symposium.
45. Nikhil Swamy, Brian Corcoran, and Michael Hicks. 2008. Fable: A Language for Enforcing User-defined Security Policies. In S&P .
46. Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In POPL.
47. David Terei, Simon Marlow, Simon Peyton Jones, and David Mazières. 2012. Safe Haskell. In Haskell Symposium.
48. Eran Tromer and Roei Schuster. 2016. DroidDisintegrator: Intra-Application Information Flow Control in Android Apps. In ASIA CCS .
49. Marco Vassena and Alejandro Russo. 2016. On Formalizing Information-Flow Control Libraries. In PLAS.
50. Niki Vazou, Leonidas Lampropoulos, and Jeff Polakow. 2017. A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq. In Haskell Symposium.
51. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. Refinement Types for Haskell. In ICFP.
52. Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. 2018. Refinement Reflection: Complete Verification with SMT. PACMPL 2, POPL (2018).
53. Lucas Waye, Pablo Buiras, Owen Arden, Alejandro Russo, and Stephen Chong. 2017. Cryptographically Secure Information Flow Control on Key-Value Stores. In CCS.
54. Jean Yang, Travis Hance, Thomas H. Austin, Armando Solar-Lezama, Cormac Flanagan, and Stephen Chong. 2016. Precise, Dynamic Information Flow for Database-backed Applications. In PLDI.
55. Jean Yang, Kuat Yessenov, and Armando Solar-Lezama. 2012. A language for automatically enforcing privacy policies. In POPL .
56. Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazières. 2006. Making Information Flow Explicit in HiStar. In OSDI.

Index Terms

• Security and privacy

  • Formal methods and theory of security

    • Logic and verification

  • Software and application security

    • Web application security

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

      • Semantics