Monday, November 23, 2020

Different boot and testing schemes

In the news, interesting to see the details of the M1-based Apple devices. As a firmware person, I was curious about how the machines boot. 

They mention the omission of bootcamp or the support of 3rd party OS's

Does that mean the boot paradigm of the Macs has changed from UEFI Apple was never fully UEFI compliant and often eschewed more complex capabilities like SMM-protected Authenticated Variables and other rich runtime services, although they did support ACPI.

The answer was formally revealed in the video at 16:22

which mentions that the boot process is leveraged from the iPhone/iPad, namely iBoot

The native iBoot launch was confirmed by Apple UEFI engineer, along with using device tree in lieu of ACPI Flattened Device Tree predates ACPI and was part of how the original PowerPC MACs booted, with OpenFirmware Forth-based FCode and FDT as the equivalent of UEFI/ACPI for the programmatic and declarative runtime tables interfaces, respectively. Open Firmware was circa 1994 whereas ACPI was 1996,Play%20BIOS%20(PnP)%20Specification.&text=ACPI%20defines%20a%20hardware%20abstraction,UEFI)%20and%20the%20operating%20systems., respectively. EFI, the precursor the UEFI, is the youngest of all three, dating its earliest appearance in 1998

As Apple showed in slide 14, the T2-based Mac's already support the bridgeOS kernel going from iBoot to UEFI. This sort of layering of UEFI implementations on top of a non-PI based platform code is pretty common, with the providing an EDK2-based implementation of UEFI for coreboot and slim bootloader We discussed this in figure 6-17 of and we are trying to generalize the use of payloads in We compare a T2-based secure boot chain to other implementations in chapter 4 of, too.

I suspect the disk layout is still based upon the GUIDed Partition Table (GPT), which was an invention of EFI. You can support GPT even without performing a non-UEFI OS boot, as showed by Chromebooks, for example. To support a non-UEFI OS you simple can omit the EFI System Partition (ESP) and have your boot loader load a kernel from some arbitrary GUID-defined partition type.

We also show how the concept of a phase-based boot and clean interfaces to payloads enables more radical firmware stacks, such as slide 24 of


Another interesting example of stacking a Rust-based UEFI implementation on an alternate platform initialization layer can be found in, too, that I saw on the open source firmware's oreboot slack channel. 

Speaking of another A-prefixed company that's not Apple, Amazon has been doing some pretty interesting things in firmware. Former Intel colleague Mark Tuttle's work in mentioned in the write-up about using the C Bounded Model Checker (CBMC) to ensure memory safety of FreeRTOS. This is a nice balance of providing better assurance with an existing type-weak language like C versus the forklift upgrade to something like Rust. We discuss CBMC a bit in chapter 21 of, including an example of usage in listing 21-2. 

This work in the rebar-embossed book is nothing like the fully operationalized example of the real-time OS listed above, though. Beyond this specific work, I appreciate how Amazon endeavors to make formal methods more developer friendly, as described in the work by Nathan, Mark, and their colleagues in This type of analysis is much more relevant to my day-job than the former treatise on FM they wrote regarding TLA, although some of Hillel Wayne's work may help build a bridge for me. More examples of the good stuff published by their engineers/'builders' that I also referenced in my last blog posting.

And formal verification of system software is popping up in other places, such as the mention "Formal verification of the code running at EL2" in I haven't dug into this too much, but I wonder if it is aligned with Google Project Oak, including the Hafnium hypervisor and its Coq based verification Or some other KVM-focused verification? 

As a parting note, I'd like to thank the work of Tim Lewis as the technical reviewer of and Leendert Van Doorn for writing the preface. I have appreciated the opportunity to work with these two technical leaders in various roles since the 2000's.