Abstract
Low-security observable determinism (LSOD), as introduced by Roscoe and Zdancewic [18, 24], is the simplest criterion which guarantees probabilistic noninterference for concurrent programs. But LSOD prohibits any, even secure low-nondeterminism. Giffhorn developed an improvement, named RLSOD, which allows some secure low-nondeterminism, and can handle full Java with high precision [5].
In this paper, we describe a new generalization of RLSOD. By applying aggressive program analysis, in particular dominators for multi-threaded programs, precision can be boosted and false alarms minimized. We explain details of the new algorithm, and provide a soundness proof. The improved RLSOD is integrated into the JOANA tool; a case study is described. We thus demonstrate that low-deterministic security is a highly precise and practically mature software security analysis method.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
A more detailed discussion of IFC attacker models can be found in e.g. [5]. Note that JOANA allows arbitrary lattices of security classifications, not just the simple \(\bot =L\le H=\top \) lattice. Note also that integrity is dual to confidentiality, but will not be discussed here. JOANA can handle both.
- 2.
That is, 2’ as in [4] holds; the slightly less precise, but simpler 2’ condition in the current paper is violated, but 3’ as defined in the current paper holds. We thank C. Hammer and his students for this subtle observation.
- 3.
In programs with procedures and threads, immediate dominators may not be unique due to context-sensitivity [2]. Likewise, the dominator definition must be extended if the same thread can be spawned several times. Both issues are not discussed here.
- 4.
In case n was manually classified low, a trivial explicit leak has been discovered. Same for the standard flow equation [7].
- 5.
Note that in case of dynamically created threads, the definition of common dominator must be extended, such that the static cdom lies before all dynamically possible spawns. This extension for dynamic threads is not covered by definition 4, but implemented in JOANA. JOANA also handles interprocedural, context-sensitive dominators.
References
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)
De Sutter, B., Van Put, L., De Bosschere, K.: A practical interprocedural dominance algorithm. ACM Trans. Program. Lang. Syst. 29(4), 19 (2007)
Gawlitza, T.M., Lammich, P., Müller-Olm, M., Seidl, H., Wenner, A.: Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 199–213. Springer, Heidelberg (2011)
Giffhorn, D.: Slicing of concurrent programs and its application to information flow control. Ph.D. thesis, Karlsruher Institut für Technologie, Fakultät für Informatik, May 2012
Giffhorn, D., Snelting, G.: A new algorithm for low-deterministic security. Int. J. Inf. Secur. 14(3), 263–287 (2015)
Graf, J., Hecker, M., Mohr, M., Snelting, G.: Checking applications using security APIs with JOANA. In: 8th International Workshop on Analysis of Security APIs. http://www.dsi.unive.it/focardi/ASA8/
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)
Horwitz, S., Prins, J., Reps, T.: On the adequacy of program dependence graphs for representing programs. In: Proceedings POPL 1988. pp. 146–157. ACM, New York, NY, USA (1988)
Huisman, M., Ngo, T.: Scheduler-specific confidentiality for multi-threaded programs and its logic-based verification. In: Proceedings Formal Verification of Object-Oriented Systems (2011)
Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of observational determinism. In: Proceedings of the 19th CSFW, pp. 3. IEEE (2006)
Küsters, R., Scapin, E., Truderung, T., Graf, J.: Extending and applying a framework for the cryptographic verification of java programs. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 220–239. Springer, Heidelberg (2014)
Küsters, R., Truderung, T., Graf, J.: A framework for the cryptographic verification of Java-like programs. In: 2012 IEEE 25th Symposium on Computer Security Foundations (CSF). IEEE Computer Society (2012)
Mantel, H., Sudbrock, H.: Flexible Scheduler-independent security. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 116–133. Springer, Heidelberg (2010)
Mohr, M., Graf, J., Hecker, M.: JoDroid: adding android support to a static information flow control tool. In: Gemeinsamer Tagungsband der Workshops der Tagung Software Engineering 2015, Dresden, Germany, 17–18 Mäarz 2015, vol. 1337, pp. 140–145, CEUR Workshop Proceedings. CEUR-WS.org (2015)
Ngo, T.M.: Qualitative and quantitative information flow analysis for multi-threaded programs. Ph.D. thesis, University of Enschede (2014)
Popescu, A., Hölzl, J., Nipkow, T.: Formalizing probabilistic noninterference. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 259–275. Springer, Heidelberg (2013)
Popescu, A., Hölzl, J., Nipkow, T.: Noninterfering schedulers. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 236–252. Springer, Heidelberg (2013)
Roscoe, A.W., Woodcock, J.C.P., Wulf, L.: Non-interference through determinism. In: Gollmann, Dieter (ed.) ESORICS 1994. LNCS, vol. 875. Springer, Heidelberg (1994)
Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW 2000) 3–5 July 2000, Cambridge, pp. 200–214 (2000)
Smith, G.: Improved typings for probabilistic noninterference in a multi-threaded language. J. Comput. Secur. 14(6), 591–623 (2006). http://iospress.metapress.com/content/4wt8erpe5eqkc0df
Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: Proceedings of POPL 1998, pp. 355–364. ACM, January 1998
Snelting, G.: Combining slicing and constraint solving for validation of measurement software. In: Cousot, Radhia, Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145. Springer, Heidelberg (1996)
Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. ACM Trans. Softw. Eng. Methodol. 15(4), 410–457 (2006)
Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings CSFW, pp. 29–43. IEEE (2003)
Acknowledgements
This work was partially supported by Deutsche Forschungsgemeinschaft in the scope of SPP “Reliably Secure Software Systems”, and by BMBF in the scope of the KASTEL project.
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
Breitner, J., Graf, J., Hecker, M., Mohr, M., Snelting, G. (2016). On Improvements of Low-Deterministic Security. 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_4
Download citation
DOI: https://doi.org/10.1007/978-3-662-49635-0_4
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)
