Model checking boot code from AWS data centers

Boot code starts a sequenced boot flow [4] in which each stage locates, loads, and launches the next stage. The boot flow in a modern data center proceeds as follows: (1) When the power is turned on, before a single instruction is executed, the hardware interrogates banks of fuses and hardware registers for configuration information that is distributed to various parts of the platform. (2) Boot code starts up to boot a set of microcontrollers that orchestrate bringing up the rest of the platform. In a cloud data center, some of these microcontrollers are feature-rich cores with their own devices used to support virtualization. (3) The BIOS familiar to most people starts up to boot the cores and their devices. (4) A boot loader for the hypervisor launches the hypervisor to virtualize those cores. (5) A boot loader for the operating system launches the operating system itself. The security of each stage, including operating system launched for the customer, depends on the integrity of all prior stages [27].

Ensuring boot code security using traditional techniques is hard. Visibility into code execution can only be achieved via debug ports, with almost no ability to single-step the code for debugging. UEFI (Unified Extensible Firmware Interface) [56] provides an elaborate infrastructure for debugging BIOS, but not for the boot code below BIOS in the software stack. Instrumenting boot code may be impossible because it can break the build process: the increased size of instrumented code can be larger than the size of the ROM targeted by the build process. Extracting the data collected by instrumentation may be difficult because the code has no access to a file system to record the data, and memory available for storing the data may be limited.

Static analysis is a relatively new approach to enhancing confidence in boot code security. As discussed in Sect. 2, most work applying static analysis to boot code applies technology like symbolic execution to binary code, either because the work strips the boot code from ROMs on shipping products for analysis and reverse engineering [38, 51], or because code like UEFI-based implementations of BIOS loads modules with a form of dynamic linking that makes source code analysis of any significant functionality impossible [5, 28]. But with access to the source code—source code without the complexity of dynamic linking—meaningful static analysis at the source code level is possible.

Boot code is a foundational component of data center security: it controls what code is run on the server. Attacking boot code is a path to booting your own code, installing a persistent root kit, or making the server unbootable. Boot code also initializes devices and interfaces directly with them. Attacking boot code can also lead to controlling or monitoring peripherals like storage devices.

The input to boot code is primarily configuration information. The run-time behavior of boot code is determined by configuration information in fuses, hardware straps, one-time programmable memories, and ROMs.

From a security perspective, boot code is susceptible to a variety of events that could set the configuration to an undesirable state. To keep any malicious adversary from modifying this configuration information, the configuration is usually locked or otherwise write-protected. Nonetheless, it is routine to discover during hardware vetting before placing hardware on a data center floor that some BIOS added by a supplier accidentally leaves a configuration register unlocked after setting it. In fact, configuration information can be intentionally unlocked for the purpose of patching and then be locked again. Any bug in a patch or in a patching mechanism has the potential to leave a server in a vulnerable configuration. Perhaps more likely than anything is a simple configuration mistake at installation. We want to know that no matter how a configuration may have been corrupted, the boot code will operate as intended and without latent exposures for potential adversaries.

The attack surface we focus on in this paper is memory safety, meaning there are no buffer overflows, no dereferencing of null pointers, and no pointers pointing into unallocated regions of memory. Code written in C is known to be at risk for memory safety, and boot code is almost always written in C, in part because of the direct connection between boot code and the hardware, and sometimes because of space limitations in the ROMs used to store the code.

There are many techniques for protecting against memory safety errors and mitigating their consequences at the higher levels of the software stack. Languages other than C are less prone to memory safety errors. Safe libraries can do bounds checking for standard library functions. Compiler extensions to compilers like gcc and clang can help detect buffer overflow when it happens (which is different from keeping it from happening). Address space layout randomization makes it harder for the adversary to make reliable use of a vulnerability. None of these mitigations, however, apply to firmware. Firmware is typically built using the tool chain that is provided by the manufacturer of the microcontroller, and firmware typically runs before the operating system starts, without the benefit of operating system support like a virtual machine or randomized memory layout.

To facilitate analysis of low-level code, we have added to CBMC a built-in function

