2008 Research Summary

SMT Solver for Security

View Current Project Information

Susmit Kumar Jha and Sanjit A. Seshia

Satisfiability solvers have become a critical component of most static and dynamic techniques for program analysis. We are exploring the use of satisfiability modulo theory (SMT) solving techniques beyond their conventional use as satisfiability oracles to generate better debugging information and facilitating automated repair. We are also developing specialized satisfiability solving techniques geared towards applications in security that can reason over hard satisfiability problems generated during the analysis of malicious but obfuscated code. In order to build such decision procedures which can scale to real-life problems, we combine scalable randomized algorithms with traditional solver techniques to deal with adversarially created hard problems which are not efficiently handled by existing satisfiability solvers.