Topics

[GSoC proposal] Secure Image Loader


Marvin Häuser
 

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


Nate DeSimone
 

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




Marvin Häuser
 

Good day Nate,

Comments are inline.

Best regards,
Marvin

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 would call it "semi-automated", a great deal of intermediate goals (preconditions, postconditions, invariants, assertions, ...) were required to show all interesting properties. But yes, the actual proof steps are automated by common SMT solvers. It was done using the AstraVer Toolset and ACSL, latter basically a language to express logic statements with C-like syntax.

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.
I'm glad to hear that. :)

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?
Please don't get me wrong, but I would be surprised if the UEFI specification changes I'd like to discuss alone would be completed within 10 weeks, let alone implementation throughout the codebase. While I think the plain amount of code may be a bit less than say a MinPlatform port, the changes are much deeper and require much more caution to avoid regressions (e.g. by invalidating undocumented assertions). This sadly is not a matter of just replacing the underlying library implementation or "plug-in and play" at all. It furthermore affects many parts of the stack, the core dispatchers used for all platforms, image emulation (EBC), UEFI userland emulation (EmuPkg), and so on. I was rather worried the scope is too broad time-wise, but it can be narrowed/widened as you see fit really. This is one of *the* core components used on millions of device, and many package maintainers need to review and validate the changes, this must really be done right the first try. :)

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.
I believed that was part of the workload, yes, but even without it I think there is plenty to do.

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.
Thank you, I will gladly explain anything unclear. Just try to not give Laszlo too many flashbacks. :)


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






Michael Brown
 

On 05/04/2021 00:01, Marvin Häuser wrote:
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.
Would any of these changes break backwards compatibility? With the UEFI development model, any protocol that has ever existed in the specification will practically need to always be supported in that form: breaking backwards compatibility is simply not an option.

