Bitfields and Tagged Unions in C: Verification through Automatic Generation

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 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. Within seL4, it has eliminated the need for unions entirely.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: David Cock
• Keywords: Automated Reasoning, CADE 2008, Lowest-level Refinement Step, Machine Checked Refinement, Systems-level C