Skip to main content

Inferring Secrets by Guided Experiments

  • Conference paper
  • First Online:

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

Abstract

A program has secure information flow if it does not leak any secret information to publicly observable output. A large number of static and dynamic analyses have been devised to check programs for secure information flow. In this paper, we present an algorithm that can carry out a systematic and efficient attack to automatically extract secrets from an insecure program. The algorithm combines static analysis and dynamic execution. The attacker strategy learns from past experiments and chooses as its next attack one that promises maximal knowledge gain about the secret. The idea is to provide the software developer with concrete information about the severity of an information leakage.

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

Buying options

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

Learn about institutional subscriptions

Notes

  1. 1.

    www.coin-or.org/Bonmin and projects.coin-or.org/Couenne.

References

  1. Alvim, M., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: 2012 IEEE 25th Computer Security Foundations Symposium (CSF), pp. 265–279, June 2012

    Google Scholar 

  2. Alvim, M.S., Scedrov, A., Schneider, F.B.: When not all bits are equal: worth-based information flow. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 120–139. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54792-8_7

    Chapter  Google Scholar 

  3. Backes, M., Kopf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: 30th Symposium on Security and Privacy, pp. 141–153 (2009)

    Google Scholar 

  4. Benoist, T., Estellon, B., Gardi, F., Megel, R., Nouioua, K.: Localsolver 1.x: a black-box local-search solver for 0–1 programming. 4OR 9, 299–316 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  5. Clark, D., Hunt, S., Malacaria, P.: A static analysis for quantifying information flow in a simple imperative language. J. Comput. Secur. 15(3), 321–371 (2007)

    Article  Google Scholar 

  6. Clarkson, M.R., Myers, A.C., Schneider, F.B.: Quantifying information flow with beliefs. J. Comput. Secur. 17(5), 655–701 (2009)

    Article  Google Scholar 

  7. 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). doi:10.1007/978-3-540-32004-3_20

    Chapter  Google Scholar 

  8. Do, Q.H., Bubel, R., Hähnle, R.: Exploit generation for information flow leaks in object-oriented programs. In: Federrath, H., Gollmann, D. (eds.) ICT Systems Security and Privacy Protection. IFIPAICT, vol. 455. Springer, Cham (2015). doi:10.1007/978-3-319-18467-8_27

    Chapter  Google Scholar 

  9. Do, Q.H., Bubel, R., Hähnle, R.: Inferring secrets by guided experiments. Technical report, TU Darmstadt (2017)

    Google Scholar 

  10. Gay, D.M.: The AMPL modeling language: an aid to formulating and solving optimization problems. In: Al-Baali, M., Grandinetti, L., Purnama, A. (eds.) Numerical Analysis and Optimization. PROMS, vol. 134. Springer, Cham (2015). doi:10.1007/978-3-319-17689-5_5

    Chapter  Google Scholar 

  11. Hentschel, M., Hähnle, R., Bubel, R.: Visualizing unbounded symbolic execution. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 82–98. Springer, Cham (2014). doi:10.1007/978-3-319-09099-3_7

    Google Scholar 

  12. Heusser, J., Malacaria, P.: Quantifying information leaks in software. In: Proceedings of the 26th Annual Computer Security Applications Conference, pp. 261–269. ACM (2010)

    Google Scholar 

  13. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  14. Klebanov, V.: Precise quantitative information flow analysis–a symbolic approach. Theor. Comput. Sci. 538, 124–139 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  15. Köpf, B., Basin, D.: An information-theoretic model for adaptive side-channel attacks. In: Proceedings of the 14th ACM Conference on Computer and Communications Security, CCS 2007, pp. 286–296. ACM (2007)

    Google Scholar 

  16. Malacaria, P., Chen, H.: Lagrange multipliers and maximum information leakage in different observational models. In: Proceedings of the 3rd ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pp. 135–146. ACM (2008)

    Google Scholar 

  17. Meng, Z., Smith, G.: Calculating bounds on information leakage using two-bit patterns. In: Proceedings of the ACM SIGPLAN 6th Workshop on Programming Languages, Analysis for Security, PLAS 2011, pp. 1:1–1:12. ACM (2011)

    Google Scholar 

  18. Ngo, T.M., Huisman, M.: Quantitative security analysis for programs with low input and noisy output. In: Jürjens, J., Piessens, F., Bielova, N. (eds.) ESSoS 2014. LNCS, vol. 8364, pp. 77–94. Springer, Cham (2014). doi:10.1007/978-3-319-04897-0_6

    Chapter  Google Scholar 

  19. Pasareanu, C.S., Phan, Q., Malacaria, P.: Multi-run side-channel analysis using symbolic execution and Max-SMT. In: IEEE 29th Computer Security Foundations Symposium, CSF 2016, pp. 387–400. IEEE Computer Society (2016)

    Google Scholar 

  20. Phan, Q.-S., Malacaria, P., Tkachuk, O., Păsăreanu, C.S.: Symbolic quantitative information flow. SIGSOFT Softw. Eng. Notes 37(6), 1–5 (2012)

    Article  Google Scholar 

  21. Robling Denning, D.E.: Cryptography and Data Security. Addison-Wesley, Boston (1982)

    MATH  Google Scholar 

  22. Sabelfeld, A., Sands, D.: Declassification: dimensions and principles. J. Comput. Secur. 17(5), 517–548 (2009)

    Article  Google Scholar 

  23. Smith, G.: On the foundations of quantitative information flow. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 288–302. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00596-1_21

    Chapter  Google Scholar 

  24. Verdoolaege, S., Seghir, R., Beyls, K., Loechner, V., Bruynooghe, M.: Counting integer points in parametric polytopes using Barvinok’s rational functions. Algorithmica 48(1), 37–66 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  25. Yasuoka, H., Terauchi, T.: On bounding problems of quantitative information flow. J. Comput. Secur. 19(6), 1029–1082 (2011)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Quoc Huy Do .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Do, Q.H., Bubel, R., Hähnle, R. (2017). Inferring Secrets by Guided Experiments. In: Hung, D., Kapur, D. (eds) Theoretical Aspects of Computing – ICTAC 2017. ICTAC 2017. Lecture Notes in Computer Science(), vol 10580. Springer, Cham. https://doi.org/10.1007/978-3-319-67729-3_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67729-3_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67728-6

  • Online ISBN: 978-3-319-67729-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics