Verification of Programs Sensitive to Heap Layout

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F22%3A00125301" target="_blank" >RIV/00216224:14330/22:00125301 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1145/3508363" target="_blank" >https://doi.org/10.1145/3508363</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/3508363" target="_blank" >10.1145/3508363</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Verification of Programs Sensitive to Heap Layout

Popis výsledku v původním jazyce

Most C and C++ programs use dynamically allocated memory (often known as a heap) to store and organize their data. In practice, it can be useful to compare addresses of different heap objects, for instance, to store them in a binary search tree or a sorted array. However, comparisons of pointers to distinct objects are inherently ambiguous: the address order of two objects can be reversed in different executions of the same program, due to the nature of the allocation algorithm and other external factors. This poses a significant challenge to program verification since a sound verifier must consider all possible behaviors of a program, including an arbitrary reordering of the heap. A naive verification of all possibilities, of course, leads to a combinatorial explosion of the state space: for this reason, we propose an under-approximating abstract domain which can be soundly refined to consider all relevant heap orderings. We have implemented the proposed abstract domain and evaluated it against several existing software verification tools on a collection of pointer-manipulating programs. In many cases, existing tools only consider a single fixed heap order, which is a source of unsoundness. We demonstrate that using our abstract domain, this unsoundness can be repaired at only a very modest performance cost. Additionally, we show that, even though many verifiers ignore it, ambiguous behavior is present in a considerable fraction of programs from software verification competition.

Název v anglickém jazyce

Verification of Programs Sensitive to Heap Layout

Popis výsledku anglicky

Most C and C++ programs use dynamically allocated memory (often known as a heap) to store and organize their data. In practice, it can be useful to compare addresses of different heap objects, for instance, to store them in a binary search tree or a sorted array. However, comparisons of pointers to distinct objects are inherently ambiguous: the address order of two objects can be reversed in different executions of the same program, due to the nature of the allocation algorithm and other external factors. This poses a significant challenge to program verification since a sound verifier must consider all possible behaviors of a program, including an arbitrary reordering of the heap. A naive verification of all possibilities, of course, leads to a combinatorial explosion of the state space: for this reason, we propose an under-approximating abstract domain which can be soundly refined to consider all relevant heap orderings. We have implemented the proposed abstract domain and evaluated it against several existing software verification tools on a collection of pointer-manipulating programs. In many cases, existing tools only consider a single fixed heap order, which is a source of unsoundness. We demonstrate that using our abstract domain, this unsoundness can be repaired at only a very modest performance cost. Additionally, we show that, even though many verifiers ignore it, ambiguous behavior is present in a considerable fraction of programs from software verification competition.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2022

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 periodika

ACM Transactions on Software Engineering and Methodology

ISSN

1049-331X

e-ISSN

1557-7392

Svazek periodika

31

Číslo periodika v rámci svazku

4

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

27

Strana od-do

1-27

Kód UT WoS článku

000859387700015

EID výsledku v databázi Scopus

2-s2.0-85141097473