For example: there is a fundamental design flaw in the LoadImage() and StartImage() API that makes it logically impossible for arbitrary code to install an EFI_LOADED_IMAGE_PROTOCOL instance (see https://github.com/ipxe/ProxyLoaderPkg/#why-is-it-needed for details on this). But there's zero chance that this design flaw will ever be fixed, because there's no way to eliminate code that relies on the existing LoadImage()/StartImage() APIs.

So: if the formally verified image loader can fit within the constraints of "must not modify any externally exposed APIs" then it sounds like a potentially good idea. If it requires breaking changes to public APIs then I don't see how it could be integrated in practice.

Thanks,

Michael


Marvin Häuser
 

Good day Michael,

Sorry, but I do not see why this would be the case. In fact the solution is (temporary) co-existence, as already is the case with InstallProtocolInterface() and InstallMultipleProtocolInterfaces(). As the new APIs would be a superset of the old ones, latter can be implemented with former, as also previously done (*2_PROTOCOL instances and shims in e.g. EdkCompatibilityPkg). In some cases, the original protocol interfaces were actually deprecated successfully from the EDK II code base. I would probably offer PCDs to disable the expose of the old APIs, so platforms with little need for backwards-compatibility and more focus on security can tighten the constraints as they see fit. Considering the shimmed interfaces for the old protocols/PPIs/... can be implemented on top of the new public API, and the public API must not change, this code would be practically maintenance-free too in my opinion.

As for your example, I do not believe what is described is "broken". Ideally, the platform loads all images to have a centralized place for the security verification. While we do a very similar thing at Acidanthera with our OpenCore bootloader to support Apple Secure Boot, I hope you agree that this behaviour is actually a risky hack (now there are two points of failure for security verification). Meanwhile, the changes I'd like to propose to the current interfaces are mandatory to ensure secure parsing of data. Lastly, this sort of API I would not expect to be accessed outside of platform code.

Am I missing or overlooking something?

Best regards,
Marvin

On 07.04.21 23:05, Michael Brown wrote:
On 05/04/2021 00:01, Marvin Häuser wrote:
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.
Would any of these changes break backwards compatibility?  With the UEFI development model, any protocol that has ever existed in the specification will practically need to always be supported in that form: breaking backwards compatibility is simply not an option.

For example: there is a fundamental design flaw in the LoadImage() and StartImage() API that makes it logically impossible for arbitrary code to install an EFI_LOADED_IMAGE_PROTOCOL instance (see https://github.com/ipxe/ProxyLoaderPkg/#why-is-it-needed for details on this).  But there's zero chance that this design flaw will ever be fixed, because there's no way to eliminate code that relies on the existing LoadImage()/StartImage() APIs.

So: if the formally verified image loader can fit within the constraints of "must not modify any externally exposed APIs" then it sounds like a potentially good idea.  If it requires breaking changes to public APIs then I don't see how it could be integrated in practice.

Thanks,

Michael




Michael Brown
 

On 07/04/2021 22:31, Marvin Häuser wrote:
Sorry, but I do not see why this would be the case. In fact the solution is (temporary) co-existence, as already is the case with InstallProtocolInterface() and InstallMultipleProtocolInterfaces()
InstallMultipleProtocolInterfaces() is not a breaking change: the existence of InstallMultipleProtocolInterfaces() does not require any change to the way that InstallProtocolInterface() is implemented or consumed.

Code written before the invention of InstallMultipleProtocolInterfaces() will still work now, with no modifications required.

the new APIs would be a superset of the old ones, latter can be implemented with former, as also previously done (*2_PROTOCOL instances and shims in e.g. EdkCompatibilityPkg). In some cases, the original protocol interfaces were actually deprecated successfully from the EDK II code base. I would probably offer PCDs to disable the expose of the old APIs, so platforms with little need for backwards-compatibility and more focus on security can tighten the constraints as they see fit. Considering the shimmed interfaces for the old protocols/PPIs/... can be implemented on top of the new public API, and the public API must not change, this code would be practically maintenance-free too in my opinion.
You have to remember that UEFI is not a monolithic codebase with a single maintaining organisation. Implementing a *2_PROTOCOL and deprecating the original just causes pain for all the code in the world that is maintained outside of the EDK2 repository, since that code now has to support *both* the old and new protocols.

As for your example, I do not believe what is described is "broken".
To avoid distraction from that specific example: have a different example. The EFI_USB_IO_PROTOCOL is fundamentally broken from the perspective of implementing a network device driver, since there is simply no way to enqueue a receive buffer that will wait for the next available packet. But this won't get fixed, because it can't get fixed without breaking API compatibility.

(Incidentally, I've observed UEFI software in the wild (from Insyde) that works around these UEFI USB specification flaws by having all of the USB drivers bind to private protocols in addition to EFI_USB_IO_PROTOCOL, resulting in device drivers that point-blank fail to work with a standards-conformant UEFI USB host controller driver.)


Don't get me wrong: I *am* in favour of improving the security of EDK2, and a formally verified loader is potentially useful for that. But I could only consider it a good idea if it can be done without making breaking API changes for which I know I will personally have to maintain workarounds for the next ten years.

Thanks,

Michael


Andrew Fish
 

On Apr 7, 2021, at 2:50 PM, Michael Brown <mcb30@ipxe.org> wrote:

On 07/04/2021 22:31, Marvin Häuser wrote:
Sorry, but I do not see why this would be the case. In fact the solution is (temporary) co-existence, as already is the case with InstallProtocolInterface() and InstallMultipleProtocolInterfaces()
InstallMultipleProtocolInterfaces() is not a breaking change: the existence of InstallMultipleProtocolInterfaces() does not require any change to the way that InstallProtocolInterface() is implemented or consumed.

Code written before the invention of InstallMultipleProtocolInterfaces() will still work now, with no modifications required.

the new APIs would be a superset of the old ones, latter can be implemented with former, as also previously done (*2_PROTOCOL instances and shims in e.g. EdkCompatibilityPkg). In some cases, the original protocol interfaces were actually deprecated successfully from the EDK II code base. I would probably offer PCDs to disable the expose of the old APIs, so platforms with little need for backwards-compatibility and more focus on security can tighten the constraints as they see fit. Considering the shimmed interfaces for the old protocols/PPIs/... can be implemented on top of the new public API, and the public API must not change, this code would be practically maintenance-free too in my opinion.
You have to remember that UEFI is not a monolithic codebase with a single maintaining organisation. Implementing a *2_PROTOCOL and deprecating the original just causes pain for all the code in the world that is maintained outside of the EDK2 repository, since that code now has to support *both* the old and new protocols.

As for your example, I do not believe what is described is "broken".
To avoid distraction from that specific example: have a different example. The EFI_USB_IO_PROTOCOL is fundamentally broken from the perspective of implementing a network device driver, since there is simply no way to enqueue a receive buffer that will wait for the next available packet. But this won't get fixed, because it can't get fixed without breaking API compatibility.

(Incidentally, I've observed UEFI software in the wild (from Insyde) that works around these UEFI USB specification flaws by having all of the USB drivers bind to private protocols in addition to EFI_USB_IO_PROTOCOL, resulting in device drivers that point-blank fail to work with a standards-conformant UEFI USB host controller driver.)


Don't get me wrong: I *am* in favour of improving the security of EDK2, and a formally verified loader is potentially useful for that. But I could only consider it a good idea if it can be done without making breaking API changes for which I know I will personally have to maintain workarounds for the next ten years.
Well it is just software at the end of the day. We could always wrap any Industry Standard API (PPI, Protocol, etc) in a library function and let people chose backward compatibility vs better security. The Library Class would be owned by the edk2 Open Source project so we have more control over it.

The general UEFI (and UEFI PI) is we mostly add new things, and don’t depreciated things to maintain compatibility. So for example you can add a new Protocol to a handle so you have V1 and V2 of a protocol on the same handle. An example of this is SimpleTextIn and SimpleTextInEx. SimpleTextIn was modeled on the LCD of a serial terminal (our server roots) so it did not expose modifier keys, or have an easy way to implement snag keys so that is why SimpleTextInEx got added for the new functional.

Thanks,

Andrew Fish

Thanks,

Michael


Andrew Fish
 

Some of use also sit on the UEFI standards committees so getting changes into the specification is possible with in constraints of what the spec committees find acceptable. 

Thanks,

Andrew Fish

On Apr 7, 2021, at 3:02 PM, Andrew Fish via groups.io <afish@...> wrote:



On Apr 7, 2021, at 2:50 PM, Michael Brown <mcb30@...> wrote:

On 07/04/2021 22:31, Marvin Häuser wrote:
Sorry, but I do not see why this would be the case. In fact the solution is (temporary) co-existence, as already is the case with InstallProtocolInterface() and InstallMultipleProtocolInterfaces()

InstallMultipleProtocolInterfaces() is not a breaking change: the existence of InstallMultipleProtocolInterfaces() does not require any change to the way that InstallProtocolInterface() is implemented or consumed.

Code written before the invention of InstallMultipleProtocolInterfaces() will still work now, with no modifications required.

the new APIs would be a superset of the old ones, latter can be implemented with former, as also previously done (*2_PROTOCOL instances and shims in e.g. EdkCompatibilityPkg). In some cases, the original protocol interfaces were actually deprecated successfully from the EDK II code base. I would probably offer PCDs to disable the expose of the old APIs, so platforms with little need for backwards-compatibility and more focus on security can tighten the constraints as they see fit. Considering the shimmed interfaces for the old protocols/PPIs/... can be implemented on top of the new public API, and the public API must not change, this code would be practically maintenance-free too in my opinion.

You have to remember that UEFI is not a monolithic codebase with a single maintaining organisation.  Implementing a *2_PROTOCOL and deprecating the original just causes pain for all the code in the world that is maintained outside of the EDK2 repository, since that code now has to support *both* the old and new protocols.

As for your example, I do not believe what is described is "broken". 

To avoid distraction from that specific example: have a different example.  The EFI_USB_IO_PROTOCOL is fundamentally broken from the perspective of implementing a network device driver, since there is simply no way to enqueue a receive buffer that will wait for the next available packet.  But this won't get fixed, because it can't get fixed without breaking API compatibility.

(Incidentally, I've observed UEFI software in the wild (from Insyde) that works around these UEFI USB specification flaws by having all of the USB drivers bind to private protocols in addition to EFI_USB_IO_PROTOCOL, resulting in device drivers that point-blank fail to work with a standards-conformant UEFI USB host controller driver.)


Don't get me wrong: I *am* in favour of improving the security of EDK2, and a formally verified loader is potentially useful for that.  But I could only consider it a good idea if it can be done without making breaking API changes for which I know I will personally have to maintain workarounds for the next ten years.


Well it is just software at the end of the day. We could always wrap any Industry Standard API (PPI, Protocol, etc) in a library function and let people chose backward compatibility vs better security. The Library Class would be owned by the edk2 Open Source project so we have more control over it. 

The general UEFI (and UEFI PI) is we mostly add new things, and don’t depreciated things to maintain compatibility. So for example you can add a new Protocol to a handle so you have V1 and V2 of a protocol on the same handle. An example of this is SimpleTextIn and SimpleTextInEx. SimpleTextIn was modeled on the LCD of a serial terminal (our server roots) so it did not expose modifier keys, or have an easy way to implement snag keys so that is why SimpleTextInEx got added for the new functional. 

Thanks,

Andrew Fish

Thanks,

Michael





Marvin Häuser
 

On 07.04.21 23:50, Michael Brown wrote:
On 07/04/2021 22:31, Marvin Häuser wrote:
Sorry, but I do not see why this would be the case. In fact the solution is (temporary) co-existence, as already is the case with InstallProtocolInterface() and InstallMultipleProtocolInterfaces()
InstallMultipleProtocolInterfaces() is not a breaking change: the existence of InstallMultipleProtocolInterfaces() does not require any change to the way that InstallProtocolInterface() is implemented or consumed.

Code written before the invention of InstallMultipleProtocolInterfaces() will still work now, with no modifications required.
The same is true for the *2_PROTOCOL instances, I do not see how you distinct between them. Could you elaborate, please?

the new APIs would be a superset of the old ones, latter can be implemented with former, as also previously done (*2_PROTOCOL instances and shims in e.g. EdkCompatibilityPkg). In some cases, the original protocol interfaces were actually deprecated successfully from the EDK II code base. I would probably offer PCDs to disable the expose of the old APIs, so platforms with little need for backwards-compatibility and more focus on security can tighten the constraints as they see fit. Considering the shimmed interfaces for the old protocols/PPIs/... can be implemented on top of the new public API, and the public API must not change, this code would be practically maintenance-free too in my opinion.
You have to remember that UEFI is not a monolithic codebase with a single maintaining organisation.  Implementing a *2_PROTOCOL and deprecating the original just causes pain for all the code in the world that is maintained outside of the EDK2 repository, since that code now has to support *both* the old and new protocols.
I am aware, but actually it's not far from it nowadays. In contrast to the days of Aptio IV, I believe all big vendors maintain forks of EDK II. I know the fork nature taints the issue, but also see last quote comment.

As for your example, I do not believe what is described is "broken".
To avoid distraction from that specific example: have a different example.  The EFI_USB_IO_PROTOCOL is fundamentally broken from the perspective of implementing a network device driver, since there is simply no way to enqueue a receive buffer that will wait for the next available packet.  But this won't get fixed, because it can't get fixed without breaking API compatibility.
I see that there is no EFI_USB_IO2_PROTOCOL instance to argue by. Yet there are EFI_BLOCK_IO2_PROTOCOL and EFI_LOAD_FILE2_PROTOCOL. Former, in my opinion, close in nature to your your example, and latter close to the nature on what I plan to propose. Sorry, but I do not see how what I suggest has not been done multiple times in the past already.

Please also look at it from an angle of trust. How can I trust the "secure" advertisements of UEFI / EDK II when the specification *dictates* the usage of intrinsically insecure APIs?
The consequence for security-critical situations would be to necessarily abandon UEFI and come up with a new design. In who's interest is this?

(Incidentally, I've observed UEFI software in the wild (from Insyde) that works around these UEFI USB specification flaws by having all of the USB drivers bind to private protocols in addition to EFI_USB_IO_PROTOCOL, resulting in device drivers that point-blank fail to work with a standards-conformant UEFI USB host controller driver.)


Don't get me wrong: I *am* in favour of improving the security of EDK2, and a formally verified loader is potentially useful for that.  But I could only consider it a good idea if it can be done without making breaking API changes for which I know I will personally have to maintain workarounds for the next ten years.
Sorry, but you seem to have missed my points regarding these concerns, at least you did not address them I believe. I don't know why you need to (actively) maintain workarounds for APIs external code has no reason to use, especially when the legacy implementation would quite literally be a wrapper function. This could both be a separate driver (Thunk, as in EdkCompatibilityPkg) or integrated (per PCD). In fact, this does need thorough discussion, but my favourite route would be to actually pull some things from the PI specification and make them EDK II implementation details.

Best regards,
Marvin


Thanks,

Michael


Marvin Häuser
 

Hey Andrew,

Thank you a lot. One thing I noticed is that part of the quote I did not see on the list before, so I marked it below.

Best regards,
Marvin

On 08.04.21 00:10, Andrew Fish wrote:
Some of use also sit on the UEFI standards committees so getting changes into the specification is possible with in constraints of what the spec committees find acceptable.

Thanks,

Andrew Fish

On Apr 7, 2021, at 3:02 PM, Andrew Fish via groups.io <http://groups.io> <afish=apple.com@groups.io <mailto:afish=apple.com@groups.io>> wrote:



On Apr 7, 2021, at 2:50 PM, Michael Brown <mcb30@ipxe.org <mailto:mcb30@ipxe.org>> wrote:

On 07/04/2021 22:31, Marvin Häuser wrote:
Sorry, but I do not see why this would be the case. In fact the solution is (temporary) co-existence, as already is the case with InstallProtocolInterface() and InstallMultipleProtocolInterfaces()
InstallMultipleProtocolInterfaces() is not a breaking change: the existence of InstallMultipleProtocolInterfaces() does not require any change to the way that InstallProtocolInterface() is implemented or consumed.

Code written before the invention of InstallMultipleProtocolInterfaces() will still work now, with no modifications required.

the new APIs would be a superset of the old ones, latter can be implemented with former, as also previously done (*2_PROTOCOL instances and shims in e.g. EdkCompatibilityPkg). In some cases, the original protocol interfaces were actually deprecated successfully from the EDK II code base. I would probably offer PCDs to disable the expose of the old APIs, so platforms with little need for backwards-compatibility and more focus on security can tighten the constraints as they see fit. Considering the shimmed interfaces for the old protocols/PPIs/... can be implemented on top of the new public API, and the public API must not change, this code would be practically maintenance-free too in my opinion.
You have to remember that UEFI is not a monolithic codebase with a single maintaining organisation.  Implementing a *2_PROTOCOL and deprecating the original just causes pain for all the code in the world that is maintained outside of the EDK2 repository, since that code now has to support *both* the old and new protocols.

As for your example, I do not believe what is described is "broken".
To avoid distraction from that specific example: have a different example.  The EFI_USB_IO_PROTOCOL is fundamentally broken from the perspective of implementing a network device driver, since there is simply no way to enqueue a receive buffer that will wait for the next available packet.  But this won't get fixed, because it can't get fixed without breaking API compatibility.

(Incidentally, I've observed UEFI software in the wild (from Insyde) that works around these UEFI USB specification flaws by having all of the USB drivers bind to private protocols in addition to EFI_USB_IO_PROTOCOL, resulting in device drivers that point-blank fail to work with a standards-conformant UEFI USB host controller driver.)


Don't get me wrong: I *am* in favour of improving the security of EDK2, and a formally verified loader is potentially useful for that.  But I could only consider it a good idea if it can be done without making breaking API changes for which I know I will personally have to maintain workarounds for the next ten years.
Well it is just software at the end of the day. We could always wrap any Industry Standard API (PPI, Protocol, etc) in a library function and let people chose backward compatibility vs better security. The Library Class would be owned by the edk2 Open Source project so we have more control over it.

The general UEFI (and UEFI PI) is we mostly add new things, and don’t depreciated things to maintain compatibility. So for example you can add a new Protocol to a handle so you have V1 and V2 of a protocol on the same handle. An example of this is SimpleTextIn and SimpleTextInEx. SimpleTextIn was modeled on the LCD of a serial terminal (our server roots) so it did not expose modifier keys, or have an easy way to implement snag keys so that is why SimpleTextInEx got added for the new functional.

Thanks,

Andrew Fish
^ Here; +1


Thanks,

Michael



Michael Brown
 

On 08/04/2021 09:53, Marvin Häuser wrote:
On 07.04.21 23:50, Michael Brown wrote:
InstallMultipleProtocolInterfaces() is not a breaking change: the existence of InstallMultipleProtocolInterfaces() does not require any change to the way that InstallProtocolInterface() is implemented or consumed.

Code written before the invention of InstallMultipleProtocolInterfaces() will still work now, with no modifications required.
The same is true for the *2_PROTOCOL instances, I do not see how you distinct between them. Could you elaborate, please?
The distinction is very straightforward. If you plan to *remove* support for the older protocols, then you by definition place a burden on all externally maintained code to support both protocols. If the older protocol will continue to be supported then no such burden is created.

This is why I am asking you if your proposed changes require *breaking* backwards compatibility. You still haven't answered this key question.

You have to remember that UEFI is not a monolithic codebase with a single maintaining organisation.  Implementing a *2_PROTOCOL and deprecating the original just causes pain for all the code in the world that is maintained outside of the EDK2 repository, since that code now has to support *both* the old and new protocols.
I am aware, but actually it's not far from it nowadays. In contrast to the days of Aptio IV, I believe all big vendors maintain forks of EDK II. I know the fork nature taints the issue, but also see last quote comment.
This is empirically not true. Buy a selection of devices in the wild, and you'll find a huge amount of non-EDK2 code on them.

I would be extremely happy if every vendor just used the EDK2 code: it would make my life a lot easier. But it's not what happens in the real world.

I see that there is no EFI_USB_IO2_PROTOCOL instance to argue by. Yet there are EFI_BLOCK_IO2_PROTOCOL and EFI_LOAD_FILE2_PROTOCOL. Former, in my opinion, close in nature to your your example, and latter close to the nature on what I plan to propose. Sorry, but I do not see how what I suggest has not been done multiple times in the past already.
Please also look at it from an angle of trust. How can I trust the "secure" advertisements of UEFI / EDK II when the specification *dictates* the usage of intrinsically insecure APIs?
The consequence for security-critical situations would be to necessarily abandon UEFI and come up with a new design. In who's interest is this?
Again, we return to the question that you have not yet answered: do your proposed changes require breaking backwards compatibility?

Please do answer this question: if you're *not* proposing to break the platform in a way that would prevent older binaries from working without modification, then we have no disagreement! :)

Don't get me wrong: I *am* in favour of improving the security of EDK2, and a formally verified loader is potentially useful for that. But I could only consider it a good idea if it can be done without making breaking API changes for which I know I will personally have to maintain workarounds for the next ten years.
Sorry, but you seem to have missed my points regarding these concerns, at least you did not address them I believe. I don't know why you need to (actively) maintain workarounds for APIs external code has no reason to use, especially when the legacy implementation would quite literally be a wrapper function.
<same comment as above>

Thanks,

Michael


Michael Brown
 

On 08/04/2021 10:04, Marvin Häuser wrote:
Thank you a lot. One thing I noticed is that part of the quote I did not see on the list before, so I marked it below.
On 08.04.21 00:10, Andrew Fish wrote:
The general UEFI (and UEFI PI) is we mostly add new things, and don’t depreciated things to maintain compatibility. So for example you can add a new Protocol to a handle so you have V1 and V2 of a protocol on the same handle. An example of this is SimpleTextIn and SimpleTextInEx. SimpleTextIn was modeled on the LCD of a serial terminal (our server roots) so it did not expose modifier keys, or have an easy way to implement snag keys so that is why SimpleTextInEx got added for the new functional.
^ Here; +1
The addition of EFI_SIMPLE_TEXT_INPUT_EX_PROTOCOL was really not a good example of how to handle this issue gracefully.

Here is the kind of workaround that external code has to implement: it's a perfect example of how this "add a V2 protocol" approach ends up imposing a permanent maintenance burden on external code:

https://github.com/ipxe/ipxe/commit/a08244ecc

Note that there was absolutely no reason for the specification to require a V2 protocol in order to support Ctrl-<key>, and the EDK2 codebase will indeed do the sensible thing and return the ASCII values for Ctrl-<key> via the original EFI_SIMPLE_TEXT_INPUT_PROTOCOL. It would be amazing if, as you suggested, everyone uses the EDK2 codebase and so all public implementations of EFI_SIMPLE_TEXT_INPUT_PROTOCOL would do this sensible thing.

Unfortunately, this is not the case. Very large numbers of vendors use some other non-EDK2 implementation that does not do the sensible thing. I have no idea why.

It's also worth noting that the addition of EFI_SIMPLE_TEXT_INPUT_EX_PROTOCOL opened up a gaping potential security hole related to pointer lifetimes, as documented in the above-linked commit message.


TL;DR: please assume that creating a V2 protocol has a very significant cost, and needs to come with benefits that outweigh that very significant cost. If you can achieve what you need without breaking backwards compatibility, then that represents a massive increase in value.

Thanks,

Michael


Marvin Häuser
 

Well, I assume this is a misunderstanding. I understood your usage of "workaround" to be supporting both *_PROTOCOL and *2_PROTOCOL instances. Yes, backwards-compatibility will be broken in the sense that the new interface will not be compatible with the old interface. No, backwards-compatibility will not be broken in the sense that the old API is absent or malfunctioning. As I *have* said, I imagine there to be an option (default true) to expose both variants. With default settings, I want the loader to be at the very least mostly plug-'n'-play with existing platform drivers and OS loaders from the real world. "Mostly" can be clarified further once we have a detailed plan on the changes (and responses to e.g. malformed binary issues with iPXE and GNU-EFI).

Best regards,
Marvin

On 08.04.21 11:26, Michael Brown wrote:
On 08/04/2021 09:53, Marvin Häuser wrote:
On 07.04.21 23:50, Michael Brown wrote:
InstallMultipleProtocolInterfaces() is not a breaking change: the existence of InstallMultipleProtocolInterfaces() does not require any change to the way that InstallProtocolInterface() is implemented or consumed.

Code written before the invention of InstallMultipleProtocolInterfaces() will still work now, with no modifications required.
The same is true for the *2_PROTOCOL instances, I do not see how you distinct between them. Could you elaborate, please?
The distinction is very straightforward.  If you plan to *remove* support for the older protocols, then you by definition place a burden on all externally maintained code to support both protocols.  If the older protocol will continue to be supported then no such burden is created.

This is why I am asking you if your proposed changes require *breaking* backwards compatibility.  You still haven't answered this key question.

You have to remember that UEFI is not a monolithic codebase with a single maintaining organisation. Implementing a *2_PROTOCOL and deprecating the original just causes pain for all the code in the world that is maintained outside of the EDK2 repository, since that code now has to support *both* the old and new protocols.
I am aware, but actually it's not far from it nowadays. In contrast to the days of Aptio IV, I believe all big vendors maintain forks of EDK II. I know the fork nature taints the issue, but also see last quote comment.
This is empirically not true.  Buy a selection of devices in the wild, and you'll find a huge amount of non-EDK2 code on them.

I would be extremely happy if every vendor just used the EDK2 code: it would make my life a lot easier.  But it's not what happens in the real world.

I see that there is no EFI_USB_IO2_PROTOCOL instance to argue by. Yet there are EFI_BLOCK_IO2_PROTOCOL and EFI_LOAD_FILE2_PROTOCOL. Former, in my opinion, close in nature to your your example, and latter close to the nature on what I plan to propose. Sorry, but I do not see how what I suggest has not been done multiple times in the past already.

Please also look at it from an angle of trust. How can I trust the "secure" advertisements of UEFI / EDK II when the specification *dictates* the usage of intrinsically insecure APIs?
The consequence for security-critical situations would be to necessarily abandon UEFI and come up with a new design. In who's interest is this?
Again, we return to the question that you have not yet answered: do your proposed changes require breaking backwards compatibility?

Please do answer this question: if you're *not* proposing to break the platform in a way that would prevent older binaries from working without modification, then we have no disagreement! :)

Don't get me wrong: I *am* in favour of improving the security of EDK2, and a formally verified loader is potentially useful for that. But I could only consider it a good idea if it can be done without making breaking API changes for which I know I will personally have to maintain workarounds for the next ten years.
Sorry, but you seem to have missed my points regarding these concerns, at least you did not address them I believe. I don't know why you need to (actively) maintain workarounds for APIs external code has no reason to use, especially when the legacy implementation would quite literally be a wrapper function.
<same comment as above>

Thanks,

Michael


Marvin Häuser
 

Sorry, I accidentally removed an inline comment when sending.

Best regards,
Marvin

On 08.04.21 11:41, Marvin Häuser wrote:
Well, I assume this is a misunderstanding. I understood your usage of "workaround" to be supporting both *_PROTOCOL and *2_PROTOCOL instances. Yes, backwards-compatibility will be broken in the sense that the new interface will not be compatible with the old interface. No, backwards-compatibility will not be broken in the sense that the old API is absent or malfunctioning. As I *have* said, I imagine there to be an option (default true) to expose both variants. With default settings, I want the loader to be at the very least mostly plug-'n'-play with existing platform drivers and OS loaders from the real world. "Mostly" can be clarified further once we have a detailed plan on the changes (and responses to e.g. malformed binary issues with iPXE and GNU-EFI).

Best regards,
Marvin

On 08.04.21 11:26, Michael Brown wrote:
On 08/04/2021 09:53, Marvin Häuser wrote:
On 07.04.21 23:50, Michael Brown wrote:
InstallMultipleProtocolInterfaces() is not a breaking change: the existence of InstallMultipleProtocolInterfaces() does not require any change to the way that InstallProtocolInterface() is implemented or consumed.

Code written before the invention of InstallMultipleProtocolInterfaces() will still work now, with no modifications required.
The same is true for the *2_PROTOCOL instances, I do not see how you distinct between them. Could you elaborate, please?
The distinction is very straightforward.  If you plan to *remove* support for the older protocols, then you by definition place a burden on all externally maintained code to support both protocols.  If the older protocol will continue to be supported then no such burden is created.

This is why I am asking you if your proposed changes require *breaking* backwards compatibility.  You still haven't answered this key question.

You have to remember that UEFI is not a monolithic codebase with a single maintaining organisation. Implementing a *2_PROTOCOL and deprecating the original just causes pain for all the code in the world that is maintained outside of the EDK2 repository, since that code now has to support *both* the old and new protocols.
I am aware, but actually it's not far from it nowadays. In contrast to the days of Aptio IV, I believe all big vendors maintain forks of EDK II. I know the fork nature taints the issue, but also see last quote comment.
This is empirically not true.  Buy a selection of devices in the wild, and you'll find a huge amount of non-EDK2 code on them.
It is not about "how much" is EDK II code, but that it is the core. We are talking about things like the dispatcher, I have not ever seen it modified "lately" (Gigabyte modded AMI CORE_PEI and CORE_DXE with their SIO code in Z77, but you get the idea...). I am very well aware of issues with "user-facing" things such as input.


I would be extremely happy if every vendor just used the EDK2 code: it would make my life a lot easier.  But it's not what happens in the real world.

I see that there is no EFI_USB_IO2_PROTOCOL instance to argue by. Yet there are EFI_BLOCK_IO2_PROTOCOL and EFI_LOAD_FILE2_PROTOCOL. Former, in my opinion, close in nature to your your example, and latter close to the nature on what I plan to propose. Sorry, but I do not see how what I suggest has not been done multiple times in the past already.

Please also look at it from an angle of trust. How can I trust the "secure" advertisements of UEFI / EDK II when the specification *dictates* the usage of intrinsically insecure APIs?
The consequence for security-critical situations would be to necessarily abandon UEFI and come up with a new design. In who's interest is this?
Again, we return to the question that you have not yet answered: do your proposed changes require breaking backwards compatibility?

Please do answer this question: if you're *not* proposing to break the platform in a way that would prevent older binaries from working without modification, then we have no disagreement! :)

Don't get me wrong: I *am* in favour of improving the security of EDK2, and a formally verified loader is potentially useful for that. But I could only consider it a good idea if it can be done without making breaking API changes for which I know I will personally have to maintain workarounds for the next ten years.
Sorry, but you seem to have missed my points regarding these concerns, at least you did not address them I believe. I don't know why you need to (actively) maintain workarounds for APIs external code has no reason to use, especially when the legacy implementation would quite literally be a wrapper function.
<same comment as above>

Thanks,

Michael


Michael Brown
 

On 08/04/2021 10:41, Marvin Häuser wrote:
No, backwards-compatibility will not be broken in the sense that the old API is absent or malfunctioning.
Perfect. :)

As I *have* said, I imagine there to be an option (default true) to expose both variants.
Very much less perfect. The mere existence of such an option immediately reimposes the burden on external code to support both, because it opens up the possibility of running on systems where the option is set to false.

With default settings, I want the loader to be at the very least mostly plug-'n'-play with existing platform drivers and OS loaders from the real world. "Mostly" can be clarified further once we have a detailed plan on the changes (and responses to e.g. malformed binary issues with iPXE and GNU-EFI).
Yes; thank you for https://github.com/ipxe/ipxe/pull/313. It will take some time to review.

As a practical consideration: unless there is a security reason to do otherwise, you should almost certainly relax the constraints on images that your loader will accept, to avoid causing unnecessary end-user disruption. What is the *security* reason behind your alignment requirements (which clearly are not required by any other toolchain, including those used for signing Secure Boot binaries)?

Thanks,

Michael


Marvin Häuser
 

On 08.04.21 11:55, Michael Brown wrote:
On 08/04/2021 10:41, Marvin Häuser wrote:
No, backwards-compatibility will not be broken in the sense that the old API is absent or malfunctioning.
Perfect. :)

As I *have* said, I imagine there to be an option (default true) to expose both variants.
Very much less perfect.  The mere existence of such an option immediately reimposes the burden on external code to support both, because it opens up the possibility of running on systems where the option is set to false.
One more time, I do not know why any non-platform code would call those APIs. Preferably, they would be private implementation details to me. I understand that you are displeased with your maintenance burden in iPXE, and I can assure you, you are not alone. We want to support hotswap with one of our UEFI applications, and I am currently contemplating overriding Uninstall(Multiple)ProtocolInterface(s) to try to ensure security. I hear you, totally. :)

With default settings, I want the loader to be at the very least mostly plug-'n'-play with existing platform drivers and OS loaders from the real world. "Mostly" can be clarified further once we have a detailed plan on the changes (and responses to e.g. malformed binary issues with iPXE and GNU-EFI).
Yes; thank you for https://github.com/ipxe/ipxe/pull/313.  It will take some time to review.

As a practical consideration: unless there is a security reason to do otherwise, you should almost certainly relax the constraints on images that your loader will accept, to avoid causing unnecessary end-user disruption.  What is the *security* reason behind your alignment requirements (which clearly are not required by any other toolchain, including those used for signing Secure Boot binaries)?
Sorry if that was not clear from the PR, I hoped it was. It's the fact that memory permissions can only be enforced page-wise. So, when two sections with different permissions share a page, at the very least this page must be applied with relaxed permissions. I do not like relaxing permissions. :)

There already is a PCD to relax this, and both iPXE and GNU-EFI images load correctly and securely with it. Just the more relaxed loading is, the more awkward cases need to be considered when applying memory permission attributes. Logically, as the original ELF was correctly aligned segment-wise, the case I described above will not really happen. Yet it is now the firmware's burden to check all sections with overlapping pages for their attributes and adjust. As, please do not take this offensively, it is "only" iPXE images and the GNU shim loader affected so far, I hope that in due time all images can be updated (the shim can be used for older releases of any distribution as well!) and the constraints be tightened. Yet, of course, this is up to the EDK II maintainers to decide.

I furthermore hope that, at some point, both iPXE and shim switch to EDK II for PE generation to ensure consistency of the binary generation.

Best regards,
Marvin


Thanks,

Michael




Michael Brown
 

On 08/04/2021 11:13, Marvin Häuser wrote:
Very much less perfect.  The mere existence of such an option immediately reimposes the burden on external code to support both, because it opens up the possibility of running on systems where the option is set to false.
One more time, I do not know why any non-platform code would call those APIs. Preferably, they would be private implementation details to me.
If you are talking about private APIs that are not even exposed at the UEFI specification level (i.e. do not have an EFI_XXX_PROTOCOL name and well-known GUID) then there's no issue.

If they are defined as public APIs (i.e. things that do have an EFI_XXX_PROTOCOL name and well-known GUID) then you must assume that some external code, somewhere, will use them.

Which is the case?

As a practical consideration: unless there is a security reason to do otherwise, you should almost certainly relax the constraints on images that your loader will accept, to avoid causing unnecessary end-user disruption.  What is the *security* reason behind your alignment requirements (which clearly are not required by any other toolchain, including those used for signing Secure Boot binaries)?
Sorry if that was not clear from the PR, I hoped it was. It's the fact that memory permissions can only be enforced page-wise.
Perfect; thank you. So: the security requirement is that memory permissions must change only at page boundaries.

I furthermore hope that, at some point, both iPXE and shim switch to EDK II for PE generation to ensure consistency of the binary generation.
There is zero chance of ever pulling the EDK2 build system into iPXE. It's too large, too painful to use, and doesn't support the full range of target platforms required (UEFI, BIOS, and Linux userspace).

If EDK2 publishes a tool for converting ELF to PE, and that tool becomes generally available in Linux distros, then I'd be happy to drop elf2efi.c and switch to the EDK2 tool about five years from now once it's safe to assume its existence on any viable build platform.

This may not be quite the answer you were hoping for, but it's the only practical one.

Thanks,

Michael


Laszlo Ersek
 

On 04/06/21 12:06, Marvin Häuser wrote:
Good day Nate,

Comments are inline.

Best regards,
Marvin

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 would call it "semi-automated", a great deal of intermediate goals
(preconditions, postconditions, invariants, assertions, ...) were
required to show all interesting properties. But yes, the actual proof
steps are automated by common SMT solvers. It was done using the
AstraVer Toolset and ACSL, latter basically a language to express logic
statements with C-like syntax.

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.
I'm glad to hear that. :)

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?
Please don't get me wrong, but I would be surprised if the UEFI
specification changes I'd like to discuss alone would be completed
within 10 weeks, let alone implementation throughout the codebase. While
I think the plain amount of code may be a bit less than say a
MinPlatform port, the changes are much deeper and require much more
caution to avoid regressions (e.g. by invalidating undocumented
assertions). This sadly is not a matter of just replacing the underlying
library implementation or "plug-in and play" at all. It furthermore
affects many parts of the stack, the core dispatchers used for all
platforms, image emulation (EBC), UEFI userland emulation (EmuPkg), and
so on. I was rather worried the scope is too broad time-wise, but it can
be narrowed/widened as you see fit really. This is one of *the* core
components used on millions of device, and many package maintainers need
to review and validate the changes, this must really be done right the
first try. :)

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.
I believed that was part of the workload, yes, but even without it I
think there is plenty to do.

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.
Thank you, I will gladly explain anything unclear. Just try to not give
Laszlo too many flashbacks. :)
I haven't commented yet in this thread, as I thought my stance on this
undertaking was (or should be) obvious.

I very much welcome a replacement for the PE/COFF parser (as I consider
its security issues unfixable in an incremental manner). From my reading
of Marvin's and Vitaly's paper (draft), they have my full trust, and I'm
ready to put their upcoming code to use in ArmVirtPkg and OvmfPkg with
minimal actual code review. If fixing the pervasive security problems
around this area cannot avoid spiraling out to other core code in edk2,
such as dispatchers, and even to the PI / UEFI specs, so be it.

Regarding GSoC itself: as I stated elsewhere previously, I support
edk2's participation in GSoC, while at the same time I'm not
volunteering for mentorship at all. I'm uncertain if GSoC is the best
framework for upstreaming such a large undertaking, but if it can help,
we should use it as much as possible.

Thanks
Laszlo







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







Andrew Fish
 

At a minimum it would be nice if we had a tool that would point out the security faults with a given PE/COFF file layout.
On Apr 8, 2021, at 4:16 AM, Laszlo Ersek <lersek@redhat.com> wrote:

On 04/06/21 12:06, Marvin Häuser wrote:
Good day Nate,

Comments are inline.

Best regards,
Marvin

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 would call it "semi-automated", a great deal of intermediate goals
(preconditions, postconditions, invariants, assertions, ...) were
required to show all interesting properties. But yes, the actual proof
steps are automated by common SMT solvers. It was done using the
AstraVer Toolset and ACSL, latter basically a language to express logic
statements with C-like syntax.

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.
I'm glad to hear that. :)

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?
Please don't get me wrong, but I would be surprised if the UEFI
specification changes I'd like to discuss alone would be completed
within 10 weeks, let alone implementation throughout the codebase. While
I think the plain amount of code may be a bit less than say a
MinPlatform port, the changes are much deeper and require much more
caution to avoid regressions (e.g. by invalidating undocumented
assertions). This sadly is not a matter of just replacing the underlying
library implementation or "plug-in and play" at all. It furthermore
affects many parts of the stack, the core dispatchers used for all
platforms, image emulation (EBC), UEFI userland emulation (EmuPkg), and
so on. I was rather worried the scope is too broad time-wise, but it can
be narrowed/widened as you see fit really. This is one of *the* core
components used on millions of device, and many package maintainers need
to review and validate the changes, this must really be done right the
first try. :)

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.
I believed that was part of the workload, yes, but even without it I
think there is plenty to do.

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.
Thank you, I will gladly explain anything unclear. Just try to not give
Laszlo too many flashbacks. :)
I haven't commented yet in this thread, as I thought my stance on this
undertaking was (or should be) obvious.

