ASE: A Value Set Decision Procedure for Symbolic Execution

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21240%2F21%3A00365498" target="_blank" >RIV/68407700:21240/21:00365498 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1109/ASE51524.2021.9678584" target="_blank" >https://doi.org/10.1109/ASE51524.2021.9678584</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/ASE51524.2021.9678584" target="_blank" >10.1109/ASE51524.2021.9678584</a>

Jazyk výsledku

angličtina

Název v původním jazyce

ASE: A Value Set Decision Procedure for Symbolic Execution

Popis výsledku v původním jazyce

A symbolic execution engine regularly queries a Satisfiability Modulo Theory (SMT) solver to determine reachability of code during execution. Unfortunately, the SMT solver is often the bottleneck of symbolic execution. Inspired by abstract interpretation, we propose an abstract symbolic execution (ASE) engine which aims at querying the SMT solver less often by trying to compute reachability faster through an increasingly weaker abstraction. For this purpose, we have designed and implemented a value set decision procedure based on strided value interval (SVI) sets for efficiently determining precise, or under-approximating value sets for variables. Our ASE engine begins reasoning with respect to the SVI abstraction, and then only if needed uses the theory of bit-vectors implemented in SMT solvers. Our ASE engine efficiently detects when the former abstraction becomes incomplete to move on and try the next abstraction. We have designed and implemented a prototype of our engine for a subset of 64-bit RISC-V. Our experimental evaluation shows that our prototype often improves symbolic execution time by significantly reducing the number of SMT queries while, whenever the abstraction does not work, the overhead for trying still remains low.

Název v anglickém jazyce

ASE: A Value Set Decision Procedure for Symbolic Execution

Popis výsledku anglicky

A symbolic execution engine regularly queries a Satisfiability Modulo Theory (SMT) solver to determine reachability of code during execution. Unfortunately, the SMT solver is often the bottleneck of symbolic execution. Inspired by abstract interpretation, we propose an abstract symbolic execution (ASE) engine which aims at querying the SMT solver less often by trying to compute reachability faster through an increasingly weaker abstraction. For this purpose, we have designed and implemented a value set decision procedure based on strided value interval (SVI) sets for efficiently determining precise, or under-approximating value sets for variables. Our ASE engine begins reasoning with respect to the SVI abstraction, and then only if needed uses the theory of bit-vectors implemented in SMT solvers. Our ASE engine efficiently detects when the former abstraction becomes incomplete to move on and try the next abstraction. We have designed and implemented a prototype of our engine for a subset of 64-bit RISC-V. Our experimental evaluation shows that our prototype often improves symbolic execution time by significantly reducing the number of SMT queries while, whenever the abstraction does not work, the overhead for trying still remains low.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/EF15_003%2F0000421" target="_blank" >EF15_003/0000421: Big Code: Škálovatelná analýza rozsáhlých bází programů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering

ISBN

978-1-6654-0337-5

ISSN

—

e-ISSN

—

Počet stran výsledku

12

Strana od-do

203-214

Název nakladatele

IEEE Press

Místo vydání

—

Místo konání akce

Melbourne

Datum konání akce

15. 11. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000779309000020