to mark ranges of memory as valid. Accesses within this region are exempt from the out-of-bounds assertion checking that CBMC would normally do. The function declares the half-open interval as valid memory that can be read and written. This function can be used anywhere in the source code, but is most commonly used in the test harness. (CBMC, like most program analysis approaches, uses a test harness to drive the analysis.)

An MMIO region is an interface to a device. It is unsound to assume that the values returned by reading and writing this region of memory follow the semantics of ordinary read-write memory. Imagine a device that can generate unique ids. If the register returning the unique id is mapped to the byte at location 0x1000, then reading location 0x1000 will return a different value every time, even without intervening writes. These side effects have to be modeled. One easy approach is to ‘havoc’ the device, meaning that writes are ignored and reads return nondeterministic values. This is sound, but may lead to too many false positives. We can model the device semantics more precisely, using one of the options described below.

If the device has an API, we havoc the device by making use of a more general functionality we have added to CBMC. We have added a command-line option

to CBMC’s goto-instrument tool. When used, this will drop the implementation of the function device_access from compiled object code. If there is no other definition of device_access, CBMC will model each invocation of device_access as returning an unconstrained value of the appropriate return type. Now, to havoc a device with an API that includes a read and write method, we can use this command-line option to remove their function bodies, and CBMC will model each invocation of read as returning an unconstrained value.

At link time, if another object file, such as the test harness, provides a second definition of device_access, CBMC will use this definition in its place. Thus, to model device semantics more precisely, we can provide a device model in the test harness by providing implementations of (or approximations for) the methods in the API.

If the device has no API, meaning that the code refers directly to the address in the MMIO region for the device without reference to accessor functions, we have another method. We have added two function symbols

to CBMC to model the reading or writing of an address at a fixed integer address. If the test harness provides implementations of these functions, CBMC will use these functions to model every read or write of memory. For example, defining

will return the value upon any access at address 0x1000, and return a non-deterministic value in all other cases.

In both cases—with or without an API—we can thus establish sound and, if needed, precise analysis about an aspect of implementation-defined behavior.

It is common for boot code to access memory a byte at a time, and to access a byte that is not part of any variable or data structure declared in the program text. Accessing a byte in an MMIO region is the most common example. Boot code typically accesses this byte in memory by computing the address of the byte as an integer value, coercing this integer to a pointer, and dereferencing this pointer to access that byte. Boot code references memory by this kind of explicit address far more frequently than it references memory via some explicitly allocated variable or data structure. Any tool analyzing boot code must have a method for reasoning efficiently about accessing an arbitrary byte of memory.

A natural model for memory is as an array of bytes [55]. This enables CBMC to precisely reason about memory accesses in presence of pointer arithmetic, at the expense of not using abstractions like those provided by Separation Logic [52]. Any decision procedure that has a well-engineered implementation of a theory of arrays is likely to do a good job of modeling byte-level memory access. We improved CBMC’s decision procedure for arrays to follow the state-of-the-art algorithm [17, 37]. The key data structure is a weak equivalence graph whose vertices correspond to array terms. Given an equality \(a=b\) between two array terms a and b, add an unlabeled edge between a and b. Given an update \(a\{i \leftarrow v\}\) of an array term a, add an edge labeled i between a and \(a\{i \leftarrow v\}\). Two array terms a and b are weakly equivalent if there is a path from a to b in the graph, and they are equal at all indices except those updated along the path. This graph is used to encode constraints on array terms for the solver. For simplicity, our implementation generates these constraints eagerly.

One of the main jobs of any stage of the boot flow is to copy the next stage into memory, usually using some variant of . Any tool analyzing boot code must have an efficient model of . Modeling as a loop iterating through a thousand bytes of memory leads to performance problems during program analysis. We added to CBMC an improved model of the and library functions.

Boot code has no access to a C library. In our case, the boot code shipped an iterative implementation of and . CBMC’s model of the C library previously also used an iterative model. We replaced this iterative model of and with a single array operation that can be handled efficiently by the decision procedure at the back end. We instructed CBMC to replace the boot code implementations with the CBMC model using the –remove-function-body command-line option described in Sect. 4.2.

