Low-deterministic security for low-nondeterministic programs 1

Abstract

We present a new algorithm, together with a full soundness proof, which guarantees probabilistic noninterference (PN) for concurrent programs. The algorithm follows the “low-deterministic security” (LSOD) approach, but for the first time allows general low-nondeterminism as long as PN is not violated.

The algorithm is based on the earlier observation by Giffhorn and Snelting that low-nondeterminism is secure as long as it is not influenced by high events [International Journal of Information Security 14 (2015) 263–287]. It uses a new system of classification flow equations in multi-threaded programs, together with inter-thread/interprocedural dominators. Compared to LSOD, precision is boosted and false alarms are minimized. We explain details of the new algorithm and its soundness proof.

The algorithm is integrated into the JOANA software security tool, and can handle full Java with arbitrary threads. We apply JOANA to a multi-threaded e-voting system, and show how the algorithm eliminates false alarms. We thus demonstrate that low-deterministic security is a highly precise and practically mature software security analysis method.

Keywords

Software security information flow control probabilistic noninterference program analysis

Get full access to this article

View all access options for this article.

References

Ahrendt,

Beckert,

Bubel,

Hähnle,

P.H.

Schmitt and

Ulbrich (eds), Deductive Software Verification – the Key Book – from Theory to Practice, Lecture Notes in Computer Science, Vol. 10001, Springer, 2016.

Askarov,

Hunt,

Sabelfeld and

Sands, Termination-insensitive noninterference leaks more than just a bit, in: Proc. ESORICS, LNCS, Vol. 5283, 2008, pp. 333–348.

Barthe,

Fournet,

Grégoire,

Strub,

Swamy and

S.Z.

Béguelin, Probabilistic relational verification for cryptographic implementations, in: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, Ca, Usa, January 20–21, 2014, 2014, pp. 193–206.

Breitner,

Graf,

Hecker,

Mohr and

Snelting, On improvements of low-deterministic security, in: Proc. Principles of Security and Trust (POST 2016), Lecture Notes in Computer Science, Vol. 9635, Springer Berlin Heidelberg, 2016, pp. 68–88. doi:10.1007/978-3-662-49635-0_4.

De Sutter,

Van Put and

De Bosschere, A practical interprocedural dominance algorithm, Acm Trans. Program. Lang. Syst. 29(4) (2007).

Giffhorn, Advanced chopping of sequential and concurrent programs, Software Quality Journal 19(2) (2011), 239–294. doi:10.1007/s11219-010-9114-7.

Giffhorn, Slicing of Concurrent Programs and its Application to Information Flow Control, PhD thesis, Karlsruher Institut für Technologie, Fakultät für Informatik, 2012.

Giffhorn and

Snelting, A new algorithm for low-deterministic security, International Journal of Information Security 14(3) (2015), 263–287. doi:10.1007/s10207-014-0257-6.

Graf, Information Flow Control with System Dependence Graphs — Improving Modularity, Scalability and Precision for Object Oriented Languages, PhD thesis, Karlsruher Institut für Technologie, Fakultät für Informatik, 2016.

10.

Graf,

Hecker,

Mohr and

Snelting, Checking applications using security APIs with JOANA, 2015, 8th International Workshop on Analysis of Security APIs.

11.

Graf,

Hecker,

Mohr and

Snelting, Tool demonstration: JOANA, in: Proc. Principles of Security and Trust (POST 2016), Lecture Notes in Computer Science, Vol. 9635, Springer Berlin Heidelberg, 2016, pp. 89–93. doi:10.1007/978-3-662-49635-0_5.

12.

Greiner,

Mohr and

Beckert, Modular verification of information flow security in component-based systems, in: Software Engineering and Formal Methods – 15th International Conference, SEFM 2017, Proceedings, Trento, Italy, September 4–8, 2017, 2017, pp. 300–315.

13.

Hammer, Experiences with PDG-based IFC, in: Proc. ESSoS’10,

Massacci,

Wallach and

Zannone, eds, LNCS, Vol. 5965, Springer-Verlag, 2010, pp. 44–60.

14.

Hammer and

Snelting, Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs, International Journal of Information Security 8(6) (2009), 399–422. doi:10.1007/s10207-009-0086-1.

15.

Horwitz,

Prins and

Reps, On the adequacy of program dependence graphs for representing programs, in: Proc. POPL ’88, ACM, New York, NY, USA, 1988, pp. 146–157. doi:10.1145/73560.73573.

16.

Huisman and

T.M.

Ngo, Scheduler-specific confidentiality for multi-threaded programs and its logic-based verification, in: Proc. Formal Verification of Object-Oriented Systems, 2011.

17.

Huisman,

Worah and

Sunesen, A temporal logic characterisation of observational determinism, in: Proc. 19th CSFW, IEEE, 2006, p. 3.

18.

Hunt and

Sands, On flow-sensitive security types, in: POPL ’06, ACM, 2006, pp. 79–90. doi:10.1145/1111037.1111045.

