Skip to main content

TS

Bitfields and tagged unions in C – verification through automatic generation

Authors

David Cock

NICTA

Abstract

We present a tool for automatic generation of packed bitfields and tagged unions for systems-level C, along with automatic, machine checked refinement proofs in Isabelle/HOL. Our approach provides greater predictability than compiler-specific bitfield implementations, and also provides a basis for formal reasoning about these typically non-type-safe operations. The tool is used in the implementation of the seL4 microkernel, and hence also in the lowest-level refinement step of the L4.verified project which aims to prove the functional correctness of seL4. In the seL4 implementation, it has eliminated the need for unions entirely.

BibTeX Entry

  @inproceedings{Cock_08,
    author           = {Cock, David},
    month            = aug,
    year             = {2008},
    keywords         = {bitfields, isabelle/hol, refinement},
    title            = {Bitfields and Tagged Unions in {C} – Verification through Automatic Generation},
    booktitle        = {VERIFY08},
    pages            = {44-55},
    address          = {Sydney}
  }

Download

Served by Apache on Linux on seL4.