Verifying low-level implementations of high-level datatypes

Christopher L. Conway, Clark Barrett

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 22nd International Conference, CAV 2010, Proceedings
Pages306-320
Number of pages15
DOIs
StatePublished - 2010
Event22nd International Conference on Computer-Aided Verification, CAV 2010 - Edinburgh, United Kingdom
Duration: Jul 15 2010Jul 19 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6174 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other22nd International Conference on Computer-Aided Verification, CAV 2010
CountryUnited Kingdom
CityEdinburgh
Period7/15/107/19/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Verifying low-level implementations of high-level datatypes'. Together they form a unique fingerprint.

Cite this