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 http://vzimmer.blogspot.com/2013/12/better-living-through-tools.html, 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 https://nwcpp.org/author/lloyd-moore.html on Everest which provides a practical realization of generating usable C code https://github.com/denismerigoux/hacl-star/tree/master/snapshots/hacl-c 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 https://github.com/termite2/Termite I saw that one of the primary challenges in UEFI code generation https://www.intel.com/content/dam/www/public/us/en/documents/research/2013-vol17-iss-2-intel-technology-journal.pdf 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 http://eptcs.web.cse.unsw.edu.au/Published/ACL22018/Proceedings.pdf 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 https://www.vice.com/en_us/article/8xwm54/number-theorist-fears-all-published-math-is-wrong-actually.
In general, math can be your friend. And speaking of mathematicians, I was always intrigued by folks who mentioned their Erdős number https://en.wikipedia.org/wiki/
This does not mean there is no place for formal methods in the firmware space, though. For example, the formalization of EFI FAT32 http://eptcs.web.cse.unsw.edu.au/Published/ACL22018/Proceedings.pdf 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 https://www.vice.com/en_us/article/8xwm54/number-theorist-fears-all-published-math-is-wrong-actually.
In general, math can be your friend. And speaking of mathematicians, I was always intrigued by folks who mentioned their Erdős number https://en.wikipedia.org/wiki/
[1/11/2022] correction.
from https://www.csauthors.net/distance/paul-erdos/vincent-zimmer the number is '3' via
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 https://twitter.com/NikolajSchlej/status/1159602635176939520
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 https://cansecwest.com/slides/2015/UEFI%20open%20platforms_Vincent.pptx 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 https://edk2-docs.gitbooks.io/understanding-the-uefi-secure-boot-chain/comparing-clark-wilson-and-uefi-secure-boot.html. 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 https://firmware.intel.com/sites/default/files/resources/A_Tour_Beyond_BIOS_Supporting_SMM_Resource_Monitor_using_the_EFI_Developer_Kit_II.pdf 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 https://patents.google.com/patent/US20030188173 filed back in 2002 (17 years ago, gasp).
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 http://bitsavers.trailing-edge.com/components/intel/80386/240852-002_386SL_Technical_Overview_1991.pdf 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 https://firmware.intel.com/sites/default/files/resources/A_Tour_Beyond_BIOS_Supporting_SMM_Resource_Monitor_using_the_EFI_Developer_Kit_II.pdf. Some of the venerable collateral does describe the smi# pin http://bitsavers.trailing-edge.com/components/intel/80386/240814-005_386SL_Data_Book_Jul92.pdf, though. And a later book https://www.amazon.com/Intels-Architecture-Designing-Applications-McGraw-Hill/dp/0079113362 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 https://www.amazon.com/Beyond-BIOS-Developing-Extensible-Interface/dp/1501514784/ 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.
1 comment:
"I saw that one of the primary challenges in UEFI code generation (...) involving production of readable source code."
Well, that's already the issue with UEFI as a whole I think. Coming from other architectures (PowerPC, ARM), this is really an over-engineered stuff.
Code amount does not help as well: Same order of magnitude than Linux Kernel for EDK2 for only a fraction of the functionality and a few "user space" tools with a clunky shell that reminds DOS. Well, having 3 separate phases (SEC/PEI/DXE) means having some commonalities coded 3 times but this does not explain anything + this is x86 centric.
Well, ARM looks to be a target. Probably pushed by Microsoft attempts on this architecture + the fact they always relied on boot loader services (from so called "BIOS Interrupts" that soon become a boot viruses target to current UEFI RT services... that triggered another layer of complexity with secure-boot to avoid history repeats itself!). Not sure this'll meet favours outside of winArm diversification attempts from winTel that did not succeed for now.
So, if specifications are over-complex I'm not sure code generators will do a better job! That's probably why google avoided using a UEFI payload on coreboot for it's x86 based chromebooks and on server side, were boot times with UEFI is an heavy issue, we see attempts to replace UEFI with a stripped Linux kernel that will boot a full Linux in a few seconds instead of minutes.
Post a Comment