Verification of Programs Sensitive to Heap Layout

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

Verification of Programs Sensitive to Heap Layout

Original language description

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.

Czech name

—

Czech description

—

Type

J_imp - Article in a specialist periodical, which is included in the Web of Science database

CEP classification

—

OECD FORD branch

10200 - Computer and information sciences

Project

—

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2022

Confidentiality

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

Name of the periodical

ACM Transactions on Software Engineering and Methodology

ISSN

1049-331X

e-ISSN

1557-7392

Volume of the periodical

31

Issue of the periodical within the volume

4

Country of publishing house

US - UNITED STATES

Number of pages

27

Pages from-to

1-27

UT code for WoS article

000859387700015

EID of the result in the Scopus database

2-s2.0-85141097473