| Title | Taint Analysis of Security Code in the KLEE Symbolic Execution Engine |
| Publication Type | Conference Paper |
| Year of Publication | 2012 |
| Authors | Corin, R, Manzano, FA |
| Editor | Chim, TW, Yuen, TH |
| Conference Name | Information and Communications Security - 14th International Conference, ICICS 2012, Hong Kong, China, October 29-31, 2012. Proceedings |
| ISBN Number | 978-3-642-34128-1 |
| 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. |
| DOI | 10.1007/978-3-642-34129-8_23 |
