Verifying Low-Level Implementations of High-Level Datatypes

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.

Abstract

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