Malware (such as viruses, worms, and spyware) pose a significant threat
to our computing infrastructure. Vulnerabilities in widely-used
software can leak secret data and violate system integrity.
There is a pressing need for techniques
for analysis of system security that are fast, accurate, and mostly-automatic.
In this project, we are investigating the use of formal techniques for assurance of system security, based in particular on computational engines such as Boolean satisfiability (SAT) solvers, satisfiability modulo theories (SMT) solvers, and model checkers.
A few sample papers are listed below. For more recent related publications, please follow this link.
SoftwareBeaver SMT solver
Solver for Information-Flow Constraints
SupportThis project receives generous support from the National Science Foundation (NSF CyberTrust grant CNS-0627734), Microsoft Research, and an equipment grant from Intel.