On Apr 13, 2021, at 12:31 AM, Marvin Häuser <mhaeuser@posteo.de> wrote:

Hey Mike,
Hey Nate,

I'm not 100 % sure I get what you mean. The interfaces of the two solutions are not compatible (however I could write wrapper code to shim the old into the new I suppose?), so on-the-fly switching between the two would be inconvenient. I do plan to keep the old library around and guard it with the deprecated interfaces macro, for out-of-tree code, however. The new library interfaces will probably be something like PeCoffLib2, PeCoffDebugLib2, maybe more.

I'm also not sure what on-the-fly switching would accomplish, as testing with the old loader allows broken images to be loaded, i.e. just because something "works" with the old code but not the new, it doesn't mean that the new code is broken.

Instead of debugging with two libraries, I rather want to make sure this thing is rock-solid before even sending out the patches. For this I would like to build a small EFI file database to parse and load from userland, checking for image acceptance and memory safety. This would include several versions of Windows and macOS bootloaders, Option ROMs (NVIDIA and AMD GOP, iPXE), tools (memtest), and so on. If you have anything you want to have especially tested, please let me know.

Best regards,
Marvin

13.04.2021 02:56:22 Desimone, Nathaniel L <nathaniel.l.desimone@intel.com>:

Hi Marvin,

I agree with Mike K that having both the new strict loader and the old loader co-exist for some time may be the best option. That will give the ecosystem time to test the new loader and correct any issues that arise from its introduction.

Best Regards,
Nate

-----Original Message-----
From: Kinney, Michael D <michael.d.kinney@intel.com>
Sent: Monday, April 12, 2021 5:20 PM
To: Marvin Häuser <mhaeuser@posteo.de>; devel@edk2.groups.io; Desimone, Nathaniel L <nathaniel.l.desimone@intel.com>; Laszlo Ersek <lersek@redhat.com>; Andrew Fish <afish@apple.com>; Kinney, Michael D <michael.d.kinney@intel.com>
Subject: RE: [edk2-devel] [GSoC proposal] Secure Image Loader

Hi Marvin,

If it has not already been considered, one option is to submit a new instance of the PE/COFF Library, so both the existing one and the new one are available to the ecosystem.

This allows you to be successful in submitting code outlined in your proposal and gives the ecosystem time to evaluate and decide when/if to switch from the old to the new.

Mike

-----Original Message-----
From: Marvin Häuser <mhaeuser@posteo.de>
Sent: Monday, April 12, 2021 10:22 AM
To: devel@edk2.groups.io; Desimone, Nathaniel L
<nathaniel.l.desimone@intel.com>; Laszlo Ersek <lersek@redhat.com>;
Andrew Fish <afish@apple.com>; Kinney, Michael D
<michael.d.kinney@intel.com>
Subject: Re: [edk2-devel] [GSoC proposal] Secure Image Loader

Good day Nate,

As you seem to be mostly in charge of the GSoC side of things, I
direct this at you, but of course everyone is welcome to comment.

I think I finished my first round of investigations just in time for
the deadline. You can find a list of BZs attached[1]. Please note that
1) some are declared security issues and may not be publicly
accessible, and 2) that this list is far from complete. I only added
items that are
a) not implicitly fixed by "simply" deploying the new Image Loader
(*some* important prerequisites are listed), and b) I am confident are
actual issues (or things to consider) I believe to know how to approach.

I have taken notes about more things, e.g. the existence of the
security architectural protocols, which I could not find a rationale
for. I can prepare something for this matter, but it really needs an
active discussion with some of the core people. I'm not sure delayed
e-mail discussion is going to be enough, but there is an official IRC
I suppose. :) I hope we can work something out for this.

I also hope this makes it clearer why I don't believe that we need to
"fill" 10 weeks, but rather the opposite. This is not a matter of
replacing a library instance, but the whole surrounding ecosystem
needs to follow for the changes to make sense. And as I tried to make
clear in my discussion with Michael Brown, I am not keen on preserving
backwards-compatibility with platform code (i.e. PEI, DXE, things we
consider "internal"), as most of it should be controlled by EDK II
already. This of course does *not* include user code (OROMs,
bootloaders, ...), for which I want to provide the *option* to lock
some of them out for security, but with sane defaults that will ensure
good compatibility.

I'd like to thank Michael Brown for his cooperation and support,
because we recently landed changes in iPXE to allow for the strictest
image format and permission constraints currently possible[2].

I will have to rework the submitted proposal to reflect the new
knowledge. To be honest, seeing how the BZs kept rolling in, I am not
convinced an amazing amount of mainlining can be accomplished during
the
10 weeks. It may have to suffice to have a publicly accessible
prototype (e.g. OVMF) and a subset of the planned patches on the list.
I hope you can manage to provide some feedback before the deadline passes tomorrow.

Thank you in advance!

Best regards,
Marvin

[1]
https://bugzilla.tianocore.org/show_bug.cgi?id=3315
https://bugzilla.tianocore.org/show_bug.cgi?id=3316
https://bugzilla.tianocore.org/show_bug.cgi?id=3317
https://bugzilla.tianocore.org/show_bug.cgi?id=3318
https://bugzilla.tianocore.org/show_bug.cgi?id=3319
https://bugzilla.tianocore.org/show_bug.cgi?id=3320
https://bugzilla.tianocore.org/show_bug.cgi?id=3321
https://bugzilla.tianocore.org/show_bug.cgi?id=3322
https://bugzilla.tianocore.org/show_bug.cgi?id=3323
https://bugzilla.tianocore.org/show_bug.cgi?id=3324
https://bugzilla.tianocore.org/show_bug.cgi?id=3326
https://bugzilla.tianocore.org/show_bug.cgi?id=3327
https://bugzilla.tianocore.org/show_bug.cgi?id=3328
https://bugzilla.tianocore.org/show_bug.cgi?id=3329
https://bugzilla.tianocore.org/show_bug.cgi?id=3330
https://bugzilla.tianocore.org/show_bug.cgi?id=3331

[2] https://github.com/ipxe/ipxe/pull/313

On 06.04.21 11:41, Nate DeSimone wrote:

Hi Marvin,

Great to meet you and welcome back! Glad you hear you are
interested! Completing a formal verification of a PE/COFF

loader is certainly impressive. Was this done with some sort of
automated theorem proving? It would seem a rather arduous task doing
an inductive proof for an algorithm like that by hand! I completely agree with you that getting a formally verified PE/COFF loader into mainline is undoubtably valuable and would pay security dividends for years to come.

Admittedly, this is an area of computer science that I don't have a
great deal of experience with. The furthest I have

gone on this topic is writing out proofs for simple algorithms on
exams in my Algorithms class in college. Regardless you have a much
better idea of what the current status is of the work that you and
Vitaly have done. I guess my only question is do you think there is
sufficient work remaining to fill the 10 week GSoC development window? Certainly we can use some of that time to perform the code reviews you mention and write up formal ECRs for the UEFI spec changes that you believe are needed.

Thank you for sending the application and alerting us to the great
work you and Vitaly have done! I'll read your paper

more closely and come back with any questions I still have.

With Best Regards,
Nate

-----Original Message-----
From: devel@edk2.groups.io <devel@edk2.groups.io> On Behalf Of
Marvin Häuser
Sent: Sunday, April 4, 2021 4:02 PM
To: devel@edk2.groups.io; Laszlo Ersek <lersek@redhat.com>; Andrew
Fish <afish@apple.com>; Kinney, Michael D
<michael.d.kinney@intel.com>
Subject: [edk2-devel] [GSoC proposal] Secure Image Loader

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