Abstract
In this article, we propose a static information-flow analysis for multi-threaded programs with shared memory communication and synchronization via locks. In contrast to many prior analyses, our analysis does not only prevent information leaks due to synchronization, but can also benefit from synchronization for its precision. Our analysis is a novel combination of type systems and a reachability analysis based on dynamic pushdown networks. The security type system supports flow-sensitive tracking of security levels for shared variables in the analysis of one thread by exploiting assumptions about variable accesses by other threads. The reachability analysis based on dynamic pushdown networks verifies that these assumptions are sound using the result of an automatic guarantee inference. The combined analysis is the first automatic static analysis that supports flow-sensitive tracking of security levels while being sound with respect to termination-sensitive noninterference.
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
Notes
- 1.
We use \(\mathbin {\dot{\cup }}\) to denote the disjoint union of two sets, e.g., \( locks ( {ccnf} ')= locks ( {ccnf} )\mathbin {\dot{\cup }}\{ l \}\) is equivalent to \( locks ( {ccnf} ')=( locks ( {ccnf} )\cup \{ l \})\wedge l \notin locks ( {ccnf} )\).
References
Andrews, G., Reitman, R.: An axiomatic approach to information flow in programs. ACM Trans. Program. Lang. Syst. 2(1), 56–76 (1980)
Arden, O., Chong, S., Liu, J., Myers, A.C., Nystrom, N., Vikram, K., Zdancewic, S., Zhang, D., Zheng, L.: Jif. Software release: http://www.cs.cornell.edu/jif/ (2014)
Askarov, A., Chong, S., Mantel, H.: Hybrid monitors for concurrent noninterference. In: 28th IEEE Computer Security Foundations Symposium, pp. 137–151 (2015)
Askarov, A., Hunt, S., Sabelfeld, A., Sands, D.: Termination-insensitive noninterference leaks more than just a bit. In: 13th European Symposium on Research in Computer Security, pp. 333–348 (2008)
Broberg, N., van Delft, B., Sands, D.: Paragon for practical programming with information-flow control. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 217–232. Springer, Heidelberg (2013)
Giffhorn, D., Snelting, G.: A new algorithm for low-deterministic security. International Journal of Information Security pp. 1–25 (2014)
Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Secur. 8(6), 399–422 (2009)
Huisman, M., Blondeel, H.-C.: Model-checking secure information flow for multi-threaded programs. In: Mödersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 148–165. Springer, Heidelberg (2012)
Lammich, P., Müller-Olm, M., Wenner, A.: Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 525–539. Springer, Heidelberg (2009)
Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: 24th IEEE Computer Security Foundations Symposium, pp. 218–232 (2011)
Mantel, H., Sudbrock, H., Kraußer, T.: Combining different proof techniques for verifying information flow security. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 94–110. Springer, Heidelberg (2007)
Myers, A.C.: JFlow: practical mostly-static information flow control. In: 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 228–241 (1999)
Ngo, T.M., Stoelinga, M., Huisman, M.: Confidentiality for probabilistic multi-threaded programs and its verification. In: Jürjens, J., Livshits, B., Scandariato, R. (eds.) ESSoS 2013. LNCS, vol. 7781, pp. 107–122. Springer, Heidelberg (2013)
Sabelfeld, A.: The impact of synchronisation on secure information flow in concurrent programs. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol. 2244, pp. 225–239. Springer, Heidelberg (2001)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)
Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: 13th IEEE Computer Security Foundations Workshop, pp. 200–214 (2000)
Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 355–364 (1998)
Sudbrock, H.: Compositional and Scheduler-Independent Information Flow Security. Ph.D. thesis, Technische Universität Darmstadt, Germany (2013)
Terauchi, T.: A type system for observational determinism. In: 21st IEEE Computer Security Foundations Symposium, pp. 287–300 (2008)
Vaughan, J., Millstein, T.: Secure information flow for concurrent programs under total store order. In: 25th IEEE Computer Security Foundations Symposium, pp. 19–29 (2012)
Acknowledgments
This work was funded by the DFG under the projects RSCP (MA 3326/4-1/2/3) and IFC4MC (MU 1508/2-1/2/3) in the priority program RS\(^3\) (SPP 1496) and under project OpIAT (MU 1508/1-1/2).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Mantel, H., Müller-Olm, M., Perner, M., Wenner, A. (2015). Using Dynamic Pushdown Networks to Automate a Modular Information-Flow Analysis. In: Falaschi, M. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2015. Lecture Notes in Computer Science(), vol 9527. Springer, Cham. https://doi.org/10.1007/978-3-319-27436-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-27436-2_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-27435-5
Online ISBN: 978-3-319-27436-2
eBook Packages: Computer ScienceComputer Science (R0)