Top

Published in:

2018 | OriginalPaper | Chapter

A Uniform Information-Flow Security Benchmark Suite for Source Code and Bytecode

Authors : Tobias Hamann, Mihai Herda, Heiko Mantel, Martin Mohr, David Schneider, Markus Tasch

Published in: Secure IT Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

It has become common practice to formally verify the correctness of information-flow analyses wrt. noninterference-like properties. An orthogonal problem is to ensure the correctness of implementations of such analyses. In this article, we propose the benchmark suite IFSpec, which provides sample programs for checking that an information-flow analyzer correctly classifies them as secure or insecure. Our focus is on the Java and Android platforms, and IFSpec supports Java source code, Java bytecode, and Dalvik bytecode. IFSpec is structured into categories that address multiple types of information leakage. We employ IFSpec to validate and compare four information-flow analyzers: Cassandra, Joana, JoDroid, and KeY. IFSpec is based on RIFL, the RS\(^3\) Information-Flow Specification Language, and is open to extensions.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Protecting Instruction Set Randomization from Code Reuse Attacks

next chapter When Harry Met Tinder: Security Analysis of Dating Apps on Android

The benchmark suite, including all samples, evaluation results, the benchmarked tools, information how to run information-flow analyzers on IFSpec, and how to contribute to IFSpec is available under www.spp-rs3.de/IFSpec.

HPE Security Fortify Static Code Analyzer (SCA). https://saas.hpe.com/en-us/software/sca. Accessed 8 Aug 2018

IBM Security AppScan. https://www.ibm.com/developerworks/downloads/r/appscan/index.html. Accessed 8 Aug 2018

SDK Platform Release Notes. https://developer.android.com/studio/releases/platforms.html. Accessed 8 Aug 2018

Ahrendt, W., et al.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55–71. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12154-3_4CrossRef

The Activity Lifecycle of Android. https://developer.android.com/guide/components/activities/activity-lifecycle.html. Accessed 8 Aug 2018

Arzt, S., et al.: FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps. In: PLDI 2014, pp. 259–269 (2014)CrossRef

Balyo, T., Heule, M.J., Järvisalo, M.: SAT competition 2016: recent developments. In: AAAI 2017, pp. 5061–5063 (2017)

Bauereiß, T., et al.: RIFL 1.1: a common specification language for information-flow requirements. Technical report TUD-CS-2017-0225, TU Darmstadt (2017)

Beckert, B., Bruns, D., Klebanov, V., Scheben, C., Schmitt, P.H., Ulbrich, M.: Information flow in object-oriented software. In: Gupta, G., Peña, R. (eds.) LOPSTR 2013. LNCS, vol. 8901, pp. 19–37. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-14125-1_2CrossRef

10.

Bischof, S., Breitner, J., Graf, J., Hecker, M., Mohr, M., Snelting, G.: Low-deterministic security for low-deterministic programs. J. Comput. Secur. 26, 335–336 (2018)CrossRef

11.

Blackburn, S.M., et al.: The DaCapo benchmarks: Java benchmarking development and analysis. In: OOPSLA 2006, pp. 169–190 (2006)

12.

Breitner, J., Graf, J., Hecker, M., Mohr, M., Snelting, G.: On improvements of low-deterministic security. In: Piessens, F., Viganò, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 68–88. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49635-0_4CrossRef

13.

Bull, J.M., Smith, L.A., Westhead, M.D., Henty, D.S., Davey, R.A.: A benchmark suite for high performance Java. In: JAVA 1999, pp. 81–88 (1999)

14.

Cohen, E.S.: Information transmission in sequential programs. In: Foundations of Secure Computation, pp. 297–335 (1978)

15.

Cok, D.R., Déharbe, D., Weber, T.: The 2014 SMT competition. J. Satisf. Boolean Model. Comput. 9, 207–242 (2016)MathSciNet

16.

S. P. E. Corporation. Spec CPU Benchmarks. https://www.spec.org/benchmarks.html#cpu. Accessed Apr 8 Aug 2018

17.

Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)MathSciNetCrossRef

18.

Feiertag, R.J., Levitt, K.N., Robinson, L.: Proving multilevel security of a system design. In: SOSP 1977, pp. 57–65 (1977)

19.

