Advertisement

Information Flow Certificates

  • Manuel Töws
  • Heike Wehrheim
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)

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.

References

  1. 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. 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_26CrossRefGoogle Scholar
  3. 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_14CrossRefGoogle Scholar
  4. 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_25CrossRefGoogle Scholar
  5. 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_10CrossRefzbMATHGoogle Scholar
  6. 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. 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. 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_1CrossRefGoogle Scholar
  9. 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_20CrossRefGoogle Scholar
  10. 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_51CrossRefzbMATHGoogle Scholar
  11. 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. 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_20CrossRefGoogle Scholar
  13. 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_20CrossRefGoogle Scholar
  14. 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/2619091CrossRefGoogle Scholar
  15. 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_29CrossRefGoogle Scholar
  16. 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_3CrossRefGoogle Scholar
  17. 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-1203MathSciNetCrossRefGoogle Scholar
  18. 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_7CrossRefGoogle Scholar
  19. 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-1CrossRefGoogle Scholar
  20. 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. 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. 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_12CrossRefGoogle Scholar
  23. 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. 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_28CrossRefGoogle Scholar
  25. 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. 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-6MathSciNetCrossRefzbMATHGoogle Scholar
  27. 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.357071CrossRefzbMATHGoogle Scholar
  28. 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. 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. 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.002CrossRefGoogle Scholar
  31. 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. 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. 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_29CrossRefGoogle Scholar
  34. 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_22CrossRefGoogle Scholar
  35. 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. 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-304CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Institut für InformatikUniversität PaderbornPaderbornGermany

Personalised recommendations