Sanitizer validation using symbolic execution and library cross-checking


The goal of this project is to analyze sanitization libraries in seek of vulnerabilities. More specifically, we want to find inputs that reveal vulnerabilities in existing sanitization functions. Our contribution is twofold: (1) we want to find spec-violating inputs for the sanitization function and (2) report vulnerabilities not covered by the current library.


student: Mateus Araujo Borges <MateusAraujoBorges AT>

mentor: Marcelo d'Amorim

co-mentor: Corina Pasareanu


The sources for this project are available from a Mercurial repository at TBD


Project documentation/wiki/blog are available at TBD

Last modified 6 years ago Last modified on 04/25/2012 12:41:31 PM