Abstract
Security policies are naturally dynamic. Reflecting this, there has been a growing interest in studying information-flow properties which change during program execution, including concepts such as declassification, revocation, and role-change.
A static verification of a dynamic information flow policy, from a semantic perspective, should only need to concern itself with two things: 1) the dependencies between data in a program, and 2) whether those dependencies are consistent with the intended flow policies as they change over time. In this paper we provide a formal ground for this intuition. We present a straightforward extension to the principal flow-sensitive type system introduced by Hunt and Sands (POPL ’06, ESOP ’11) to infer both end-to-end dependencies and dependencies at intermediate points in a program. This allows typings to be applied to verification of both static and dynamic policies. Our extension preserves the principal type system’s distinguishing feature, that type inference is independent of the policy to be enforced: a single, generic dependency analysis (typing) can be used to verify many different dynamic policies of a given program, thus achieving a clean separation between (1) and (2).
We also make contributions to the foundations of dynamic information flow. Arguably, the most compelling semantic definitions for dynamic security conditions in the literature are phrased in the so-called knowledge-based style. We contribute a new definition of knowledge-based progress insensitive security for dynamic policies. We show that the new definition avoids anomalies of previous definitions and enjoys a simple and useful characterisation as a two-run style property.
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
Amtoft, T., Banerjee, A.: Information Flow Analysis in Logical Form. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 100–115. Springer, Heidelberg (2004)
Askarov, A., Chong, C.: Learning is change in knowledge: Knowledge-based security for dynamic policies. In: Computer Security Foundations Symposium, pp. 308–322. IEEE (2012)
Askarov, A., Hunt, S., Sabelfeld, A., Sands, D.: Termination-Insensitive Noninterference Leaks More Than Just a Bit. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 333–348. Springer, Heidelberg (2008)
Andrews, G.R., Reitman, R.P.: An axiomatic approach to information flow in programs. TOPLAS 2(1), 56–75 (1980)
Askarov, A., Sabelfeld, A.: Gradual release: Unifying declassification, encryption and key release policies. In: Proc. IEEE Symp. on Security and Privacy, pp. 207–221 (May 2007)
Banâtre, J.-P., Bryce, C., Le Métayer, D.: Compile-time detection of information flow in sequential programs. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, pp. 55–73. Springer, Heidelberg (1994)
Balliu, M., Dam, M., Le Guernic, G.: Epistemic temporal logic for information flow security. In: Programming Languages and Analysis for Security, PLAS 2011, pp. 6:1–6:12. ACM (2011)
Balliu, M., Dam, M., Le Guernic, G.: Encover: Symbolic exploration for information flow security. In: 2012 IEEE 25th Computer Security Foundations Symposium (CSF), pp. 30–44. IEEE (2012)
Banerjee, A., Naumann, D., Rosenberg, S.: Expressive declassification policies and modular static enforcement. In: Proc. IEEE Symp. on Security and Privacy, pp. 339–353. IEEE Computer Society (2008)
Broberg, N., David, S.: Flow-Sensitive Semantics for Dynamic Information Flow Policies. In: Programming Languages and Analysis for Security (2009)
Broberg, N., Sands, D.: Paralocks – role-based information flow control and beyond. In: Symposium on Principles of Programming Languages. ACM (2010)
Broberg, N., van Delft, B., Sands, D.: Paragon for Practical Programming with Information-Flow Control. In: Shan, C.-c. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 217–232. Springer, Heidelberg (2013)
Clark, D., Hankin, C., Hunt, S.: Information flow for Algol-like languages. Journal of Computer Languages 28(1), 3–28 (2002)
Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Comm. of the ACM 20(7), 504–513 (1977)
van Delft, B., Hunt, S., Sands, D.: Very Static Enforcement of Dynamic Policies. Technical Report 1501.02633, arXiv (2015)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, April 1982, pp. 11–20 (April 1982)
Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: Proc. IEEE Symp. on Security and Privacy, pp. 75–86 (April 1984)
Hunt, S., Sands, D.: On Flow-sensitive Security Types. In: Symposium on Principles of Programming Languages, pp. 79–90. ACM (2006)
Hunt, S., Sands, D.: From Exponential to Polynomial-Time Security Typing via Principal Types. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 297–316. Springer, Heidelberg (2011)
Hicks, M., Tse, S., Hicks, B., Zdancewic, S.: Dynamic updating of information-flow policies. In: Foundations of Computer Security Workshop, pp. 7–18 (2005)
Indus homepage, http://indus.projects.cis.ksu.edu/ (accessed: January 09, 2015)
JOANA homepage, http://pp.ipd.kit.edu/projects/joana/ (accessed: January 09, 2015)
Swamy, N., Hicks, M., Tse, S., Zdancewic, S.: Managing Policy Updates in Security-Typed Languages. In: Proceedings of the 19th IEEE Workshop on Computer Security Foundations (2006)
Stefan, D., Russo, A., Mitchell, J.C., Mazières, D.: Flexible dynamic information flow control in Haskell. In: Proceedings of the 4th ACM Symposium on Haskell (2011)
Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. J. Computer Security 4(3), 167–187 (1996)
Zhang, C.: Conditional Information Flow Policies and Unwinding Relations. In: Bruni, R., Sassone, V. (eds.) TGC 2011. LNCS, vol. 7173, pp. 227–241. Springer, Heidelberg (2012)
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
van Delft, B., Hunt, S., Sands, D. (2015). Very Static Enforcement of Dynamic Policies. 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_3
Download citation
DOI: https://doi.org/10.1007/978-3-662-46666-7_3
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)