Abstract
The worldwide attention generated by the Heartbleed bug has demonstrated even to the general public the potential devastating consequences of information leaks.
While substantial academic work has been done in the past on information leaks, these works have so far not satisfactorily addressed the challenges of automated analysis of real-world complex C code. On the other hand, effective working solutions rely on ad-hoc principles that have little or no theoretical justification.
The foremost contribution of this paper is to bridge this chasm between advanced theoretical work and concrete practical needs of programmers developing real world software. We present an analysis, based on clear security principles and verification tools, which is largely automatic and effective in detecting information leaks in complex C code running everyday on millions of systems worldwide.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
Here we map guess on the same name whereas we should use different names; it is easy to see this is harmless in this context.
- 3.
Provided these functions don’t leak and return deterministic values. Also if these functions have side-effects these should be deterministic.
- 4.
A soundness proof of this principle for a complex language like C is arguably infeasible and surely beyond the scope of this work.
References
Anderson, P.: Finding heartbleed with codesonar. www.grammatech.com/blog/finding-heartbleed-with-codesonar
Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: 17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004), pp. 100–114. IEEE Computer Society (2004)
Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, pp. 209–224. USENIX Association (2008)
Chou, A.: On detecting heartbleed with static analysis. security.coverity.com/blog/2014/Apr/on-detecting-heartbleed-with-static-analysis.html
Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: DAC 2003, pp. 368–371. ACM (2003)
Coverity. www.coverity.com
Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, pp. 11–20. IEEE Computer Society (1982)
Grammatech. www.grammatech.com/codesonar
Heusser, J., Malacaria, P.: Quantifying information leaks in software. In: Twenty-Sixth Annual Computer Security Applications Conference, pp. 261–269. ACM (2010)
HP/Fortify. saas.hp.com/software/fortify-on-demand
Klokwork. www.klokwork.com
Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014)
Kupsch, J.A., Miller, B.P.: Why do software assurance tools have problems finding bugs like heartbleed? April 2014. continuousassurance.org/swamp/SWAMP-Heartbleed-White-Paper-22Apr2014-current.pdf
de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Business, R.: #339 - Neel Mehta on Heartbleed, Shellshock, October 2014. media.risky.biz/RB339.mp.3
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)
Schneier, B.: Heartbleed, April 2014. www.schneier.com/blog/archives/2014/04/heartbleed.html
Seggelmann, R., Tuexen, M., Williams, M.: Transport layer security (TLS) and datagram transport layer security (DTLS) heartbeat extension. RFC 6520, RFC Editor, February 2012. www.rfc-editor.org/rfc/rfc6520.txt
Smith, G.: Principles of secure information flow analysis. In: Christodorescu, M., Jha, S., Maughan, D., Song, D., Wang, C. (eds.) Malware Detection. Advances in Information Security, vol. 27, pp. 291–307. Springer, Heidelberg (2007)
Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352–367. Springer, Heidelberg (2005)
Valgrind. valgrind.org
Zhang, L., Choffnes, D.R., Levin, D., Dumitras, T., Mislove, A., Schulman, A., Wilson, C.: Analysis of SSL certificate reissues and revocations in the wake of heartbleed. In: Internet Measurement Conference, pp. 489–502. ACM (2014)
Acknowledgments
This research was supported by EPSRC grant EP/K032011/1.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Malacaria, P., Tautchning, M., DiStefano, D. (2016). Information Leakage Analysis of Complex C Code and Its application to OpenSSL. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science(), vol 9952. Springer, Cham. https://doi.org/10.1007/978-3-319-47166-2_63
Download citation
DOI: https://doi.org/10.1007/978-3-319-47166-2_63
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47165-5
Online ISBN: 978-3-319-47166-2
eBook Packages: Computer ScienceComputer Science (R0)