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.
NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council.
In this paper we present a tool that automatically generates inline-able C functions to implement tagged unions of packed bitfield types, based on a simple domainspecific-language specification. We then generalise, and suggest a technique to exploit the desires of systems programmers to ease program verification.
The motivation for this work was the C implementation of the seL4 microkernel, and the needs of the associated L4.verified project [8,3]. The seL4 microkernel [5,7] is an evolution of the L4 family [17] for secure, embedded devices. The L4.verified project aims to prove its functional correctness. The need to produce code that can be verified with reasonable effort requires the disciplined use of 'ugly' programming idioms, those which violate the basic abstractions of the underlying semantic model. In our case, these are heap type aliases, i.e. unions, non-type-safe pointer accesses, and sub-machine-word manipulations. These violations occur commonly together, in the tagged union and bitfield construct. See Fig. 1 for an example from the OKL4 kernel [19], a current commercial implementation of L4. This pattern is very regular, and an obvious target for automation. Generation of this code is desirable for two reasons: First, via controlled tagged unions, it adds functionality to C in a disciplined, type-safe way. Second, bitfield implementations vary widely, both in performance and in actual behaviour between compilers, and even different versions of the same compiler. As a result, they are usually mistrusted by kernel programmers. In contrast, our generated code is fast, predictable and formally correct. Our approach is to provide an opaque, abstract type, implementing the tagged-union/bitfield semantics, together with generated accessor functions. The tool automatically provides the proofs that the functions behave as expected. Whilst this is not a radically new idea, our approach is successful precisely because we target the regular low-level functions, which nonetheless comprise 14% of the code within seL4. This tool also provides a case study for the use of the C semantics of Tuch et al. [26], and Dawson's Isabelle/HOL library for machine words [4]. The remainder of the paper is laid out as follows: Section 2 introduces the specification language used to describe the bit-level layout of structures, Section 3 shows the C code generation framework, and Section 4 explains the framework of automatically generated proofs to allow reasoning without descending to the level of pointers and bit manipulation.
The tagged-union/packed-bitfield structure is useful in a number of contexts e.g. hardware-dictated page-table layouts, hardware register mapping, and highly optimised data structure storage. As a running example, we will consider a subset of the seL4/ARM capability representation. Capabilities are used as a proxy for authority, and we consider only two capability types: Null caps (null cap) which function as placeholders, and Untyped caps (untyped cap) which convey authority over a power of two sized block of memory. The capability is represented as a two word (64 bit) bitfield: Null caps contain no data other than the type tag, whereas Untyped caps have two fields: capBlockSize and capPtr, a pointer aligned on a 16-byte boundary.
The cap representations are specified as follows (the full grammar is included in Fig. 5). First the machine word size (32 bits for ARM) is specified with the base keyword: base 32
Next, bitfield blocks are specified. Fields are listed from most-significant to least-significant bit (Fig. 2). The padding keyword introduces anonymous padding space, to achieve the desired alignment, and the field keyword reserves space for a named field. In the null cap example, padding 32 reserves one empty machine word, field capType 4 allocates a 4 bit field at the top of the second word, and padding 28 explicitly fills the remainder of the second word. The trailing padding is mandatory where the fields do not fill the lower bits of the last word. Padding between fields is inserted explicitly, fields are forbidden to cross word boundaries, and the size of each block must be a multiple of the base word size. These restrictions ensure that the implementation maps efficiently onto common machine operations, and present no difficulties in practice. The field high keyword specifies that a field should be left-aligned to the word size when read or written, padded on the right with zero bits, see Fig. 3. Finally, blocks are grouped together into tagged unions (Fig. 4). The keyword tagged union is followed by the name of the union, and the name of the tag field, then a list of block names, together with their associated tag values. All blocks in the union must be the same size, and each must contain a tag field. All tag fields must be the same size, and at the same location within the block.
This section gives a brief overview of the code generated from the specifications above. Each block and union in the specification language is translated to a C representation with appropriate access and update functions. Each object is represented by a struct containing simply an array of machine words, and for each union, an enum of tag values. The wrapping struct allows pass and return by value in C. For each block and union, the tool generates create, access and update functions. Each such function is generated in a purely functional version, which passes and returns a stack object of appropriate struct type:
Also generated is a pointer lifted version, which operates indirectly on heap values through a supplied pointer:
The prototypes for the remaining functions are given in Fig. 6. Note that the generated API only provides functions that read the tag field through the union type, and no function to write it directly. This imposes a class-like behaviour on the types. The subtype is set implicitly at creation time, and can only be modified by overwriting with an object of a different type. This will turn out to be an important property for verification.
In practice the output is automatically pruned, so that only those functions actually used in the source are generated. This speeds the proof process. As the specification language is highly focussed and carefully limited, the generated code is simple and fast, highly predictable, and easily inlined by the compiler.
The final and most novel part of the approach consists of the automatically generated, machine checked function specifications together with their automated proofs. The function of the generated proofs is not only to show implementation correctness, but also to provide sufficient reasoning power to allow any statement involving the generated functions to be rephrased in terms of simple operations on abstract, high-level types in the theorem prover. This means that we can avoid invoking bit manipulations and pointer dereferences when reasoning about the packed structures as part of a larger proof. We can instead reason about higher-level types, for which there is well established support. This abstract representation is expressed in terms of Isabelle's record types, which behave much like struct or record constructs in typical programming languages, providing access and update of disjoint fields. The bitfields from the C level are represented as records of fields on the abstract level. For example, the untyped cap block is represented as follows:
record cap_untyped_cap_CL = capBlockSize_CL :: "word32" capPtr_CL :: "word32"
Tagged unions are represented by an algebraic datatype wrapping the records corresponding to the component bitfields, with one constructor for each. Tag fields are not included in the record representation, but are implied by the choice of constructor within the union type. Any bitfields which are empty after the removal of the tag field are represented simply by a naked constructor, with no associated record. The cap union translates thus:
The name convention is that the C types and identifiers, when parsed into Isabelle, are tagged by appending C, whereas the lifted types are tagged with CL. The connection between the C level and the abstract level will be provided by two functions in the example below: cap_lift and cap_untyped_cap_lift. The former lifts any cap_C to a cap_CL, and the latter lifts a cap_C with the untyped cap tag directly to a cap_untyped_cap_CL. It is under-specified in all other cases.
The properties of the generated functions are expressed as strongest-postcondition Hoare rules. Specifically, we use Schirmer's [23] verification environment for imperative programs in Isabelle/HOL. It contains a verification condition generator (VCG) which automates reasoning about Hoare-triples. Tuch's et al. [26] instantiation to C parses the generated code directly into Isabelle/HOL and into Schirmer's representation language SIMPL.
As an example, we will take the generated specification of the generated C function cap untyped cap set capBlockSize. The specification above reads as follows. For all program contexts Γ , if the tag of the C-struct cap in the current state (indicated by ´) equals the value cap_untyped_cap, and we execute the function cap_untyped_cap_set_capBlockSize with parameters cap and v, storing its return value in ret__struct_cap_C, we will arrive at the following post condition: lifting the return value to the abstract record type is the same as lifting the value of cap in the initial state s, and then performing an update of the abstract record field capBlockSize_CL with the value v had in state s. Additionally, as a convenience for automated methods in the larger proof, we provide that the tag of the return value remains cap_untyped_cap. A separate specification states (and the tool proves) that the function is side-effect free, i.e. that no global variables, including the heap, are changed. The term AND (mask 5) carries the additional information that the field has a size of 5 bits. This form proved more convenient than the alternative of having an abstract field of word length 5, because casting between word lengths often introduces additional proof obligations.
The meaning of the rule can also be expressed by means of the commuting diagram in Fig. 7. For Fig. 7, consider cap untyped cap set capBlockSize as a function from cap t (its first argument) to cap t (its return value). Control flows left to right, and r (| a := x |) is the Isabelle syntax for the record r, with field a updated with value x. This makes it clear that the function of the rule is to allow us to transform a function call into a record update, by commuting it with a lift. We can therefore take any precondition of the form P (cap_untyped_cap_lift cap), and commute it past any number of field updates, to produce a postcondition of the form P (f (cap_untyped_cap_lift cap)), where f is the composition of a number of record updates. We can base our argument on such a case, as long as bitfield objects are only initialised via the appropriate * new functions, and the type tags are never externally modified. This justifies the API restriction introduced in Section 3, which is adhered to by the seL4 kernel implementation without loss of convenience or performance.
Equivalent rules are proved automatically for all the generated functions, and their pointer-lifted versions. The latter involve direct heap access to record fields and automate the interactive reasoning Tuch provides [25]. Additionally to what Tuch provides, we make use of the concept of packed records, which allow us to ignore padding in record implementations and derive more precise properties of the corresponding memory layout. Packed records are represented by a type class in Isabelle that simply states that all fields in the record are of a size that makes padding unnecessary.
The proofs of the specifications above are fully automated and generally consists of two to three automated method invocations in Isabelle. The first of these is a call to the C-level VCG mentioned above. The second and possibly third, first reduce the remaining proof obligation from variable, heap, and structupdates to a goal on bit-vectors only. This is then solved automatically with a carefully designed set of generic, algebraic rewrite rules for the bit operations involved in the generated functions. The direct proof script for one specification of a typical C-function is typically about 10 lines long.
Earlier work on OS verification includes PSOS [10] and UCLA Secure Unix [27]. Later, KIT [2] describes verification of process isolation properties down to object code level, but for an idealised kernel far simpler than modern microkernels. The Verisoft project [11,12] is attempting to verify a whole system stack, including hardware, compiler, applications, and a simplified microkernel: VAMOS. The VFiasco [14] project is attempting to verify the Fiasco kernel, another variant of L4, directly at the C++ level. These verification projects do not use generated C code for automating parts of their proof obligations. In the case of Verisoft, there is no reason to distrust the compiler as it is also verified [20,15]. Directly using C or dropping down to assembly code to implement the desired features does not have the benefit of the high-level reasoning support and API the tool presented here provides, however.
The verified proofs in this work build directly on Tuch's et al. memory model for C [26,25,24] which in turn builds on work by Schirmer [23,22] that provides a generic framework, verification condition generator, and Hoare logic [13] for imperative programs. Both are intended for interactive verification. This paper uses the predictable structure of the generated code to completely automate the pointer level proofs on the C implementation.
This work also builds directly on Dawson's machine-word library [4] for Isabelle/HOL. Despite recent progress in tools like Yices [6], bit-vector proofs for machine words remain hard to automate. Traditional SAT solvers are usually too slow to handle the resulting proof obligations on realistic word sizes. Again, due to the predictable nature of the generated code, the tool is able to fully automate the bit-level verification conditions with a set of algebraic rewrite rules. This means that switching to different, say 64-bit, architectures should not result in any noticeable slowdown of the generated proofs.
General translation validation [21] and compiler correctness including Leroy's et al. work [16] are related to the topic. As mentioned above, the tool presented here can exploit the known, predictable nature of the application to provide a convenient interface to, and integration into, the user's proofs.
Also related to generated correctness proofs is the idea of proof-carrying code [18], which usually focusses on the machine level and on specific properties such as memory safety or resource constraints. Functional correctness is not usually targeted, because it is impossible to automate completely. Barthe et al. [1] come close by automatically transforming certificates from source code to machine code and, similarly to the work presented here, generating proofs for generated code. In contrast to this, the bitfield generator here does not require any source-level proof as input. It generates a full functional correctness statement automatically.
Denney et al. [9] automatically prove properties about generated aerospace software. The generated code appears more complex than that presented here, but the semantics they are using is not foundational and the properties do not cover full functional correctness, only specific safety properties.
This paper has summarised a generator for tagged unions of packed bitfields in the C programming language, as they are used in low-level systems code and operating system kernel implementations. In theory, this data structure can be implemented with C primitives without resorting to a generator. However, compiler implementations of bitfields seem to be so unpredictable in memory layout and performance over different platforms and compilers that kernel programmers distrust this compiler feature more than others.
The tool generates efficient, predictable, and above all correct C code from a short, high-level description that is detailed enough to provide precise memory layout specification which is important to map data, for instance, to memory mapped hardware device registers. The generated code includes the data type itself as well as an API for convenient, high-level access on the stack and on the heap.
This work shows that an automatic correctness proof of generated code for controlled environments is not hard to achieve, even if this code contains bit-level reasoning and pointer access. The proof is foundational in the sense that it assumes no specific axioms on the application domain, but is built directly on the semantics of the C programming language. The proof is machine-checked in the theorem prover Isabelle/HOL and provides an example of translationvalidation: Instead of proving the correctness of the generator, the correctness of the generated code is proven instead.
The usefulness of the tool reaches further than a stand-alone correctness proof. The Hoare-triples proven integrate directly, within the same formal model, with larger implementation proofs of client code using the generated bitfields. The Hoare-triples are designed such that client proofs and code have no need to reason about the internal representation or bit-level operations that are carried out. They provide an abstract interface. Translation validation has likely made this easier to achieve than in a generator correctness proof. No meta-level reasoning or switching of formal models is required.
The tool is expected to automate 14% of the C implementation proofs in the L4.verified project, covering 1,800 lines of C code with 7,800 lines of generated proof. The seL4 kernel, including all generated inline functions, comprises 12,600 lines of code. The tool is generally applicable to code that needs to have direct, reliable control over the memory layout of data structures. The technique of generating proofs that integrate well into interactive environments should generalise easily to constrained application domains where the structure of the generated proof is predictable.