Boot code and other low-level programs control and access their memory layout using custom linker scripts, which is a mechanism external to the source code. This means that current static analysis tools, which only read and analyze the source code, do not correctly model the memory layout of such programs. This is a hindrance to verifying the memory safety of boot code, in which buffers are commonly defined in linker scripts. Without understanding what the runtime memory layout will be, static analysis tools falsely report that boot code is unsafe. In this section, we present informal description of linker scripts, how programmers use them to control memory layout, and why this poses problems for static analysis. We describe how we overcame these problems in Sect. 5.5.

The left-hand side of Fig. 1 depicts a short program written in C. This code is memory safe when linked according to the linker script on the right-hand side of the figure, but current static analyzers—that consider only the C code—cannot show that it is memory safe.

This program contains two unusual features:To explain these apparent contradictions, we present an overview of how linking works and how the linker script in Fig. 1 makes the C program valid.

Compilers, linkers, and linker scripts A compiler transforms a single source file into an object file. An object file contains machine code organized into several sections; each section has a name and contains machine code for a specific purpose. Conventionally, object files emitted by a compiler contain the following sections, among many others:A linker joins several object files into a single object. By default, it joins identically-named sections in each of the input files into a single contiguous section in the output object, as depicted in Fig. 2.

The functionality of most programs does not depend on the exact layout of the program’s own machine code and data. The default behavior of a linker therefore suffices to correctly link the majority of programs. However, the functionality of low-level software (like boot loaders, kernels, and firmware) often does depend on the exact layout of structures in the object file. For example, [10] discusses the custom sections that are present in the Linux kernel’s object file, and [44, 45, 47, 48] describe various link-level optimizations that are applied to the kernel. In such cases, programmers manually control the object file’s layout by running the linker according to a hand-written linker script. Linker scripts are imperative programs that can direct the linker to place sections at particular addresses; control the access permissions of those sections; and place symbols (named addresses that demarcate code or data) at arbitrary points in the object file. Figure 3 depicts an object file a linker might emit when linking the program in Fig. 1, following the script in that figure.

Lines 4 and 11 of the linker script instruct the linker to create sections called and in the object file. These sections are populated with machine code from the object files that the linker gets as input: line 6 says to place the machine code from all input sections into the output section, and line 13 does the same for the section. Figure 3 depicts those two sections as gray regions in the object file. In addition, the linker script adds symbols (named addresses) to the object file. The statement on line 9 sets the address of the symbol to be the number of bytes in the section. The period (“ ”) expression in a linker script evaluates to the current address in the object file, and increases as the linker populates the file with machine code. Thus, the statement “ ” on line 5 means “place a symbol called in the object file at the current address.” If that statement immediately follows the opening of a new section—as it does in Fig. 1—then it serves to demarcate the start of that section. Similarly, the statement on line 14 comes just after the linker wrote the machine code of the section and just before the curly brace that terminates the section. This means that the symbol demarcates the end of the section.

The previous paragraph illustrates how the program in Fig. 1 successfully links when the linker runs according to the script, despite the apparent problems that we highlighted. The variables in the program are -declared because they are defined in the linker script, rather than in a source file, and the linker sets their addresses. Reading those variable’s addresses in the program is thus safe. It is also safe to copy the memory region starting at the address of , because that memory region is a section of machine code that the linker allocated, and we do not stray beyond the boundary of that region because the number of bytes we copy is exactly the section’s size. The program is therefore safe, but only when linked in accordance with the script. It is therefore necessary to analyze the script, as well as the program itself, to decide the memory safety of this program.

Linker scripts pose challenges for static analysis. Current static analysis tools parse and analyze only the source code, neglecting to read the linker script if one exists. This means that they lack the following information, referring to Fig. 1 but without loss of generality: The numerical addresses of symbols can be read directly from the object file, if one exists, using a standard utility like or . However, the relationship between sections and symbols are not written to the object file. There may in fact be a symbol called that has the same address as the beginning of the section in the object file. However, the linker may have placed the symbol there coincidentally; we cannot assume that the program author explicitly demarcated the section with a symbol unless the linker script says so. To discover the symbols that demarcate object file sections, static analysis tools must therefore parse the linker script and incorporate that information into their analyses.