19.

Küsters,

Scapin,

Truderung and

Graf, Extending and applying a framework for the cryptographic verification of Java programs, in: Proc. POST 2014, LNCS 8424, Springer, 2014, pp. 220–239.

20.

Küsters,

Truderung,

Beckert,

Bruns,

Kirsten and

Mohr, A hybrid approach for proving noninterference of Java programs, in: IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13–17 July, 2015, 2015, pp. 305–319.

21.

Küsters,

Truderung and

Graf, A framework for the cryptographic verification of Java-like programs, in: Computer Security Foundations Symposium (CSF), 2012 IEEE 25th, IEEE Computer Society, 2012.

22.

Li and

Verbrugge, A practical MHP information analysis for concurrent Java programs, in: Proc. LCPC’04, LNCS, Vol. 3602, Springer, 2004, pp. 194–208. doi:10.1007/11532378_15.

23.

Mantel,

Müller-Olm,

Perner and

Wenner, Using dynamic pushdown networks to automate a modular information-flow analysis, in: Pre-Proceedings of the 25th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR), 2015.

24.

Mantel,

Sands and

Sudbrock, Assumptions and guarantees for compositional noninterference, in: Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF), IEEE Computer Society, Cernay-la-Ville, France, 2011, pp. 218–232.

25.

Mantel and

Sudbrock, Flexible scheduler-independent security, in: Computer Security – ESORICS 2010,

Gritzalis,

Preneel and

Theoharidou, eds, Lecture Notes in Computer Science, Vol. 6345, Springer Berlin Heidelberg, 2010, pp. 116–133. ISBN 978-3-642-15496-6. doi:10.1007/978-3-642-15497-3_8.

26.

Mohr,

Graf and

Hecker, 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ärz 2015, CEUR Workshop Proceedings, Vol. 1337, CEUR-WS.org, 2015, pp. 140–145.

27.

Naumovich and

G.S.

Avrunin, A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel, in: Proceedings of the 6th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ACM, New York, NY, USA, 1998, pp. 24–34.

28.

T.M.

Ngo, Qualitative and quantitative information flow analysis for multi-threaded programs, PhD thesis, University of Enschede, 2014.

29.

Popescu,

Hölzl and

Nipkow, Formalizing probabilistic noninterference, in: Certified Programs and Proofs – Third International Conference, CPP 2013, Proceedings, Melbourne, VIC, Australia, December 11–13, 2013, 2013, pp. 259–275.

30.

Popescu,

Hölzl and

Nipkow, Noninterfering schedulers, in: Algebra and Coalgebra in Computer Science,

Heckel and

Milius, eds, Lecture Notes in Computer Science, Vol. 8089, Springer Berlin Heidelberg, 2013, pp. 236–252. doi:10.1007/978-3-642-40206-7_18.

31.

Reps,

Horwitz,

Sagiv and

Rosay, Speeding up slicing, in: Proc. FSE ’94, ACM, New York, NY, USA, 1994, pp. 11–20.

32.

A.W.

Roscoe,

Woodcock and

Wulf, Non-interference through determinism, in: ESORICS, LNCS, Vol. 875, 1994, pp. 33–53.

33.

Sabelfeld and

Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communications 21(1) (2003), 5–19. doi:10.1109/JSAC.2002.806121.

34.

Sabelfeld and

Sands, Probabilistic noninterference for multi-threaded programs, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop, CSFW ’00 Cambridge, England, UK, July 3–5, 2000, 2000, pp. 200–214.

35.

Smith, Improved typings for probabilistic noninterference in a multi-threaded language, J. Comput. Secur. 14(6) (2006), 591–623. doi:10.3233/JCS-2006-14605.

36.

Smith and

Volpano, Secure information flow in a multi-threaded imperative language, in: Proc. POPL ’98, ACM, 1998, pp. 355–364. doi:10.1145/268946.268975.

37.

Snelting, Combining slicing and constraint solving for validation of measurement software, in: SAS ’96: Proceedings of the Third International Symposium on Static Analysis, Springer-Verlag, London, UK, 1996, pp. 332–348.

38.

Snelting,

Giffhorn,

Graf,

Hammer,

Hecker,

Mohr and

Wasserrab, Checking probabilistic noninterference using JOANA, It – Information Technology 56 (2014), 280–287. doi:10.1515/itit-2014-1051.

39.

Snelting,

Robschink and

Krinke, Efficient path conditions in dependence graphs for software safety analysis, ACM Trans. Softw. Eng. Methodol. 15(4) (2006), 410–457. doi:10.1145/1178625.1178628.

40.

Wasserrab,

Lohner and

Snelting, On PDG-based noninterference and its modular proof, in: Proc. PLAS ’09, ACM, 2009.

41.

Zdancewic and

A.C.

Myers, Observational determinism for concurrent program security, in: Proc. CSFW, IEEE, 2003, pp. 29–43.