“Verifying Low-Level Implementations of High-Level Datatypes” by Christopher L. Conway and Clark Barrett. In Proceedings of the 22^nd International Conference on Computer Aided Verification (CAV '10), (Tayssir Touili, Byron Cook, and Paul Jackson, eds.), July 2010, pp. 306-320. Edinburgh, Scotland.
For efficiency and portability, network packet processing code is typically written in low-level languages and makes use of bit-level operations to compactly represent data. Although packet data is highly structured, low-level implementation details make it difficult to verify that the behavior of the code is consistent with high-level data invariants. We introduce a new approach to the verification problem, using a high-level definition of packet types as part of a specification rather than an implementation. The types are not used to check the code directly; rather, the types introduce functions and predicates that can be used to assert the consistency of code with programmer-defined data assertions. We describe an encoding of these types and functions using the theories of inductive datatypes, bit vectors, and arrays in the Cvc SMT solver. We present a case study in which the method is applied to open-source networking code and verified within the Cascade verification platform.
BibTeX entry:
@inproceedings{CB10,
author = {Christopher L. Conway and Clark Barrett},
editor = {Tayssir Touili and Byron Cook and Paul Jackson},
title = {Verifying Low-Level Implementations of High-Level Datatypes},
booktitle = {Proceedings of the {\it 22^{nd}} International Conference
on Computer Aided Verification (CAV '10)},
series = {Lecture Notes in Computer Science},
volume = {6174},
pages = {306--320},
publisher = {Springer},
month = jul,
year = {2010},
note = {Edinburgh, Scotland},
url = {http://theory.stanford.edu/~barrett/pubs/CB10.pdf}
}
(This webpage was created with bibtex2web.)