Fritz, C., Arzt, S., Rasthofer, S.: DroidBench 2.0. https://github.com/secure-software-engineering/DroidBench. Accessed 8 Aug 2018

20.

Goguen, J.A., Meseguer, J.: Security policies and security models. In: S&P 1982, pp. 11–20 (1982)

21.

Graf, J., Hecker, M., Mohr, M.: Using JOANA for information flow control in Java programs - a practical guide. In: ATPS 2013, pp. 123–138 (2013)

22.

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)CrossRef

23.

Hara, Y., Tomiyama, H., Honda, S., Takada, H., Ishii, K.: CHStone: a benchmark program suite for practical C-based high-level synthesis. In: ISCAS 2008, pp. 1192–1195 (2008)

24.

Henning, J.L.: SPEC CPU2000: measuring CPU performance in the New Millennium. Computer 33(7), 28–35 (2000)CrossRef

25.

Hoos, H.H., Stützle, T.: SATLIB: an online resource for research on SAT. In: Sat 2000: highlights of satisfiability research in the year 2000, pp. 283–292 (2000)

26.

Ku, K., Hart, T.E., Chechik, M., Lie, D.: A buffer overflow benchmark for software model checkers. In: ASE 2007, pp. 389–392 (2007)

27.

Lortz, S., Mantel, H., Starostin, A., Bähr, T., Schneider, D., Weber, A.: Cassandra: towards a certifying app store for Android. In: SPSM 2014, pp. 93–104 (2014)

28.

Lux, A., Mantel, H.: Declassification with explicit reference points. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 69–85. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04444-1_5CrossRef

29.

Lux, A., Mantel, H.: Who can declassify? In: FAST 2009, pp. 35–49 (2009)CrossRef

30.

Mantel, H.: Information flow and noninterference. In: van Tilborg, H.C.A., Jajodia, S. (eds.) Encyclopedia of Cryptography and Security, 2nd edn., pp. 605–607. Springer, New York (2011)

31.

Millen, J.K.: Information flow analysis of formal specifications. In: S&P 1981, pp. 3–8 (1981)

32.

Mohr, M., Graf, J., Hecker, M.: JoDroid: adding android support to a static information flow control tool. In: SE 2015, pp. 140–145 (2015)

33.

Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification. In: CSFW 2004, pp. 172–186 (2004)

34.

Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: Jif 3.0: Java Information Flow. http://www.cs.cornell.edu/jif. Accessed 8 Aug 2018

35.

Pelánek, R.: BEEM: benchmarks for explicit model checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73370-6_17CrossRef

36.

Rushby, J.M.: Design and verification of secure systems. In: Proceedings of the Eighth ACM Symposium on Operating System Principles, pp. 12–21 (1981)

37.

Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 174–191. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-37621-7_9CrossRef

38.

Sim, S.E., Easterbrook, S., Holt, R.C.: Using benchmarking to advance research: a challenge to software engineering. In: ICSE 2003, pp. 74–83 (2003)

39.

Smith, L.A., Bull, J.M., Obdrizalek, J.: A parallel Java grande benchmark suite. In: SC 2001, p. 8 (2001)

40.

Stanford SecuriBench. http://suif.stanford.edu/~livshits/work/securibench/intro.html. Accessed 8 Aug 2018

41.

SecuriBench Micro. https://github.com/too4words/securibench-micro. Accessed 8 Aug 2018

42.

Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–361 (2009)MathSciNetCrossRef

43.

Sutcliffe, G., Schulz, S., Claessen, K., Van Gelder, A.: Using the TPTP language for writing derivations and finite interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 67–81. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_7CrossRef

44.

Wasserrab, D., Lohner, D.: Proving information flow noninterference by reusing a machine-checked correctness proof for slicing. In: VERIFY 2010

45.

Zanioli, M., Ferrara, P., Cortesi, A.: SAILS: static analysis of information leakage with sample. In: SAC 2012, pp. 1308–1313 (2012)

Title: A Uniform Information-Flow Security Benchmark Suite for Source Code and Bytecode
Authors: Tobias Hamann
Mihai Herda
Heiko Mantel
Martin Mohr
David Schneider
Markus Tasch
Publisher: Springer International Publishing
Book: Secure IT Systems
Print ISBN: 978-3-030-03637-9

Electronic ISBN: 978-3-030-03638-6

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-030-03638-6_27

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner