ISSTAC: Integrated Symbolic Execution for Space-Time Analysis of Code

Seminar
Wednesday, May 25, 2016
5:00 AM to 6:00 AM
POB 2.302
Free and open to the public

Attacks relying on the inherent space-time complexity of algorithms implemented by software systems are gaining prominence. Software systems are vulnerable to such attacks if an adversary can inexpensively generate inputs that cause the system to consume an impractically large amount of time or space to process those inputs, thus denying service to benign users or otherwise  disabling the system. The adversary can also use the same inputs to mount side-channel attacks that aim to infer some secret from the observed space-time system behavior.
 
Our project, ISSTAC: Integrated Symbolic Execution for Space-Time Analysis of Code, aims to develop automated analysis techniques and implement them in an industrial-strength tool that allows the efficient analysis of software (in the form of Java bytecode) with respect to space-time complexity vulnerabilities. The analysis is based on symbolic execution, a well-known analysis technique that systematically explores program execution paths and also generates inputs that trigger those paths. We are building a cloud-based symbolic execution engine for Java that includes new and improved algorithms for the symbolic space-time complexity and side-channel analysis of programs and a novel model counting constraint solver needed for quantifying the analysis results.
 
This is a 4-year DARPA funded collaborative project between Vanderbilt University, CMU, UC Santa Barbara and Queen Mary University, London. The project will build upon existing and mature symbolic execution tools (Symbolic PathFinder from NASA ARC). I will give an overview of the project and highlight recent advancements developed on the CMU side. The ISSTAC website is: https://www.cmu.edu/silicon-valley/research/isstac/index.html
 

x x

Speaker

Corina Pasareanu

Corina Pasareanu

NASA Ames Research Center

Corina Pasareanu is a researcher at NASA Ames, in the Robust Software Engineering group. She is employed by Carnegie Mellon University, at the Silicon Valley campus. At Ames she is developing and extending Symbolic PathFinder, a symbolic execution tool for Java bytecode. Her research interests include: Model checking and automated testing, Compositional verification, Model-based development, Probabilistic software analysis, Autonomy and Security. She was Program/General Chair for several conferences including: International Conference on Computer Aided Verification (CAV 2015), International Symposium on Software Testing and Analysis (ISSTA 2014), International Conference on Automated Software Engineering (ASE 2011), NASA Formal Methods Symposium (NFM 2009). She is the recipient of a best paper award (HVC 2014), an ACM Impact Paper Award (2010), the ICSE 2010 Most Influential Paper Award, the IBM HVC Conference Award (2007) and an ACM Distinguished Paper Award (2002). She is currently Associate Editor for the IEEE Transactions on Software Engineering (TSE) journal.