Solvers for Software Reliability and Security
Event details
| Date | 23.07.2010 |
| Hour | 07:00 |
| Speaker | Dr. Vijay Ganesh |
| Location | |
| Category | Conferences - Seminars |
Abstract:
Constraint solvers play a central role in the construction of reliable and secure software, regardless of whether such software is based on formal methods, program analysis, testing or synthesis. In this talk, I will present two solvers namely, STP and HAMPI. STP extends SAT solvers with the theory of bit-vectors and arrays, and has enabled a new testing technique known as Concolic Testing. STP-enabled Concolic testers have been used to find hundreds of previously unknown bugs in Unix utilities, OS kernels, media players, and commercial software, some with approximately a million lines of code. HAMPI is designed for the analysis of string-manipulating programs and incorporates a rich theory of equality over bounded string variables, bounded regular expressions, and context-free grammars. HAMPI has been used to find many unknown SQL injection vulnerabilities in applications with more than 100,000 lines of PHP code using static and dynamic analysis. I will discuss techniques that make these solvers scale to large formulas obtained from real-world applications, and some related theoretical results.
Bio:
Dr. Vijay Ganesh is a Research Scientist at MIT since 2007. He completed his PhD in computer science from Stanford University in 2007, and Bachelor of Technology from College of Engineering, Trivandrum, India. His primary research interests are constraint solvers and their applications to software reliability, computer security and biology. His STP solver was the co-winner of the SMTCOMP competition for bit-vector solvers in 2006, and his paper on HAMPI won the ACM Distinguished Paper Award in 2009.
Links
Practical information
- General public
- Free