Without this information, static analyzers assume that the addresses of , , and are set to an arbitrary value. This admits the possibility of a memory safety violation or other undefined behavior, for exampleThis issue prevented us from verifying the safety of our boot code, which uses a linker script, using existing tools. We describe how we extended CBMC to overcome this issue in Sect. 5.5.

MMIO regions are not explicitly allocated in the code, but the addresses of these regions appear in the header files. For example, an MMIO region for the hardware straps is given with

Each of the last two macros denotes the start of a different MMIO region, leaving 0x14 bytes for the region named . Using the builtin function added to CBMC (Sect. 4.1), we declare this region in the test harness with

All of the devices accessed by the boot code are accessed via an API. For example, the API for the UART is given by

In this work, we havoc all of the devices to make our result as strong as possible. In other words, our device model allows a device read to return any value of the appropriate type, and still we can prove that (even in the context of a misbehaving device) the boot code does not exhibit a memory safety error. Because all devices have an API, we can havoc the devices using the command line option added to CBMC (Sect. 4.2), and invoke CBMC with

All devices are accessed at the byte level by computing an integer-valued address and coercing it to a pointer. For example, the following code snippets from show how reading the hardware straps from the MMIO region discussed above translates into a byte-level memory access.

In CBMC, this translates into an access into an array modeling memory at location 0x1000 + 0x110. Our optimized encoding of the theory of arrays (Sect. 4.3) enables CBMC to reason more efficiently about this kind of construct.

The and procedures are heavily used in boot code. For example, the function used to copy the stage 2 boot code from flash memory amounts to a single, large .

CBMC reasons more efficiently about this kind of code due to our loop-free model of and procedures as array operations (Sect. 4.4).

We aim to verify the memory safety of boot code that uses a custom linker script to control its runtime memory layout. Due to the issues we described in Sect. 4.5, current static analyzers cannot correctly decide the memory safety of programs that use linker scripts. We therefore extended CBMC with a linker script parser, together with code that augments CBMC’s understanding of the runtime memory layout with the information gotten from the linker script. This work can be applied to other static analyzers so that they too can more precisely reason about linker script using programs. In this section, we describe how CBMC uses the information that our parser returns.

High-level overview Figure 5 depicts how CBMC analyzes programs, together with our extensions.

To analyze a program, users first compile each of the source files with a compiler called . This compiler is a drop-in replacement for ; in fact, it runs in the background and writes the output to an object file. In addition, writes an extra section at the end of the object file that contains the source file compiled into CBMC’s internal representation (IR). This means that the object files can be linked and executed as usual, but they can also be read and analyzed by CBMC. CBMC users then link the object files into an executable (which will contain the IR for the whole program); CBMC can then load the IR from the executable file and analyze it.

In a previous section, we noted that some of the information that CBMC requires—namely, the addresses of linker script defined symbols—must be read from a fully-linked executable. We can therefore take advantage of the process depicted in Fig. 5, because that process already yields an executable file. The parser that we wrote thus takes that executable file as input, reads the addresses from the file, and sends that information to CBMC.

Programs that use linker scripts do not compile correctly without that script. We therefore extended CBMC’s linker so that it passes the linker script to . We also parse the linker script to get the other information that CBMC requires: the mapping from section names to the names of the symbols that demarcate the section. Therefore, when a user now runs CBMC over an executable, it no longer immediately analyzes the loaded IR. Instead, if the codebase contained a linker script, CBMC passes the executable and linker script to the parser, and then instruments the IR with the information that the parser returns. CBMC then analyzes this augmented IR, which now contains enough information to correctly decide memory safety.

Parser output Our parser takes a linker script, together with an object file linked according to that script, as input. Given the linker script in Fig. 1 and the object file in Fig. 3, our parser would emit the JSON-formatted map in Fig. 6.

There are two top-level keys in the map. The key contains the memory address of every symbol in the object file. If there are sections whose start address, end address, or size was demarcated by a symbol, then that information will be in the key. For every such section in the object file, the key maps the section’s name to:Recall that static analysis in the presence of linker scripts is imprecise because the linker script contains information that does not exist in the source code. When CBMC receives the linker parser output, it therefore transforms the program’s IR by adding this missing information. There are three transformations that CBMC makes:We describe these transformations, illustrated in Fig. 7, in the next paragraphs.

