Abstract
This paper concerns the scalability challenges of symbolic abstraction: given a formula φ in a logic L and an abstract domain A, find a most precise element in the abstract domain that over-approximates the meaning of φ. Symbolic abstraction is an important point in the space of abstract interpretation, as it allows for automatically synthesizing the best abstract transformers. However, current techniques for symbolic abstraction can have difficulty delivering on its practical strengths, due to performance issues.
In this work, we introduce two algorithms for the symbolic abstraction of quantifier-free bit-vector formulas, which apply to the bit-vector interval domain and a certain kind of polyhedral domain, respectively. We implement and evaluate the proposed techniques on two machine code analysis clients, namely static memory corruption analysis and constrained random fuzzing. Using a suite of 57,933 queries from the clients, we compare our approach against a diverse group of state-of-the-art algorithms. The experiments show that our algorithms achieve a substantial speedup over existing techniques and illustrate significant precision advantages for the clients. Our work presents strong evidence that symbolic abstraction of numeric domains can be efficient and practical for large and realistic programs.
© 2021 Copyright held by the owner/author(s).
In this work, we introduce two algorithms for the symbolic abstraction of quantifier-free bit-vector formulas, which apply to the bit-vector interval domain and a certain kind of polyhedral domain, respectively. We implement and evaluate the proposed techniques on two machine code analysis clients, namely static memory corruption analysis and constrained random fuzzing. Using a suite of 57,933 queries from the clients, we compare our approach against a diverse group of state-of-the-art algorithms. The experiments show that our algorithms achieve a substantial speedup over existing techniques and illustrate significant precision advantages for the clients. Our work presents strong evidence that symbolic abstraction of numeric domains can be efficient and practical for large and realistic programs.
© 2021 Copyright held by the owner/author(s).
| Original language | English |
|---|---|
| Article number | 118 |
| Journal | Proceedings of the ACM on Programming Languages |
| Volume | 5 |
| Issue number | OOPSLA |
| DOIs | |
| Publication status | Published - Oct 2021 |
| Externally published | Yes |
Funding
We thank the anonymous reviewers and our shepherd for valuable feedback on earlier drafts of this paper, which helped improve its presentation. We also appreciate Dr. Jörg Brauer and Dr. Mianlai Zhou for insightful discussions. The authors are supported by the RGC16206517 and ITS/440/18FP grants from the Hong Kong Research Grant Council, Ant Research Program, and the donations from Microsoft and Huawei. Qingkai Shi is the corresponding author.
Research Keywords
- Abstract interpretation
- interval domain
- optimization
- polyhedral domain
- symbolic abstraction
Publisher's Copyright Statement
- This full text is made available under CC-BY 4.0. https://creativecommons.org/licenses/by/4.0/
RGC Funding Information
- RGC-funded
Fingerprint
Dive into the research topics of 'Program analysis via efficient symbolic abstraction'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver