Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Integration of Static and Dynamic Analysis Techniques for Checking Noninterference

  • Chapter
  • First Online:
Deductive Software Verification: Future Perspectives

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12345))

Abstract

In this article, we present an overview of recent combinations of deductive program verification and automatic test generation on the one hand and static analysis on the other hand, with the goal of checking noninterference. Noninterference is the non-functional property that certain confidential information cannot leak to certain public output, i.e., the confidentiality of that information is always preserved.

We define the noninterference properties that are checked along with the individual approaches that we use in different combinations. In one use case, our framework for checking noninterference employs deductive verification to automatically generate tests for noninterference violations with an improved test coverage. In another use case, the framework provides two combinations of deductive verification with static analysis based on system dependence graphs to prove noninterference, thereby reducing the effort for deductive verification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

eBook
USD 15.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 15.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Abadi, A., Ettinger, R., Feldman, Y.A.: Fine slicing. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 471–485. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28872-2_32

    Chapter  Google Scholar 

  2. Agrawal, H.: On slicing programs with jump statements. In: Sarkar, V., Ryder, B.G., Soffa, M.L. (eds.) PLDI 1994, pp. 302–312. ACM (1994). https://doi.org/10.1145/178243.178456

  3. Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book: From Theory to Practice. LNCS, vol. 10001. Springer (2016). https://doi.org/10.1007/978-3-319-49812-6

  4. Ahrendt, W., Gladisch, C., Herda, M.: Proof-based test case generation. In: Ahrendt et al. [3], chap. 12, pp. 415–451. https://doi.org/10.1007/978-3-319-49812-6_12

  5. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. Tech. rep., Department of Computer Science, The University of Iowa (2010), http://smt-lib.org/papers/smt-lib-reference-v2.0-r12.09.09.pdf, www.smt-lib.org

  6. Beckert, B., Bischof, S., Herda, M., Kirsten, M., Kleine Büning, M.: Using theorem provers to increase the precision of dependence analysis for information flow control. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 284–300. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02450-5_17

    Chapter  Google Scholar 

  7. 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_2

    Chapter  Google Scholar 

  8. Darvas, Á., Hähnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193–209. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32004-3_20

    Chapter  Google Scholar 

  9. Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976). https://doi.org/10.1145/360051.360056

    Article  MathSciNet  MATH  Google Scholar 

  10. Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977). https://doi.org/10.1145/359636.359712

    Article  MATH  Google Scholar 

  11. Do, Q.H., Bubel, R., Hähnle, R.: Automatic detection and demonstrator generation for information flow leaks in object-oriented programs. Comput. Secur. 67, 335–349 (2017). https://doi.org/10.1016/j.cose.2016.12.002

    Article  Google Scholar 

  12. Engel, C., Hähnle, R.: Generating unit tests from formal proofs. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 169–188. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73770-4_10

    Chapter  MATH  Google Scholar 

  13. Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. Trans. Program. Lang. Syst. 9(3), 319–349 (1987). https://doi.org/10.1145/24039.24041

    Article  MATH  Google Scholar 

  14. Goguen, J.A., Meseguer, J.: Security policies and security models. In: Symposium on Security and Privacy (S & P), pp. 11–20. IEEE (1982). https://doi.org/10.1109/SP.1982.10014

  15. Gruska, D.P.: Information flow testing. Fundamenta Informaticae 128(1–2), 81–95 (2013). https://doi.org/10.3233/FI-2013-934

    Article  MathSciNet  MATH  Google Scholar 

  16. Hamann, T., Herda, M., Mantel, H., Mohr, M., Schneider, D., Tasch, M.: A uniform information-flow security benchmark suite for source code and bytecode. In: Gruschka, N. (ed.) NordSec 2018. LNCS, vol. 11252, pp. 437–453. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03638-6_27

    Chapter  Google Scholar 

  17. Hammer, C.: Information flow control for Java: a comprehensive approach based on path conditions in dependence graphs. Ph.D. thesis, Karlsruhe Institute of Technology (KIT), Germany (2009). https://doi.org/10.5445/KSP/1000012049

  18. 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). https://doi.org/10.1007/s10207-009-0086-1

    Article  Google Scholar 

  19. Harman, M., Lakhotia, A., Binkley, D.: Theory and algorithms for slicing unstructured programs. Inf. Softw. Technol. 48(7), 549–565 (2006). https://doi.org/10.1016/j.infsof.2005.06.001

    Article  Google Scholar 

  20. Herda, M.: Combining Static and Dynamic Program Analysis Techniques for Checking Relational Properties. Ph.D. thesis, Karlsruhe Institute of Technology (KIT), Germany (2020). https://doi.org/10.5445/IR/1000104496

  21. Herda, M., Tyszberowicz, S., Müssig, J., Beckert, B.: Verification-based test case generation for information-flow properties. In: SAC 2019, pp. 2231–2238. ACM (2019). https://doi.org/10.1145/3297280.3297500

  22. Herda, M., Tyszberowicz, S., Beckert, B.: Using dependence graphs to assist verification and testing of information-flow properties. In: Dubois, C., Wolff, B. (eds.) TAP 2018. LNCS, vol. 10889, pp. 83–102. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92994-1_5

    Chapter  Google Scholar 

  23. Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. Trans. Program. Lang. Syst. 12(1), 26–60 (1990). https://doi.org/10.1145/77606.77608

    Article  Google Scholar 

  24. Hriţcu, C., et al.: Testing noninterference, quickly. J. Funct. Program. 26, 1–62 (2016). https://doi.org/10.1017/S0956796816000058

  25. Küsters, R., Truderung, T., Beckert, B., Bruns, D., Kirsten, M., Mohr, M.: A hybrid approach for proving noninterference of Java programs. In: CSF 2015, pp. 305–319. IEEE (2015). https://doi.org/10.1109/CSF.2015.28

  26. Guernic, G.: Information flow testing. In: Cervesato, I. (ed.) ASIAN 2007. LNCS, vol. 4846, pp. 33–47. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-76929-3_4

    Chapter  Google Scholar 

  27. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes 31(3), 1–38 (2006). https://doi.org/10.1145/1127878.1127884

    Article  Google Scholar 

  28. Milushev, D., Beck, W., Clarke, D.: Noninterference via symbolic execution. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE 2012. LNCS, vol. 7273, pp. 152–168. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30793-5_10

    Chapter  Google Scholar 

  29. de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  30. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003). https://doi.org/10.1109/JSAC.2002.806121

    Article  Google Scholar 

  31. Scheben, C.: Program-level Specification and Deductive Verification of Security Properties. Ph.D. thesis, Karlsruhe Institute of Technology (KIT), Germany (2014). https://doi.org/10.5445/IR/1000046878

  32. Scheben, C., Greiner, S.: Information flow analysis. In: Ahrendt et al. [3], chap. 13, pp. 453–471. https://doi.org/10.1007/978-3-319-49812-6_13

  33. Schmitt, P.H.: First-order logic. In: Ahrendt et al. [3], chap. 2, pp. 23–47. https://doi.org/10.1007/978-3-319-49812-6_2

  34. Snelting, G.: Combining slicing and constraint solving for validation of measurement software. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 332–348. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61739-6_51

    Chapter  Google Scholar 

  35. Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. Trans. Softw. Eng. Methodol. 15(4), 410–457 (2006). https://doi.org/10.1145/1178625.1178628

    Article  Google Scholar 

  36. Wasserrab, D., Lohner, D.: Proving information flow noninterference by reusing a machine-checked correctness proof for slicing. In: Aderhold, M., Autexier, S., Mantel, H. (eds.) VERIFY@IJCAR 2010. EPiC Series in Computing, vol. 3, pp. 141–155. EasyChair (2010). https://doi.org/10.29007/nnzj

