Sciweavers

Share
CAV
2010
Springer

Verifying Low-Level Implementations of High-Level Datatypes

9 years 7 months ago
Verifying Low-Level Implementations of High-Level Datatypes
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 Cvc3 SMT solver. We present a case study in which the method is applied to open-source networking code and verified within the Cascade verification platfor...
Christopher L. Conway, Clark Barrett
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where CAV
Authors Christopher L. Conway, Clark Barrett
Comments (0)
books