Integrated Symbolic Execution for Space-Time Analysis of Code-Silicon Valley Campus - Carnegie Mellon University

Integrated Symbolic Execution for Space-Time Analysis of Code-Silicon Valley Campus - Carnegie Mellon University


Integrated Symbolic Execution for Space-Time Analysis of Code

Cybersecurity is one of the most critical challenges facing the computing discipline. Vulnerabilities that result from space-time usage of programs are especially hard to detect and defend against, since they are due to algorithmic behavior of programs rather than implementation errors. ISSTAC aims to build an integrated approach that provides both qualitative and quantitative reasoning for space-time analysis of Java programs. The approach is based on symbolic execution, a systematic program analysis technique which efficiently explores multiple program behaviors all at once, by manipulating symbolic path conditions collected over program paths.

ISSTAC Overview
click to enlarge or download
Overview slide of ISSTAC; click to download

We are developing two critical ISSTAC components: The Worst-Case Analysis uses heuristics to efficiently search for algorithmic complexity vulnerabilities, and The Side-Channel Analysis uses quantitative information flow analysis to detect and quantify information leakage. The analyses are parameterized with respect to cost models for space-time consumption. Further both analyses produce actual test inputs that expose the vulnerabilities.

This is a 4-year collaborative project, joint with Vanderbilt University, and UC Santa Barbara. The project is funded by DARPA STAC. We build upon existing and mature symbolic execution tools (the Symbolic PathFinder from NASA ARC).

CMU Team

  • Teme Kahsai
  • Rody Kersten
  • Kasper Luckow
  • Pasquale Malacaria (external collaborator)
  • Corina Pasareanu (lead)
  • Quoc-Sang Phan


Corina S. Pasareanu and Quoc-Sang Phan and Pasquale Malacaria “Multi-run side-channel analysis using Symbolic Execution and Max-SMT” in Proceedings of 29th IEEE Computer Security Foundations Symposium, Lisbon, Portugal, 2016.

Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. Pasareanu and Tevfik Bultan. “String Analysis for Side Channels with Segmented Oracles” to appear in Proceedings of 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, Seattle, WA, USA, 2016.