CSAIL Event Calendar: Previous Series

Verifying Low-Level Implementations of High-Level Datatypes

Speaker: Clark Barrett , New York University
Date: March 31 2011
Time: 3:00PM to 4:00PM
Location: 32-G882 (Hewlett Room)
Host: Daniel Jackson, CSAIL

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

Bio:

Clark Barrett is an associate professor at New York University. His research interests include propositional satisfiability (SAT), satisfiability modulo theories (SMT), automated deduction and applied logic, proof-producing algorithms, formal and semi-formal verification of hardware and software, and combining verification systems. He was recently awarded the Haifa Verification Conference award (2010), along with Leonardo de Moura, Silvio Ranise, Aaron Stump, and Cesare Tinelli, for his pivotal role in building and promoting the Satisfiability Modulo Theories (SMT) community.

See other events that are part of

See other events happening in March 2011