Paper Info
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 overflows. 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.
Year
DOI
Venue
2016
10.1145/2970276.2970281
ASE
Keywords
Field
DocType
Symbolic execution, Compositional analysis
Static program analysis,Programming language,Computer science,Software bug,Theoretical computer science,Software,Memory management,Concolic testing,Symbolic execution,Scalability,Buffer overflow
Conference
ISSN
ISBN
Citations 
1527-1366
978-1-5090-5571-5
11
PageRank 
References 
Authors
0.60
27
4
Name
Order
Citations
PageRank
Saahil Ognawala1224.05
Martín Ochoa220122.62
Alexander Pretschner31585137.50
Tobias Limmer4110.60