Abstract
Security is rarely a static notion. What is considered to be confidential or untrusted data varies over time according to changing events and states. The static verification of secure information flow has been a popular theme in recent programming language research, but information flow policies considered are based on multilevel security which presents a static view of security levels. In this paper we introduce a very simple mechanism for specifying dynamic information flow policies, flow locks, which specify conditions under which data may be read by a certain actor. The interface between the policy and the code is via instructions which open and close flow locks. We present a type and effect system for an ML-like language with references which permits the completely static verification of flow lock policies, and prove that the system satisfies a semantic security property generalising noninterference. We show that this simple mechanism can represent a number of recently proposed information flow paradigms for declassification.
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
Abadi, M., Banerjee, A., Heintze, N., Riecke, J.: A core calculus of dependency. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 147–160 (January 1999)
Almeida Matos, A., Boudol, G.: On declassification and the non-disclosure policy. In: Proc. IEEE Computer Security Foundations Workshop (June 2005)
Askarov, A., Sabelfeld, A.: Security-typed languages for implementation of cryptographic protocols: A case study. In: di Vimercati, S.d.C., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 197–221. Springer, Heidelberg (2005)
Banerjee, A., Naumann, D.A.: Stack-based access control and secure information flow. Journal of Functional Programming 15(2), 131–177 (2005)
Chong, S., Myers, A.C.: Security policies for downgrading. In: ACM Conference on Computer and Communications Security, pp. 198–209 (October 2004)
Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Comm. of the ACM 20(7), 504–513 (1977)
Hicks, M., Tse, S., Hicks, B., Zdancewic, S.: Dynamic updating of information-flow policies. In: Proc. Foundations of Computer Security Workshop (2005)
Mantel, H., Sands, D.: Controlled downgrading based on intransitive (non)interference. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 129–145. Springer, Heidelberg (2004)
Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 228–241 (January 1999)
Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: Proc. ACM Symp. on Operating System Principles, pp. 129–142 (October 1997)
Myers, A.C., Liskov, B.: Complete, safe information flow with decentralized labels. In: Proc. IEEE Symp. on Security and Privacy, pp. 186–197 (May 1998)
Myers, A.C., Liskov, B.: Protecting privacy using the decentralized label model. ACM Transactions on Software Engineering and Methodology 9(4), 410–442 (2000)
Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification. In: Proc. IEEE Computer Security Foundations Workshop, pp. 172–186 (June 2004)
Pinsky, S.: Absorbing covers and intransitive non-interference. In: Proc. IEEE Symp. On Security and Privacy, pp. 102–113 (May 1995)
Rushby, J.M.: Noninterference, transitivity, and channel-control security policies. Technical Report CSL-92-02, SRI International (1992)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5–19 (2003)
Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proc. IEEE Computer Security Foundations Workshop, pp. 200–214 (July 2000)
Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proc. IEEE Computer Security Foundations Workshop (2005)
Tse, S., Zdancewic, S.: Run-time principals in information-flow type systems. In: Proc. Symposium on Security and Privacy (2004)
Tse, S., Zdancewic, S.: Designing a security-typed language with certificate-based declassification. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 279–294. Springer, Heidelberg (2005)
Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. J. Computer Security 4(3), 167–187 (1996)
Zdancewic, S., Myers, A.C.: Robust declassification. In: Proc. IEEE Computer Security Foundations Workshop, pp. 15–23 (June 2001)
Zheng, L., Myers, A.: Dynamic security labels and noninterference. In: Proc. Workshop on Formal Aspects in Security and Trust (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Broberg, N., Sands, D. (2006). Flow Locks: Towards a Core Calculus for Dynamic Flow Policies. In: Sestoft, P. (eds) Programming Languages and Systems. ESOP 2006. Lecture Notes in Computer Science, vol 3924. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693024_13
Download citation
DOI: https://doi.org/10.1007/11693024_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33095-0
Online ISBN: 978-3-540-33096-7
eBook Packages: Computer ScienceComputer Science (R0)