Paper Info
Title
Automatically testing implementations of numerical abstract domains.
Abstract
Static program analyses are routinely applied as the basis of code optimizations and to detect safety and security issues in software systems. For their results to be reliable, static analyses should be sound (i.e., should not produce false negatives) and precise (i.e., should report a low number of false positives). Even though it is possible to prove properties of the design of a static analysis, ensuring soundness and precision for its implementation is challenging. Complex algorithms and sophisticated optimizations make static analyzers difficult to implement and test. In this paper, we present an automatic technique to test, among other properties, the soundness and precision of abstract domains, the core of all static analyzers based on abstract interpretation. In order to cover a wide range of test data and input states, we construct inputs by applying sequences of abstract-domain operations to representative domain elements, and vary the operations through gray-box fuzzing. We use mathematical properties of abstract domains as test oracles. Our experimental evaluation demonstrates the effectiveness of our approach. We detected several previously unknown soundness and precision errors in widely-used abstract domains. Our experiments also show that our approach is more effective than dynamic symbolic execution and than fuzzing the test inputs directly.
Year
DOI
Venue
2018
10.1145/3238147.3240464
ASE
Keywords
Field
DocType
soundness testing, precision testing, abstract interpretation
Fuzz testing,Abstract interpretation,Computer science,Static analysis,Software system,Theoretical computer science,Test data,Symbolic execution,Soundness,Computer engineering,False positive paradox
Conference
ISSN
ISBN
Citations 
1527-1366
978-1-4503-5937-5
1
PageRank 
References 
Authors
0.35
31
4
Name
Order
Citations
PageRank
Alexandra Bugariu121.04
Valentin Wüstholz21178.46
Maria Christakis320016.69
Peter Müller478150.82