Saturday, September 28, 2019

Formal, Erdős, Rings, and SMM

This blog is a mix of a few topics. To begin, I have always been on the outlook for how to scale quality via tools, if possible. I continually hope that there techniques to help close that crazy semantic gap between documentation and code. To that end I enjoyed a recent talk on Everest which provides a practical realization of generating usable C code from a specification. I especially enjoyed the portion of the talk where the developer had to integrate feedback from the Firefox team on how to make the code 'look better.' When working with I saw that one of the primary challenges in UEFI code generation involving production of readable source code.

This does not mean there is no place for formal methods in the firmware space, though. For example, the formalization of EFI FAT32 provides confidence in the design of the structures, although it doesn't necessarily lead to formally validated software objects. And the space of employing computers for maths continues to get more exciting

In general, math can be your friend. And speaking of mathematicians, I was always intrigued by folks who mentioned their Erdős numberős_number. Viewing that specific wikipedia entry I noticed Leslie Lamport in the '3' category. This reminded me of the heady days of DEC research and my former Intel colleague Mark Tuttle who had worked there with Lamport. Not surprisingly, Mark co-authored a paper with Leslie, giving him an Erdős number of '4'. And since I co-authored a paper with Mark, that gives me an Erdős number of '5'. As wikipedia only mentions the cohort class up to 3, I suspect some exponential blow up of any numbers beyond that Nevertheless I still find it to be a pretty cool detail.

[1/11/2022] correction.
co-authored 4 papers with
Noga Alon
co-authored 1 paper with
Mark R. Tuttle
co-authored 1 paper with
distance = 3

And on the topic of cool details, it is always exciting to see the evolution of UEFI security in the market, including work done by Apple

for driver isolation. The UEFI specification has API's to abstract access to resources, and we even modeled said resources via a Clark Wilson analysis slides 73+.

The slides commenced with a summary of the isolation rules, and then a mapping of the rules to the important boot flows of host firmware.

The flows begin with the normal boot, or S5,

and continue with the S3 wake from sleep event (eschewed these days in lieu of S0ix)

and culminates with a boot flow for a flash update. This is typically the boot response to an UpdateCapsule invocation wherein an update-across-reset (versus runtime update in SMM or BMC) is employed.

With these rules, the OEM-only extensible compartment should be isolated from the 3rd party pre-OS extensible compartment (e.g., option ROM's) and extensible 3rd party runtime (e.g., OS). This analysis was used to inform work in the standards body and open source on what defenses we should erect. We refreshed some of this type of analysis recently in Regrettably we added a code signing guard in the mid-2000's (e.g., UEFI Secure Boot) but we didn't provide inter-agent isolation.

As a historical note, we talk about isolation, including rings, in for SMM using user mode and paging (page 10) in 2015 and an earlier mention of pushing EFI drivers into ring 3 in the now expired filed back in 2002 (17 years ago, gasp).

Given the 1999 inception of EFI and 2001 for the EFI driver model, the challenge has been application compatibility and delivering these features to market given their later addition. To that end I must given credit to Apple for their work in this space, especially as true innovation is delivering the solution to market in my view .

On other oddities from the past and SMM, I was curious about the first mention of System Management Mode (SMM).  This archaeology was also motivated by testing the claim wherein technology is most fully described in its initial product introduction, with further evolution having successively fewer details given industry practice in the domain. Since the CPU mode was introduced in the 386SL, I found the following in which the feature is first described, although the acronym "SMM" was never used. I especially enjoyed this quote from the datasheet:

"Since system management software always runs in the same mode, OEM firmware only needs to provide a single set of SMI service routines. Since real mode is essentially a subset of each of the other modes, it is generally the one for which software development is most straight-forward. SMI firmware developers therefore need not be concerned with the virtual memory system, page translation tables initialized by other tasks, interprocess protection mechanisms, and so forth. "
(page 58).

Especially ironic the mention of paging given the earlier topic in this blog on isolation and the document Some of the venerable collateral does describe the smi# pin, though.  And a later book on the 486SL has source code for an assembly language 'kernel' to handle dispatching of event handlers. In that latter book, it was nice to see a mention of my former colleague and co-author Suresh, too.

Well, so much for September 2019 blogging. I did my usual wandering across topics. I should probably produce more bite-sized blogs, one per topic, but what would be the fun in that.