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.
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).
- 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.