@inproceedings{3383b9ea9ae647a09138d75fdcd72143,
title = "MACKE: Compositional analysis of low-level vulnerabilities with symbolic execution",
abstract = "Concolic (concrete+symbolic) execution has recently gained popularity as an effective means to uncover non-trivial vulnerabilities in software, such as subtle buffer overows. However, symbolic execution tools that are designed to optimize statement coverage often fail to cover potentially vulnerable code because of complex system interactions and scalability issues of constraint solvers. In this paper, we present a tool (MACKE) that is based on the modular interactions inferred by static code analysis, which is combined with symbolic execution and directed inter-procedural path exploration. This provides an advantage in terms of statement coverage and ability to uncover more vulnerabilities. Our tool includes a novel feature in the form of interactive vulnerability report generation that helps developers prioritize bug fixing based on severity scores. A demo of our tool is available at https://youtu.be/icC3jc3mHEU.",
keywords = "Compositional analysis, Symbolic execution",
author = "Saahil Ognawala and Mart{\'i}n Ochoa and Alexander Pretschner and Tobias Limmer",
note = "Publisher Copyright: {\textcopyright} 2016 ACM.; 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016 ; Conference date: 03-09-2016 Through 07-09-2016",
year = "2016",
month = aug,
day = "25",
doi = "10.1145/2970276.2970281",
language = "English",
series = "ASE 2016 - Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering",
publisher = "Association for Computing Machinery, Inc",
pages = "780--785",
editor = "Sarfraz Khurshid and David Lo and Sven Apel",
booktitle = "ASE 2016 - Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering",
}