Solvers for Security

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.

Relevant Publications

On Voting Machine Design for Verification and Testability
Cynthia Sturton, Susmit Jha, Sanjit A. Seshia, and David Wagner
In ACM Conference on Computer and Communications Security (CCS), November 2009.

 
Effective Blame for Information-Flow Violations
Dave King, Trent Jaeger, Somesh Jha, and Sanjit A. Seshia
In ACM Conference on Foundations of Software Engineering (FSE), November 2008.

 
Deciding Bit-Vector Arithmetic with Abstraction
Randal E. Bryant, Daniel Kroening, Joel Ouaknine, Sanjit A. Seshia, Ofer Strichman, and Bryan Brady.
In 13th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), March 2007.

 
Semantics-Aware Malware Detection.
Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Song, and Randal E. Bryant.
IEEE Symposium on Security and Privacy, Oakland, May 2005, pages 32-46.

 

 Software

Beaver SMT solver
Solver for Information-Flow Constraints

 Support

This project receives generous support from the National Science Foundation (NSF CyberTrust grant CNS-0627734), Microsoft Research, and an equipment grant from Intel.

 
  Sanjit A. Seshia, last updated August 2010.