Skip to main content
SpringerLink
Log in

Information Flow Certificates

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2018 (ICTAC 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11187))

Included in the following conference series:

  • 470 Accesses

Abstract

Information flow analysis investigates the flow of data in applications, checking in particular for flows from private sources to public sinks. Flow- and path-sensitive analyses are, however, often too costly to be performed every time a security-critical application is run. In this paper, we propose a variant of proof carrying code for information flow security. To this end, we develop information flow (IF) certificates which get attached to programs as well as a method for IF certificate validation. We prove soundness of our technique, i.e., show it to be tamper-free. The technique is implemented within the program analysis tool CPAchecker. Our experiments confirm that the use of certificates pays off for costly analysis runs.

This work was partially supported by the German Research Foundation (DFG) within the Collaborative Research Centre “On-The-Fly Computing” (SFB 901).

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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

Notes

  1. 1.

    Relative to the employed analysis.

  2. 2.

    The \(\uplus \)-operation is only defined if \({ {\ell }}'={ {\ell }}''\). For the computation of the equation system \({\mathbb {I}\mathbb {F}}\) the evaluation order of \(\uplus \) is not specified. Hence, it is possible that the two listed abstract states weren’t joined directly.

  3. 3.

    https://sv-comp.sosy-lab.org/2017/.

  4. 4.

    Still, the number of computed states might be much larger.

References

  1. Agrawal, S., Bonakdarpour, B.: Runtime verification of \(k\)-safety hyperproperties in HyperLTL. In: Proceedings of 29th IEEE Computer Security Foundations Symposium, CSF 2016, Lisbon, June/July 2016, pp. 239–252. IEEE CS Press, Washington, DC (2016). https://doi.org/10.1109/csf.2016.24

  2. Albert, E., Arenas, P., Puebla, G.: An incremental approach to abstraction-carrying code. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 377–391. Springer, Heidelberg (2006). https://doi.org/10.1007/11916277_26

    Chapter  Google Scholar 

  3. Albert, E., Arenas-Sánchez, P., Puebla, G., Hermenegildo, M.V.: Reduced certificates for abstraction-carrying code. In: Etalle, S., Truszczynski, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 163–178. Springer, Heidelberg (2006). https://doi.org/10.1007/11799573_14

    Chapter  Google Scholar 

  4. Albert, E., Puebla, G., Hermenegildo, M.: Abstraction-carrying code. In: Baader, F., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3452, pp. 380–397. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32275-7_25

    Chapter  Google Scholar 

  5. Amtoft, T., Banerjee, A.: Information flow analysis in logical form. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 100–115. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27864-1_10

    Chapter  MATH  Google Scholar 

  6. Arzt, S., et al.: FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps. In: Proc. of 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, June 2014, pp. 259–269. ACM Press, New York (2014). https://doi.org/10.1145/2594291.2594299

  7. Assaf, M., Naumann, D.A., Signoles, J., Totel, E., Tronel, F.: Hypercollecting semantics and its application to static analysis of information flow. In: Proceedings of 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, January 2017, pp. 874–887. ACM Press, New York (2017). https://doi.org/10.1145/3009837.3009889

  8. Barthe, G., Crégut, P., Grégoire, B., Jensen, T., Pichardie, D.: The MOBIUS proof carrying code infrastructure. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 1–24. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-92188-2_1

    Chapter  Google Scholar 

  9. Beyer, D.: Software verification with validation of results. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 331–349. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_20

    Chapter  Google Scholar 

  10. Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504–518. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_51

    Chapter  MATH  Google Scholar 

  11. Bidmeshki, M., Makris, Y.: Toward automatic proof generation for information flow policies in third-party hardware IP. In: Proceedings of 2015 IEEE International Symposium on Hardware-Oriented Security and Trust, HOST 2015, Washington, DC, May 2015, pp. 163–168. IEEE CS Press, Washington, DC (2015). https://doi.org/10.1109/hst.2015.7140256

  12. Chaieb, A.: Proof-producing program analysis. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 287–301. Springer, Heidelberg (2006). https://doi.org/10.1007/11921240_20

    Chapter  Google Scholar 

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

  14. Enck, W., et al.: TaintDroid: an information-flow tracking system for realtime privacy monitoring on smartphones. ACM Trans. Comput. Syst. 32(2), 5 (2014). https://doi.org/10.1145/2619091

    Article  Google Scholar 

  15. Finkbeiner, B., Hahn, C., Stenger, M.: EAHyper: satisfiability, implication, and equivalence checking of hyperproperties. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 564–570. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_29

    Chapter  Google Scholar 

  16. Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for model checking HyperLTL and HyperCTL\(^*\). In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30–48. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_3

    Chapter  Google Scholar 

  17. Foley, S.N.: Aggregation and separation as noninterference properties. J. Comput. Sec. 1(2), 159–188 (1992). https://doi.org/10.3233/jcs-1992-1203

    Article  MathSciNet  Google Scholar 

  18. Le Guernic, G., Banerjee, A., Jensen, T., Schmidt, D.A.: Automata-based confidentiality monitoring. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 75–89. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77505-8_7

    Chapter  Google Scholar 

  19. Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Sec. 8(6), 399–422 (2009). https://doi.org/10.1007/s10207-009-0086-1

    Article  Google Scholar 

  20. Horwitz, S., Reps, T.W.: The use of program dependence graphs in software engineering. In: Proceedings of 14th International Conference on Software Engineering, ICSE 1992, Melbourne, May 1992, pp. 392–411. ACM Press, New York (1992). https://doi.org/10.1145/143062.143156

  21. Hunt, S., Sands, D.: On flow-sensitive security types. In: Proceedings of 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, SC, January 2006, pp. 79–90. ACM Press, New York (2006). https://doi.org/10.1145/1111037.1111045

  22. Jakobs, M.-C.: Speed up configurable certificate validation by certificate reduction and partitioning. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 159–174. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22969-0_12

    Chapter  Google Scholar 

  23. Jakobs, M., Wehrheim, H.: Certification for configurable program analysis. In: Proceedings of 2014 International Symposium on Model Cheking for Software, SPIN 2014, San Jose, CA, July 2014, pp. 30–39. ACM Press, New York (2014). https://doi.org/10.1145/2632362.2632372

  24. Jakobs, M.-C., Wehrheim, H.: Compact proof witnesses. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 389–403. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_28

    Chapter  Google Scholar 

  25. Jin, Y., Yang, B., Makris, Y.: Cycle-accurate information assurance by proof-carrying based signal sensitivity tracing. In: Proceedings of 2013 International Symposium on Hardware-Oriented Security and Trust, HOST 2013, Austin, TX, June 2013, pp. 99–106. IEEE CS Press, Washington, DC (2013). https://doi.org/10.1109/hst.2013.6581573

  26. Joshi, R., Leino, K.R.M.: A semantic approach to secure information flow. Sci. Comput. Program. 37(1–3), 113–138 (2000). https://doi.org/10.1016/s0167-6423(99)00024-6

    Article  MathSciNet  MATH  Google Scholar 

  27. Lengauer, T., Tarjan, R.E.: A fast algorithm for finding dominators in a flowgraph. ACM Trans. Program. Lang. Syst. 1(1), 121–141 (1979). https://doi.org/10.1145/357062.357071

    Article  MATH  Google Scholar 

  28. Loidl, H., MacKenzie, K., Jost, S., Beringer, L.: A proof-carrying-code infrastructure for resources. In: Proceedings of 4th Latin-American Symposium on Dependable Computing, LADC 2009, João Pessoa, September 2009, pp. 127–134. IEEE CS Press, Washington, DC (2009). https://doi.org/10.1109/ladc.2009.13

  29. Lortz, S., Mantel, H., Starostin, A., Bähr, T., Schneider, D., Weber, A.: Cassandra: towards a certifying app store for Android. In: Proceedings of 4th ACM Workshop on Security and Privacy in Smartphones and Mobile Devices, SPSM 2014, Scottsdale, AZ, November 2014, pp. 93–104. ACM Press, New York (2014). https://doi.org/10.1145/2666620.2666631

  30. Magazinius, J., Russo, A., Sabelfeld, A.: On-the-fly inlining of dynamic security monitors. Comput. Sec. 31(7), 827–843 (2012). https://doi.org/10.1016/j.cose.2011.10.002

    Article  Google Scholar 

  31. Mantel, H.: On the composition of secure systems. In: Proceedings of 2002 IEEE Symposium on Security and Privacy, S&P 2002, Berkeley, CA, May 2002, pp. 88–101. IEEE CS Press, Washington, DC (2002). https://doi.org/10.1109/secpri.2002.1004364

  32. Necula, G.C.: Proof-carrying code. In: Conference on Record of 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, Paris, January 1997, pp. 106–119. ACM Press, New York (1997). https://doi.org/10.1145/263699.263712

  33. Töws, M., Wehrheim, H.: A CEGAR scheme for information flow analysis. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 466–483. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47846-3_29

    Chapter  Google Scholar 

  34. Töws, M., Wehrheim, H.: Policy dependent and independent information flow analyses. In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 362–378. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68690-5_22

    Chapter  Google Scholar 

  35. Vachharajani, N., et al.: RIFLE: an architectural framework for user-centric information-flow security. In: Proceedings of 37th Annual International Symposium on Microarchitecture, MICRO-37, Portland, OR, December 2004, pp. 243–254. IEEE CS Press, Washington, DC (2004). https://doi.org/10.1109/micro.2004.31

  36. Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Sec. 4(2–3), 167–188 (1996). https://doi.org/10.3233/jcs-1996-42-304

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Paderborn, Warburger Straße 100, 33098, Paderborn, Germany

    Manuel Töws & Heike Wehrheim

Authors
  1. Manuel Töws
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Heike Wehrheim
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Manuel Töws .

Editor information

Editors and Affiliations

  1. Stellenbosch University, Stellenbosch, South Africa

    Bernd Fischer

  2. Reykjavík University, Reykjavik, Iceland

    Tarmo Uustalu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Töws, M., Wehrheim, H. (2018). Information Flow Certificates. In: Fischer, B., Uustalu, T. (eds) Theoretical Aspects of Computing – ICTAC 2018. ICTAC 2018. Lecture Notes in Computer Science(), vol 11187. Springer, Cham. https://doi.org/10.1007/978-3-030-02508-3_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02508-3_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02507-6

  • Online ISBN: 978-3-030-02508-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation