[GSoC proposal] Secure Image Loader

["Marvin Häuser" <mhaeuser@posteo.de>]

Good day everyone,

I'll keep the introduction brief because I've been around for a while 
now. :)
I'm Marvin Häuser, a third-year Computer Science student from TU 
Kaiserslautern, Germany. Late last year, my colleague Vitaly from ISP 
RAS and me introduced a formally verified Image Loader for UEFI usage at 
ISP RAS Open[1] due to various defects we outlined in the corresponding 
paper. Thank you once again Laszlo for your *incredible* review work on 
the publication part.

I now want to make an effort to mainline it, preferably as part of the 
current Google Summer of Code event. To be clear, my internship at ISP 
RAS has concluded, and while Vitaly will be available for design 
discussion, he has other priorities at the moment and the practical part 
will be on me. I have previously submitted a proposal via the GSoC 
website for your review.

There are many things to consider:
1. The Image Loader is a core component, and there needs to be a 
significant level of quality and security assurance.
2. Being consumed by many packages, the proposed patch set will take a 
lot of time to review and integrate.
3. During my initial exploration, I discovered defective PPIs and 
protocols (e.g. returning data with no corresponding size) originating 
from the UEFI PI and UEFI specifications. Changes need to be discussed, 
settled on, and submitted to the UEFI Forum.
4. Some UEFI APIs like the Security Architecture protocols are 
inconveniently abstract, see 5.
5. Some of the current code does not use the existing context, or 
accesses it outside of the exposed APIs. The control flow of the 
dispatchers may need to be adapted to make the context available to 
appropriate APIs.

But obviously there are not only unpleasant considerations:
A. The Image Loader is mostly formally verified, and only very few 
changes will be required from the last proven state. This gives a lot of 
trust in its correctness and safety.
B. All outlined defects that are of critical nature have been fixed 
successfully.
C. The Image Loader has been tested with real-world code loading 
real-world OSes on thousands of machines in the past few months, 
including rejecting malformed images (configurable by PCD).
D. The new APIs will centralise everything PE, reducing code duplication 
and potentially unsafe operations.
E. Centralising and reduced parse duplication may improve overall boot 
performance.
F. The code has been coverage-tested to not contain dead code.
G. The code has been fuzz-tested including sanitizers to not invoke 
undefined behaviour.
H. I already managed to identify a malformed image in OVMF with its help 
(incorrectly reported section alignment of an Intel IPXE driver). A fix 
will be submitted shortly.
I. I plan to support PE section permissions, allowing for read-only data 
segments when enabled.

There are likely more points for both lists, but I hope this gives a 
decent starting point for discussion. What are your thoughts on the 
matter? I strongly encourage everyone to read the section regarding 
defects of our publication[2] to better understand the motivation. The 
vague points above can of course be elaborated in due time, as you see fit.

Thank you for your time!

Best regards,
Marvin


[1] https://github.com/mhaeuser/ISPRASOpen-SecurePE
[2] https://arxiv.org/pdf/2012.05471.pdf