Don't Sweat the Small Stuff: Formal Verification of C Code Without the Pain

Select |




Print


Greenaway, David; Lim, Japheth; Andronick, June; Klein, Gerwin

Greenaway, David; Lim, Japheth; Andronick, June; Klein, Gerwin


2014-06-09


Conference Material


Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation


Edinburgh, UK


429--439


We present an approach for automatically generating provably correct abstractions from C source code that are useful for practical implementation verification. The abstractions are easier for a human verification engineer to reason about than the implementation and increase the productivity of interactive code proof. We guarantee soundness by automatically generating proofs that the abstractions are correct. In particular, we show two key abstractions that are critical for verifying systems-level C code: automatically turning potentially overflowing machine-word arithmetic into ideal integers, and transforming low-level C pointer reasoning into separate abstract heaps. Previous work carrying out such transformations has either done so using unverified translations, or required significant proof engineering effort. We implement these abstractions in an existing proof-producing specification transformation framework named AutoCorres, developed in Isabelle/HOL, and demonstrate its effectiveness in a number of case studies. We show scalability on multiple OS microkernels, and we show how our changes to AutoCorres improve productivity for total correctness by porting an existing high-level verification of the Schorr-Waite algorithm to a low-level C implementation with minimal effort.


ACM


C verification; Isabelle/HOL


https://doi.org/10.1145/2594291.2594296


http://conferences.inf.ed.ac.uk/pldi2014/


nicta:7629


Greenaway, David; Lim, Japheth; Andronick, June; Klein, Gerwin. Don't Sweat the Small Stuff: Formal Verification of C Code Without the Pain. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation; Edinburgh, UK. ACM; 2014-06-09. 429--439. https://doi.org/10.1145/2594291.2594296



Loading citation data...

Citation counts
(Requires subscription to view)