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.
@inproceedings{Greenaway_LAK_14,
title = {Don't Sweat the Small Stuff: Formal Verification of {C} Code
Without the Pain},
author = {David Greenaway and Japheth Lim and June Andronick and
Gerwin Klein},
booktitle = {Proceedings of the 35th ACM SIGPLAN Conference on
Programming Language Design and Implementation},
year = {2014},
month = {jun},
pages = {429--439},
address = {Edinburgh, UK},
publisher = {ACM},
doi = {10.1145/2594291.2594296}
}