Type transformation We transform the intermediate representation of the target program so that it contains the information needed to decide its memory safety. Static analyzers must ensure that linker defined symbols have the address that the linker assigned to them. However, it is not possible to assign a value to an address (i.e. ) in C, since that is the linker’s job. Our solution is to change the program such that we assign directly to the variable, rather than to the variable’s address. However, since some scalar types (like ) cannot contain arbitrary memory addresses, we change the declaration of linker defined variables to make them pointer types, if they were not already. We also remove the qualifier, so that we can define the variables (rather than just declaring them). Finally, we also change all accesses to linker defined variables in the program, such that they correctly access the pointer value (rather than the original variable address).

The linker manual [14] sets the convention of declaring linker defined variables to have type . However, linker defined variables can be declared as having any type, since only their address may be accessed from the program (so the bit width of the variable’s value is immaterial). Many programmers do declare linker defined variables as having type , , or something else; furthermore, accesses to of type can sometimes be preprocessed into . We give the correct pointer type to the declaration no matter what the original type was.

Address fixup and memory allocation After performing the previous step, it is possible to assign the addresses of linker defined symbols to their associated variables in the IR. We do this assignment in , which is a function that CBMC symbolically executes just before executing . We also use that function to tell CBMC that the memory regions corresponding to object file sections are allocated, using the directive. This ensures that CBMC does not report a memory safety violation when the program accesses memory in those regions.

Application to AWS boot code The linker script used in AWS boot code calls on linker defined memory regions, in a similar manner to Fig. 1. It defines a region to hold the stage 2 binary and passes the address and size of the region as the addresses of the symbols and .

The code declares the symbols as externally defined, and uses a pair of macros to convert the addresses of the symbols to an address and a constant before use.

CBMC’s new approach to handling linker scripts modifies the CBMC intermediate representation of this code as described in the previous paragraphs.

Scope and limitations Our linker script parser, distributed with the CBMC source code [13], recognizes a subset of the linker command language. This subset is sufficient to enable CBMC to determine the memory safety of the AWS boot code mentioned above. The full language contains many additional constructs that were not used in the AWS linker script, but which would need to be considered by static analyses for memory safety. One example is access control: linker scripts can designate sections as being readable, writeable, or executable at runtime. It is a segmentation violation to read from or write to sections that do not have the correct permission; future work would allow static analysis tools to detect the possibility of such accesses. Linkers also place sections according to the padding constraints imposed by particular machine architectures and calling conventions, and the linker language includes constructs for fine-tuning or overriding these constraints. If the correctness of the code depends on data being padded according to explicit linker directives, then analysis tools would need to understand these directives to correctly decide memory safety.

Our work targets linkers that emit object files in the Executable and Linkable Format (ELF), specified in [53]. ELF is used on modern BSD and Linux-based operating systems; [42] is a reference work on linkers and loaders that also describes the linkers for other object formats, like COFF and PE (used on Microsoft Windows) and Mach-O (used on macOS).

The implementation of our linker script parser can take any linker script as input; it is designed to ignore any linker script construct that it does not understand. Thus, it currently extracts only the section and symbol layout information described earlier in this section. It should be straightforward to extend the parser to parse and emit information about additional linker language directives for programs whose memory safety depends on the meaning of those directives.

Running CBMC on the test harness above as a job under AWS Batch, it finished successfully in 10:02 min. It ran on a 16-core server with 122 GiB of memory running Ubuntu 14.04, and consumed one core at 100% using 5 GiB of memory. The new encoding of arrays improved this time by 45 s.

The boot code consists of 783 lines of statically reachable code, meaning the number of lines of code in the functions that are reachable from the test harness in the function call graph. CBMC achieves complete code coverage, in the sense that every line of code CBMC fails to exercise is dead code. An example of dead code found in the boot code is the default case of a switch statement whose cases enumerate all possible values of an expression.

The boot code consists of 98 loops that fall into two classes. First are -loops with constant-valued expressions for the upper and lower bounds. Second are loops of the form and code inspection yields a bound on . Thus, it is possible to choose loop bounds that cause all loop-unwinding assertions to hold, making CBMC’s results sound for boot code.