Test-guided proofs for C programs on LLVM

Abstract

Software defects can be very expensive, especially when encountered in economically critical or safety critical systems. Many of these defects can be avoided if it can be ensured that a program meets its specification. When the specification is given formally, for example with assertions embedded in the source code, automated software verification methods can be applied to determine whether a program complies with its specification.

Recently there has been much interest in combining under approximation and over approximation based approaches to software verification. Such a technique is employed by the DASH algorithm originally developed at Microsoft, which generates tests to improve an under approximation of the program under test. Simultaneously, an over approximating abstraction of the program is refined with information gathered from test generation.

We present an open source implementation of the DASH algorithm for the verification of C programs compiled on the LLVM compiler framework. Our implementation is an extension of the dynamic symbolic execution tool LCT. We also present a detailed method for constructing the weakest precondition based refinement operator employed by DASH for instructions of the LLVM internal representation.

To maintain a mapping between concrete executions and the abstraction DASH needs to evaluate predicates on the concrete states visited during test executions. A straightforward implementation might store the complete concrete states of each executed test or might employ expensive re-executions to recover the concrete states. We present a technique which allows only the concrete values of pointer variables to be stored while still requiring no re-executions.

Finally we present a case study to show the viability of our tool. We also document a more powerful abstraction refinement method used in DASH and evaluate its effect.

Ohjelmistovirheet voivat olla hyvin kalliita, varsinkin turvallisuus- ja talouskriittisissä järjestelmissä. Monet näistä virheistä voidaan välttää jos voidaan varmistaa että ohjelmistot täyttävät niille annetut spesifikaatiot. Kun spesifikaatio on annettu formaalisti, esimerkiksi lähdekoodiin kirjoitetuilla assertioilla, voidaan automaattisilla ohjelmiston verifiointimenetelmillä tarkastaa että ohjelmisto täyttää sen spesifikaation.

Viime aikoina on ollut paljon kiinnostusta yhdistää yli- ja aliapproksimoivia lähestymistapoja ohjelmistojen verifiointiin. DASH algoritmi toteuttaa tällaisen menetelmän. Se generoi testejä parantaakseen aliapproksimaatiota verifioitavasta ohjelmasta. Samanaikaisesti DASH hienontaa ohjelmaa yliapproksimoivaa abstraktiota testien generoinnista kerätyllä informaatiolla.

Esittelemme avoimen lähdekoodin työkalun, joka toteuttaa DASH algoritmin LLVM kääntäjäkirjastolla käännettyjen C ohjelmien verifiointiin. Toteutuksemme perustuu dynaamisen symbolisen suorituksen työkaluun LCT:hen. Annamme myös yksityiskohtaisen menetelmän tuottaa DASH:n vaatima heikoimpiin esiehtoihin perustuva abstraktion hienonnusoperaattori LLVM:n välikielen käskyille.

DASH evaluoi predikaatteja testien aikana nähdyille konkreettisille tiloille ylläpitääkseen kuvausta testiajojen ja abstraktion välillä. Suoraviivainen toteutus saattaisi tallentaa jokaisen ajetun testin kokonaiset konkreettiset tilat tai ajaa testejä toistamiseen konkreettisten tilojen uudelleenkonstruoimiseksi. Esittelemme menetelmän jolla ainoastaan osoittimia sisältävien muuttujien arvot tallennetaan ilman että testejä pitää uudelleenajaa.

Lopuksi näytämme työkalumme käyttökelpoisuuden kokeiden avulla. Dokumentoimme myös DASH algoritmissa käytetyn tehokkaamman abstraktion hienonnusoperaattorin sekä esittelemme sen vaikutuksen kokeellisesti.