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 https://support.apple.com/boot-camp https://discussions.apple.com/thread/252021896 or the support of 3rd party OS's https://www.zdnet.com/article/top-apple-exec-native-windows-10-on-m1-macs-is-a-choice-microsoft-needs-to-make/.
Does that mean the boot paradigm of the Macs has changed from UEFI http://refit.sourceforge.net/info/boot_process.html? 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 https://developer.apple.com/videos/play/wwdc2020/10686 at 16:22
which mentions that the boot process is leveraged from the iPhone/iPad, namely iBoot https://en.wikipedia.org/wiki/IBoot.
The native iBoot launch was confirmed by Apple UEFI engineer https://twitter.com/NikolajSchlej/status/1275951574200709120, along with using device tree https://elinux.org/Device_Tree_What_It_Is in lieu of ACPI https://twitter.com/NikolajSchlej/status/1275951827754774528. 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 https://en.wikipedia.org/wiki/Open_Firmware whereas ACPI was 1996 https://en.wikipedia.org/wiki/Advanced_Configuration_and_Power_Interface#:~:text=First%20released%20in%20December%201996,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 https://en.wikipedia.org/wiki/Unified_Extensible_Firmware_Interface.
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 https://github.com/tianocore/edk2/tree/master/UefiPayloadPkg providing an EDK2-based implementation of UEFI for coreboot https://doc.coreboot.org/ and slim bootloader https://slimbootloader.github.io/index.html. We discussed this in figure 6-17 of https://link.springer.com/chapter/10.1007/978-1-4842-0070-4_6 and we are trying to generalize the use of payloads in https://github.com/universalpayload. We compare a T2-based secure boot chain to other implementations in chapter 4 of https://www.amazon.com/Building-Secure-Firmware-Armoring-Foundation/dp/1484261054, 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 https://www.chromium.org/chromium-os/chromiumos-design-docs/disk-format, 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 https://cfp.osfc.io/media/osfc2020/submissions/SLFJTN/resources/OSFC2020_Rust_EFI_Yao_Zimmer_NDK4Dme.pdf.
Another interesting example of stacking a Rust-based UEFI implementation on an alternate platform initialization layer can be found in https://github.com/retrage/rust-hypervisor-firmware/tree/coreboot-support, 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 https://www.freertos.org/2020/02/ensuring-the-memory-safety-of-freertos-part-1.html about using the C Bounded Model Checker (CBMC) https://www.cprover.org/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 https://www.amazon.com/Building-Secure-Firmware-Armoring-Foundation/dp/1484261054, 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 https://assets.amazon.science/d0/de/cbec0b4547e3ae7ff077f8aa978f/code-level-model-checking-in-thesoftware-development-workflow.pdf. This type of analysis is much more relevant to my day-job than the former treatise on FM they wrote regarding TLA https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext, although some of Hillel Wayne's https://www.hillelwayne.com/post/why-dont-people-use-formal-methods/ 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 https://linuxplumbersconf.org/event/7/contributions/780/attachments/514/925/LPC2020_-_Protected_KVM_.pdf. I haven't dug into this too much, but I wonder if it is aligned with Google Project Oak, including the Hafnium hypervisor https://hafnium.googlesource.com/hafnium/+/HEAD/docs/Architecture.md and its Coq based verification https://github.com/project-oak/hafnium-verification/tree/hfo2/coq-verification? Or some other KVM-focused verification?
As a parting note, I'd like to thank the work of Tim Lewis https://uefi.blogspot.com/ as the technical reviewer of https://link.springer.com/book/10.1007/978-1-4842-6106-4 and Leendert Van Doorn https://www.paramecium.org:4443/~leendert/ for writing the preface. I have appreciated the opportunity to work with these two technical leaders in various roles since the 2000's.
