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
Volume6174 LNCS
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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Machine oriented languages
Surface mount technology
Packet networks
Specifications
Processing
Portability
Assertion
Networking
Open Source
Predicate
Cascade
Encoding
Specification
Verify
Invariant

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Conway, C. L., & Barrett, C. (2010). Verifying low-level implementations of high-level datatypes. In Computer Aided Verification - 22nd International Conference, CAV 2010, Proceedings (Vol. 6174 LNCS, pp. 306-320). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6174 LNCS). https://doi.org/10.1007/978-3-642-14295-6_28

Verifying low-level implementations of high-level datatypes. / Conway, Christopher L.; Barrett, Clark.

Computer Aided Verification - 22nd International Conference, CAV 2010, Proceedings. Vol. 6174 LNCS 2010. p. 306-320 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6174 LNCS).

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

Conway, CL & Barrett, C 2010, Verifying low-level implementations of high-level datatypes. in Computer Aided Verification - 22nd International Conference, CAV 2010, Proceedings. vol. 6174 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6174 LNCS, pp. 306-320, 22nd International Conference on Computer-Aided Verification, CAV 2010, Edinburgh, United Kingdom, 7/15/10. https://doi.org/10.1007/978-3-642-14295-6_28
Conway CL, Barrett C. Verifying low-level implementations of high-level datatypes. In Computer Aided Verification - 22nd International Conference, CAV 2010, Proceedings. Vol. 6174 LNCS. 2010. p. 306-320. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-14295-6_28
Conway, Christopher L. ; Barrett, Clark. / Verifying low-level implementations of high-level datatypes. Computer Aided Verification - 22nd International Conference, CAV 2010, Proceedings. Vol. 6174 LNCS 2010. pp. 306-320 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{2492d798f20a4496ac96de13cc1ebd95,
title = "Verifying low-level implementations of high-level datatypes",
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.",
author = "Conway, {Christopher L.} and Clark Barrett",
year = "2010",
doi = "10.1007/978-3-642-14295-6_28",
language = "English (US)",
isbn = "364214294X",
volume = "6174 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "306--320",
booktitle = "Computer Aided Verification - 22nd International Conference, CAV 2010, Proceedings",

}

TY - GEN

T1 - Verifying low-level implementations of high-level datatypes

AU - Conway, Christopher L.

AU - Barrett, Clark

PY - 2010

Y1 - 2010

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

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

UR - http://www.scopus.com/inward/record.url?scp=77955004853&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77955004853&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-14295-6_28

DO - 10.1007/978-3-642-14295-6_28

M3 - Conference contribution

SN - 364214294X

SN - 9783642142949

VL - 6174 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 306

EP - 320

BT - Computer Aided Verification - 22nd International Conference, CAV 2010, Proceedings

ER -