Abstract
We analyse the security of code by extending the KLEE symbolic execution engine with a tainting mechanism that tracks information flows of data. We consider both simple flows from direct assignment operations, and (more subtle) indirect flows inferred from the control flow. Our mechanism prevents overtainting by using a region-based static analysis provided by LLVM, the compiler infrastructure machine on which KLEE runs. We rigorously define taint propagation in a formal LLVM intermediate representation semantics, and show the correctness of our method. We illustrate the mechanism with several examples, showing how we use tainting to prove confidentiality and integrity properties.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Barthe, G., Rezk, T.: Non-interference for a jvm-like language. In: TLDI 2005, pp. 103–112. ACM, New York (2005)
Brumley, D., Caballero, J., Liang, Z., Newsome, J., Song, D.: Towards automatic discovery of deviations in binary implementations with applications to error detection and fingerprint generation. In: USENIX, SS 2007, pp. 15:1–15:16. USENIX Association, Berkeley (2007)
Cadar, C., Dunbar, D., Engler, D.R.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of OSDI, pp. 209–224 (2008)
Corin, R., Manzano, F.: Dynamic taint analysis for the klee symbolic execution engine (extended version), http://cs.famaf.unc.edu.ar/~rcorin/kleecrypto
Corin, R., Manzano, F.: Efficient Symbolic Execution for Analysing Cryptographic Protocol Implementations. In: Erlingsson, Ú., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol. 6542, pp. 58–72. Springer, Heidelberg (2011)
Ganesh, V., Dill, D.L.: A Decision Procedure for Bit-Vectors and Arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007)
Johnson, R., Pearson, D., Pingali, K.: The program structure tree: Computing control regions in linear time, pp. 171–185 (1994)
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)
Lattner, C., Adve, V.: The LLVM language reference manual, http://llvm.org/docs/LangRef.html
Rizzo, J., Duong, T.: Practical padding oracle attacks. In: Proceedings of the 4th USENIX Conference on Offensive Technologies, WOOT 2010, pp. 1–8. USENIX Association, Berkeley (2010)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE JSAC 21(1), 5–19 (2003)
Schwartz, E.J., Avgerinos, T., Brumley, D.: All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask) (2010)
Vaudenay, S.: Security Flaws Induced by CBC Padding - Applications to SSL, IPSEC, WTLS... In: Knudsen, L.R. (ed.) EUROCRYPT 2002. LNCS, vol. 2332, pp. 534–546. Springer, Heidelberg (2002)
Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the llvm intermediate representation for verified program transformations. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 427–440. ACM, New York (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Corin, R., Manzano, F.A. (2012). Taint Analysis of Security Code in the KLEE Symbolic Execution Engine. In: Chim, T.W., Yuen, T.H. (eds) Information and Communications Security. ICICS 2012. Lecture Notes in Computer Science, vol 7618. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34129-8_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-34129-8_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34128-1
Online ISBN: 978-3-642-34129-8
eBook Packages: Computer ScienceComputer Science (R0)