Skip to main content

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

Date:February 29, 2016 
Talk Title:ISSTAC - Integrated Symbolic Execution for Space-Time Analysis of Code
Speaker:Corina Pasareanu
Time & Location:12:00pm - 1:00pm
DEC, CIC Building, Pittsburgh


Attacks relying on the inherent space-time complexity of algorithms used for building software systems are gaining prominence. When an adversary can inexpensively generate inputs that induce behaviors with expensive space-time resource utilization at the defender's end, in addition to mounting denial-of-service attacks, the adversary can also use the same inputs to facilitate side-channel attacks in order to infer some secret from the observed 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 these problems rapidly enough for inclusion in a state-of-the-art development process.

Our idea is to perform the analysis using an improved form of symbolic execution of Java bytecode. Symbolic execution is a powerful code analysis technique that not only implicitly enumerates all program execution paths, but is also capable of constructing the inputs that trigger those paths.

If successful, our project will build the first industrial-strength cloud-based symbolic execution engine for Java that is capable of scaling over hundreds of computing nodes while providing fault-tolerance and data integrity, new and improved algorithms for the symbolic time/space analysis and side-channel analysis of programs, and a novel model counting constraint solver needed for doing this kind of analysis.

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 (the 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:

Speaker Bio

Corina is performing research in software engineering 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 is/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.

Projects at CMU:

  • ISSTAC: Integrated Symbolic Execution for Space-Time Analysis of Code -- CMU PI
    • Funded by DARPA; a collaborative project with Vanderbilt University (the lead) and UC Santa Barbara
  • Mera: Memoized Ranged Systematic Software Analyses — CMU PI
    • Funded by NSF; a collaborative project with UT Austin
  • Circular compositional reasoning by learning and abstraction-refinement —CMU PI
    • Funded by NSF and BSF; a collaborative project with Technion and Tel-Aviv Yaffo.

Additional information can be found on the following website: NASA web profile