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
We are developing two critical
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).
Carnegie Mellon 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.