Download references

Author information

Authors and Affiliations

  1. Karlsruhe Institute of Technology (KIT), Karlsruhe, Germany

    Bernhard Beckert, Mihai Herda & Michael Kirsten

  2. Afeka Academic College of Engineering, Tel Aviv, Israel

    Shmuel Tyszberowicz

Authors
  1. Bernhard Beckert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mihai Herda
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael Kirsten
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Shmuel Tyszberowicz
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Kirsten .

Editor information

Editors and Affiliations

  1. Chalmers University of Technology, Gothenburg, Sweden

    Wolfgang Ahrendt

  2. Karlsruhe Institute of Technology, Karlsruhe, Germany

    Bernhard Beckert

  3. Technical University of Darmstadt, Darmstadt, Germany

    Richard Bubel

  4. Technical University of Darmstadt, Darmstadt, Germany

    Reiner Hähnle

  5. Karlsruhe Institute of Technology, Karlsruhe, Germany

    Mattias Ulbrich

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Beckert, B., Herda, M., Kirsten, M., Tyszberowicz, S. (2020). Integration of Static and Dynamic Analysis Techniques for Checking Noninterference. In: Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Ulbrich, M. (eds) Deductive Software Verification: Future Perspectives. Lecture Notes in Computer Science(), vol 12345. Springer, Cham. https://doi.org/10.1007/978-3-030-64354-6_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-64354-6_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-64353-9

  • Online ISBN: 978-3-030-64354-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation