Abstract
We present disjunction category (DC) labels, a new label format for enforcing information flow in the presence of mutually distrusting parties. DC labels can be ordered to form a lattice, based on propositional logic implication and conjunctive normal form. We introduce and prove soundness of decentralized privileges that are used in declassifying data, in addition to providing a notion of privilege-hierarchy. Our model is simpler than previous decentralized information flow control (DIFC) systems and does not rely on a centralized principal hierarchy. Additionally, DC labels can be used to enforce information flow both statically and dynamically. To demonstrate their use, we describe two Haskell implementations, a library used to perform dynamic label checks, compatible with existing DIFC systems, and a prototype library that enforces information flow statically, by leveraging the Haskell type checker.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Bomberger, A.C., Frantz, A.P., Frantz, W.S., Hardy, A.C., Hardy, N., Landau, C.R., Shapiro, J.S.: The KeyKOS nanokernel architecture. In: Proc. of the USENIX Workshop on Micro-Kernels and Other Kernel Architectures (April 1992)
Boneh, D., Ding, X., Tsudik, G., Wong, C.: A method for fast revocation of public key certificates and security capabilities. In: Proceedings of the 10th Conference on USENIX Security Symposium, vol. 10, pages 22. USENIX Association (2001)
Broberg, N., Sands, D.: Paralocks: role-based information flow control and beyond. In: SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 431–444 (2010)
Denning, D.E.: A lattice model of secure information flow. Communications of the ACM 19(5), 236–243 (1976)
Department of Defense. Trusted Computer System Evaluation Criteria (Orange Book), DoD 5200.28-STD edition (December 1985)
Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: 2010 IEEE Symposium on Security and Privacy, pp. 109–124. IEEE (2010)
Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 795–807 (1992)
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: Proc. of the 20th ACM Symposium on Operating Systems Principles, Brighton, UK, pp. 17–30. ACM (October 2005)
Gallier, J.: Constructive logics part i: A tutorial on proof systems and typed λ- calculi. Theoretical Computer Science 110(2), 249–339 (1993)
Goguen, J., Meseguer, J.: Security policies and security models. In: I.C.S. Press (ed.) Proc. of IEEE Symp. on Security and Privacy, pp. 11–20 (April 1982)
Gunter, C., Jim, T.: Generalized certificate revocation. In: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 316–329. ACM (2000)
Howard, W.: The formulae-as-types notion of construction. To HB Curry: essays on combinatory logic, lambda calculus and formalism, pp. 479–490 (1980)
Jaskelioff, M., Russo, A.: Secure multi-execution in Haskell. In: Proc. Andrei Ershov International Conference on Perspectives of System Informatics. Springer, Heidelberg (June 2011)
Kashyap, V., Wiedermann, B., Hardekopf, B.: Timing-and termination-sensitive secure information flow: Exploring a new approach. In: 2011 IEEE Symposium on Security and Privacy (SP), pp. 413–428. IEEE (2011)
Krohn, M., Yip, A., Brodsky, M., Cliffer, N., Kaashoek, M.F., Kohler, E., Morris, R.: Information flow control for standard OS abstractions. In: Proc. of the 21st Symp. on Operating Systems Principles (October 2007)
Lampson, B.W.: A note on the confinement problem. Communications of the ACM 16(10), 613–615 (1973)
Li, P., Zdancewic, S.: Arrows for secure information flow. Theoretical Computer Science 411(19), 1974–1994 (2010)
Miller, M.S., Shapiro, J.S.: Paradigm Regained: Abstraction Mechanisms for Access Control. In: Saraswat, V.A. (ed.) ASIAN 2003. LNCS, vol. 2896, pp. 224–242. Springer, Heidelberg (2003)
Miller, M.S.: Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD thesis, Johns Hopkins University, Baltimore, Maryland, USA (May 2006)
Myers, A., Liskov, B.: Complete, safe information flow with decentralized labels. In: IEEE Security and Privacy, pp. 186–197. IEEE (1998)
Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: Proc. of the 16th ACM Symp. on Operating Systems Principles (1997)
Myers, A.C., Liskov, B.: Protecting privacy using the decentralized label model. ACM Trans. on Computer Systems 9(4), 410–442 (2000)
Papadimitriou, C.: Complexity Theory. Addison Wesley (1993)
Redell, D., Fabry, R.: Selective revocation of capabilities. In: Proceedings of the International Workshop on Protection in Operating Systems, pp. 192–209 (1974)
Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proc. IEEE Computer Security Foundations Workshop, pp. 255–269 (June 2005)
Saltzer, J.H., Schroeder, M.D.: The protection of information in computer systems. Proc. of the IEEE 63(9), 1278–1308 (1975)
Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: A tool for the automatic ver- ification of algebraic properties of functional programs. Technical report, Imperial College London (February 2011)
Stefan, D., Russo, A., Mitchell, J.C., Mazières, D.: Flexible dynamic information flow control in Haskell. In: Haskell Symposium, pp. 95–106. ACM SIGPLAN (September 2011)
Zdancewic, S., Myers, A.C.: Robust declassification. In: Proc. IEEE Computer Security Foundations Workshop, pp. 15–23 (June 2001)
Zeldovich, N., Boyd-Wickizer, S., Kohler, E., Mazières, D.: Making information flow explicit in HiStar. In: Proc. of the 7th Symp. on Operating Systems Design and Implementation, Seattle, WA, pp. 263–278 (November 2006)
Zeldovich, N., Boyd-Wickizer, S., Mazières, D.: Securing distributed systems with information flow control. In: Proc. of the 6th Symp. on Networked Systems Design and Implementation, San Francisco, CA, pp. 293–308 (April 2008)
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
Stefan, D., Russo, A., Mazières, D., Mitchell, J.C. (2012). Disjunction Category Labels. In: Laud, P. (eds) Information Security Technology for Applications. NordSec 2011. Lecture Notes in Computer Science, vol 7161. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29615-4_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-29615-4_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29614-7
Online ISBN: 978-3-642-29615-4
eBook Packages: Computer ScienceComputer Science (R0)