Abstract
An application that fails to ensure information flow security may leak sensitive data such as passwords, credit card numbers, or medical records. News stories of such failures abound. Austin and Flanagan [2] introduce faceted values – values that present different behavior according to the privilege of the observer – as a dynamic approach to enforce information flow policies for an untyped, imperative \(\lambda \)-calculus.
We implement faceted values as a Haskell library, elucidating their relationship to types and monadic imperative programming. In contrast to previous work, our approach does not require modification to the language runtime. In addition to pure faceted values, our library supports faceted mutable reference cells and secure facet-aware socket-like communication. This library guarantees information flow security, independent of any vulnerabilities or bugs in application code. The library uses a control monad in the traditional way for encapsulating effects, but it also uniquely uses a second data monad to structure faceted values. To illustrate a non-trivial use of the library, we present a bi-monadic interpreter for a small language that illustrates the interplay of the control and data monads.
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
Similar content being viewed by others
Notes
- 1.
We refer to sensitive values as “private” and non-sensitive values as “public”, as confidentiality is generally given more attention in the literature on information flow analysis. However, the same mechanism can also enforce integrity properties, such as that trusted outputs are not influenced by untrusted inputs.
- 2.
Alternatively, a faceted value can be interpreted as a function mapping sets of labels to values, and the syntax above as merely a compact representation.
- 3.
That is, authorized to see data marked as sensitive to principal k.
- 4.
Faceted values are closely related to the value pairs used by [22]; while intended as a proof technique rather than a dynamic enforcement mechanism, the construct is essentially identical.
References
Austin, T.H., Flanagan, C.: Efficient purely-dynamic information flow analysis. In: PLAS 2009. ACM Press, New York (2009)
Austin, T.H., Flanagan, C.: Multiple Facets for Dynamic Information Flow. In: POPL 2012, pp. 165–178. ACM Press, New York (2012)
Austin, T.H., et al.: Faceted execution of policy-agnostic programs. In: PLAS 2013, 15–26. ACM Press, New York (2013)
Buiras, P., Russo, A.: Lazy programs leak secrets. In: Riis Nielson, H., Gollmann, D. (eds.) NordSec 2013. LNCS, vol. 8208, pp. 116–122. Springer, Heidelberg (2013)
De Groef, W., et al.: FlowFox: a web browser with flexible and precise information flow control. In: CCS 2012, pp. 748–759. ACM Press, New York (2012)
Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)
Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977)
Devriese, D., Piessens, F.: Information Flow Enforcement in Monadic Libraries. In: TLDI 2011, pp. 59–72. ACM Press, New York (2011)
Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: Symposium on Security and Privacy, pp. 109–124. IEEE, Los Alamitos (2010)
Dhawan, M., Ganapathy, V.: Analyzing information flow in javascript-based browser extensions. In: ACSAC. IEEE (2009)
Fenton, J.S.: Memoryless subsystems. Comput. J. 17(2), 143–147 (1974)
Le Guernic, G., Banerjee, A., Jensen, T., Schmidt, D.A.: Automata-based confidentiality monitoring. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 75–89. Springer, Heidelberg (2008)
Hedin, D., Sabelfeld, A.: Information-flow security for a core of JavaScript. In: CSF, pp. 3–18. IEEE (2012)
Heintze, N., Riecke, J.G.: The SLam calculus: programming with secrecy and integrity. In: POPL, pp. 365–377. ACM (1998)
Jang, D., et al.: An empirical study of privacy-violating information flows in JavaScript web applications. In: ACM Conference on Computer and Communications Security, pp. 270–283 (2010)
Jaskelioff, M., Russo, A.: Secure multi-execution in haskell. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 170–178. Springer, Heidelberg (2012)
Jones, M.P., Duponcheel, L.: Composing Monads. Technical report. Research Report YALEU/DCS/RR-1004. Yale University (1993)
Kerschbaumer, C., Hennigan, E., Larsen, P., Brunthaler, S., Franz, M.: Towards precise and efficient information flow control in web browsers. In: Huth, M., Asokan, N., Čapkun, S., Flechais, I., Coles-Kemp, L. (eds.) TRUST 2013. LNCS, vol. 7904, pp. 187–195. Springer, Heidelberg (2013)
Li, P., Zdancewic, S.: Encoding information flow in haskell. In: CSFW 2006, p.12. IEEE Computer Society, Washington, DC, USA (2006)
Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: Proceedings of 22nd ACM Symposium on Principles of Programming Languages. ACM Press, New York (1995)
Myers, A.C.: JFlow: practical mostly-static information flow control. In: Symposium on Principles of Programming Languages (POPL), pp. 228–241. ACM (1999)
Pottier, F., Simonet, V.: Information flow inference for ML. ACM Trans. Program. Lang. Syst. 25(1), 117–158 (2003)
Rafnsson, W., Sabelfeld, A.: Secure multi-execution: fine-grained, declassification-aware, and transparent. In: IEEE 26th Computer Security Foundations Symposium (CSF), pp. 33–48 (2013)
Russo, A., Claessen, K., Hughes, J.: A library for lightweight information-flow security in haskell. In: Haskell 2008, pp. 13–24. ACM, New York, NY, USA (2008)
Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: CSF 2010, pp. 186–199. IEEE Computer Society, Washington, DC, USA (2010)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas in Commun. 21(1), 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)
Sabelfeld, A., Sands, D.: Declassification: dimensions and principles. J. Comput. Secur. 17(5), 517–548 (2009)
Schmitz, T., et al.: Faceted dynamic information flow via control and data monads. In: University of California, Santa Cruz, Technical report UCSC-SOE-16-01 (2016)
Steele, G.L., Jr.: Building interpreters by composing monads. In: POPL 1994. ACM, Portland (1994)
Stefan, D., et al.: Flexible dynamic information flow control in haskell. In: Haskell 2011, 95–106. ACM, New York (2011)
Stefan, D., et al.: Flexible dynamic information flow control in Haskell, vol. 46(12). ACM (2011)
Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2–3), 167–187 (1996)
Wadler, P.: The essence of functional programming. In: POPL 1992. ACM, Albuquerque, New Mexico, USA (1992)
Zanarini, D., Jaskelioff, M., Russo, A.: Precise enforcement of confidentiality for reactive systems. In: CSF, pp. 18–32 (2013)
Zdancewic, S.A.: Programming languages for information security. PhD thesis. Cornell University (2002)
Acknowledgements
This research was supported by the National Science Foundation under grants CCF-1337278 and CCF-1421016.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmitz, T., Rhodes, D., Austin, T.H., Knowles, K., Flanagan, C. (2016). Faceted Dynamic Information Flow via Control and Data Monads. In: Piessens, F., Viganò, L. (eds) Principles of Security and Trust. POST 2016. Lecture Notes in Computer Science(), vol 9635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49635-0_1
Download citation
DOI: https://doi.org/10.1007/978-3-662-49635-0_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-49634-3
Online ISBN: 978-3-662-49635-0
eBook Packages: Computer ScienceComputer Science (R0)
