@conference {49,
	title = {Taint Analysis of Security Code in the KLEE Symbolic Execution Engine},
	booktitle = { 2012 International Conference on Information and Communications Security (ICICS)},
	year = {2012},
	month = {10/2012},
	publisher = {LNCS},
	organization = {LNCS},
	address = {Hong Kong},
	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.},
	author = {Corin, Ricardo and Manzano, Felipe}
}