I very much welcome a replacement for the PE/COFF parser (as I consider
its security issues unfixable in an incremental manner). From my reading
of Marvin's and Vitaly's paper (draft), they have my full trust, and I'm
ready to put their upcoming code to use in ArmVirtPkg and OvmfPkg with
minimal actual code review. If fixing the pervasive security problems
around this area cannot avoid spiraling out to other core code in edk2,
such as dispatchers, and even to the PI / UEFI specs, so be it.

Regarding GSoC itself: as I stated elsewhere previously, I support
edk2's participation in GSoC, while at the same time I'm not
volunteering for mentorship at all. I'm uncertain if GSoC is the best
framework for upstreaming such a large undertaking, but if it can help,
we should use it as much as possible.

Thanks
Laszlo







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











Marvin Häuser
 

We use the loader code in userspace anyway for fuzzing and such. I also want to build a database of all sorts of UEFI binaries some time before the merge to confirm they are all accepted (Windows / macOS / Linux bootloaders, tools like memtest, drivers like iPXE). As part of that, I'm sure we can have a userspace tool that uses the code to emit parsing information.

But as the EDK II build system is very... not so userspace friendly, I will not promise it will be very nice. :)

Best regards,
Marvin

On 08.04.21 16:13, Andrew (EFI) Fish wrote:
At a minimum it would be nice if we had a tool that would point out the security faults with a given PE/COFF file layout.

