Trustworthy Systems

Bitfields and tagged unions in C — verification through automatic generation


David Cock



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

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