Sent from my iPhone

On Apr 8, 2021, at 4:16 AM, Laszlo Ersek <lersek@redhat.com> wrote:

On 04/06/21 12:06, Marvin Häuser wrote:
Good day Nate,

Comments are inline.

Best regards,
Marvin

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 would call it "semi-automated", a great deal of intermediate goals
(preconditions, postconditions, invariants, assertions, ...) were
required to show all interesting properties. But yes, the actual proof
steps are automated by common SMT solvers. It was done using the
AstraVer Toolset and ACSL, latter basically a language to express logic
statements with C-like syntax.

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.
I'm glad to hear that. :)

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?
Please don't get me wrong, but I would be surprised if the UEFI
specification changes I'd like to discuss alone would be completed
within 10 weeks, let alone implementation throughout the codebase. While
I think the plain amount of code may be a bit less than say a
MinPlatform port, the changes are much deeper and require much more
caution to avoid regressions (e.g. by invalidating undocumented
assertions). This sadly is not a matter of just replacing the underlying
library implementation or "plug-in and play" at all. It furthermore
affects many parts of the stack, the core dispatchers used for all
platforms, image emulation (EBC), UEFI userland emulation (EmuPkg), and
so on. I was rather worried the scope is too broad time-wise, but it can
be narrowed/widened as you see fit really. This is one of *the* core
components used on millions of device, and many package maintainers need
to review and validate the changes, this must really be done right the
first try. :)

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.
I believed that was part of the workload, yes, but even without it I
think there is plenty to do.

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.
Thank you, I will gladly explain anything unclear. Just try to not give
Laszlo too many flashbacks. :)
I haven't commented yet in this thread, as I thought my stance on this
undertaking was (or should be) obvious.

I very much welcome a replacement for the PE/COFF parser (as I consider
its security issues unfixable in an incremental manner). From my reading
of Marvin's and Vitaly's paper (draft), they have my full trust, and I'm
ready to put their upcoming code to use in ArmVirtPkg and OvmfPkg with
minimal actual code review. If fixing the pervasive security problems
around this area cannot avoid spiraling out to other core code in edk2,
such as dispatchers, and even to the PI / UEFI specs, so be it.

Regarding GSoC itself: as I stated elsewhere previously, I support
edk2's participation in GSoC, while at the same time I'm not
volunteering for mentorship at all. I'm uncertain if GSoC is the best
framework for upstreaming such a large undertaking, but if it can help,
we should use it as much as possible.

Thanks
Laszlo





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