[GSoC proposal] Secure Image Loader

[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

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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
> 
> 
> 
> 

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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
>>
>>
>>
>>
>
>
> 
>
>

Re: [EXTERNAL] Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Bret Barkelew]

[-- Attachment #1: Type: text/plain, Size: 8273 bytes --]

You’ve got my vote! This sounds amazing!

- Bret

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

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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fmhaeuser%2FISPRASOpen-SecurePE&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C85d20ecd77ca4c34d8ca08d8f8e41eb5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637533006571825642%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=oWA5TZaj9Tpm6%2FtDGOYLj%2FmFIrUdKh943uMl6Z5f8YM%3D&amp;reserved=0
>> [2] https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Farxiv.org%2Fpdf%2F2012.05471.pdf&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C85d20ecd77ca4c34d8ca08d8f8e41eb5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637533006571825642%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=zge5VG18wDyu6IexsugW4o243PPUTh2UywXWhJTR0Wo%3D&amp;reserved=0
>>
>>
>>
>>
>
>
>
>
>







[-- Attachment #2: Type: text/html, Size: 12189 bytes --]

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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
>
>
> 
>
>

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Andrew Fish]

[-- Attachment #1: Type: text/plain, Size: 4091 bytes --]

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=apple.com@groups.io> wrote:
> 
> 
> 
>> 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
> 
> 
> 
> 


[-- Attachment #2: Type: text/html, Size: 12601 bytes --]

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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
>>
>>
>>
>> 
>

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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
>

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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
>
>
> 
>
>

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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
>>>
>>>
>>>
>>>
>>
>>
>> 
>>
>>
> 

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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
>>>> 
>>>> 
>>>> 
>>>> 
>>> 
>>> 
>>> 
>>> 
>>> 
>> 
> 
> 
> 
> 
> 
> 

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[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
>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>>>
>>>>
>>>>
>>
>>
>> 
>>
>>

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Andrew Fish]

[-- Attachment #1: Type: text/plain, Size: 19761 bytes --]



> On Apr 8, 2021, at 9:06 AM, Marvin Häuser <mhaeuser@posteo.de> wrote:
> 
> 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. :)
> 

Marvin,

The BaseTools can easily build C command line tools that are cross platform?

Actually GenFw [1] already does a lot of PE/COFF magic, so it should be relatively easy to add a -I, —info, and dump out an overview of a PE/COFF image, and make comments on things that are not secure. It would also probably be useful to dump out information about the Debug Directory entries, His sections, etc. for general debug.

[1] https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/GenFw
/Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>. edksetup.sh
Loading previous configuration from /Volumes/Case/edk2-github/Conf/BuildEnv.sh
WORKSPACE: /Volumes/Case/edk2-github
EDK_TOOLS_PATH: /Volumes/Case/edk2-github/BaseTools
CONF_PATH: /Volumes/Case/edk2-github/Conf
/Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>GenFw -h
GenFw Version 0.2 Developer Build based on Revision: Unknown 

Usage: GenFw [options] <input_file>

Copyright (c) 2007 - 2018, Intel Corporation. All rights reserved.

Options:
  -o FileName, --outputfile FileName
                        File will be created to store the output content.
  -e EFI_FILETYPE, --efiImage EFI_FILETYPE
                        Create Efi Image. EFI_FILETYPE is one of BASE,SMM_CORE,
                        PEI_CORE, PEIM, DXE_CORE, DXE_DRIVER, UEFI_APPLICATION,
                        SEC, DXE_SAL_DRIVER, UEFI_DRIVER, DXE_RUNTIME_DRIVER,
                        DXE_SMM_DRIVER, SECURITY_CORE, COMBINED_PEIM_DRIVER,
                        MM_STANDALONE, MM_CORE_STANDALONE,
                        PIC_PEIM, RELOCATABLE_PEIM, BS_DRIVER, RT_DRIVER,
                        APPLICATION, SAL_RT_DRIVER to support all module types
                        It can only be used together with --keepexceptiontable,
                        --keepzeropending, --keepoptionalheader, -r, -o option.
                        It is a action option. If it is combined with other action options,
                        the later input action option will override the previous one.
  -c, --acpi            Create Acpi table.
                        It can't be combined with other action options
                        except for -o, -r option. It is a action option.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  -t, --terse           Create Te Image.
                        It can only be used together with --keepexceptiontable,
                        --keepzeropending, --keepoptionalheader, -r, -o option.
                        It is a action option. If it is combined with other action options,
                        the later input action option will override the previous one.
  -u, --dump            Dump TeImage Header.
                        It can't be combined with other action options
                        except for -o, -r option. It is a action option.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  -z, --zero            Zero the Debug Data Fields in the PE input image file.
                        It also zeros the time stamp fields.
                        This option can be used to compare the binary efi image.
                        It can't be combined with other action options
                        except for -o, -r option. It is a action option.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  -b, --exe2bin         Convert the input EXE to the output BIN file.
                        It can't be combined with other action options
                        except for -o, -r option. It is a action option.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  -l, --stripped        Strip off the relocation info from PE or TE image.
                        It can't be combined with other action options
                        except for -o, -r option. It is a action option.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  -s timedate, --stamp timedate
                        timedate format is "yyyy-mm-dd 00:00:00". if timedata 
                        is set to NOW, current system time is used. The support
                        date scope is 1970-01-01 00+timezone:00:00
                        ~ 2038-01-19 03+timezone:14:07
                        The scope is adjusted according to the different zones.
                        It can't be combined with other action options
                        except for -o, -r option. It is a action option.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  -m, --mcifile         Convert input microcode txt file to microcode bin file.
                        It can't be combined with other action options
                        except for -o option. It is a action option.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  -j, --join            Combine multi microcode bin files to one file.
                        It can be specified with -a, -p, -o option.
                        No other options can be combined with it.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  -a NUM, --align NUM   NUM is one HEX or DEC format alignment value.
                        This option is only used together with -j option.
  -p NUM, --pad NUM     NUM is one HEX or DEC format padding value.
                        This option is only used together with -j option.
  --keepexceptiontable  Don't clear exception table.
                        This option can be used together with -e or -t.
                        It doesn't work for other options.
  --keepoptionalheader  Don't zero PE/COFF optional header fields.
                        This option can be used together with -e or -t.
                        It doesn't work for other options.
  --keepzeropending     Don't strip zero pending of .reloc.
                        This option can be used together with -e or -t.
                        It doesn't work for other options.
  -r, --replace         Overwrite the input file with the output content.
                        If more input files are specified,
                        the last input file will be as the output file.
  -g HiiPackageListGuid, --hiiguid HiiPackageListGuid
                        Guid is used to specify hii package list guid.
                        Its format is xxxxxxxx-xxxx-xxxx-xxxx-xxxxxxxxxxxx
                        If not specified, the first Form FormSet guid is used.
  --hiipackage          Combine all input binary hii packages into 
                        a single package list as the text resource data(RC).
                        It can't be combined with other action options
                        except for -o option. It is a action option.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  --hiibinpackage       Combine all input binary hii packages into 
                        a single package list as the binary resource section.
                        It can't be combined with other action options
                        except for -o option. It is a action option.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  --rc FlieName         Append a Hii resource section to the
                        last PE/COFF section. The FileName is the resource section to append
                        If FileName does not exist this operation is skipped. This feature is
                        only intended for toolchains, like XCODE, that don't suport $(RC).
                        This option can only be combined with -e
  --rebase NewAddress   Rebase image to new base address. New address 
                        is also set to the first none code section header.
                        It can't be combined with other action options
                        except for -o or -r option. It is a action option.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  --address NewAddress  Set new address into the first none code 
                        section header of the input image.
                        It can't be combined with other action options
                        except for -o or -r option. It is a action option.
                        If it is combined with other action options, the later
                        input action option will override the previous one.
  -v, --verbose         Turn on verbose output with informational messages.
  -q, --quiet           Disable all messages except key message and fatal error
  -d, --debug level     Enable debug messages, at input debug level.
  --version             Show program's version number and exit
  -h, --help            Show this help message and exit

Thanks,

Andrew Fish

> 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
>>>>>> 
>>>>>> 
>>>>>> 
>>>>>> 
>>>>> 
>>>>> 
>>>>> 
>>>>> 
>>> 
>>> 
>>> 
>>> 
> 
> 
> 
> 


[-- Attachment #2: Type: text/html, Size: 61516 bytes --]

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Marvin Häuser]

On 08.04.21 18:44, Andrew Fish via groups.io wrote:
>
>
>> On Apr 8, 2021, at 9:06 AM, Marvin Häuser <mhaeuser@posteo.de 
>> <mailto:mhaeuser@posteo.de>> wrote:
>>
>> 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. :)
>>
>
> Marvin,
>
> The BaseTools can easily build C command line tools that are cross 
> platform?
>
> Actually GenFw [1] already does a lot of PE/COFF magic, so it should 
> be relatively easy to add a -I, —info, and dump out an overview of a 
> PE/COFF image, and make comments on things that are not secure. It 
> would also probably be useful to dump out information about the Debug 
> Directory entries, His sections, etc. for general debug.

I did not look at the code much, but I do know that BaseTools duplicates 
the PE/COFF code from MdePkg. Whether it was changed or not I cannot tell.

Best regards,
Marvin

>
> [1] 
> https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/GenFw 
> <https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/GenFw>
> /Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>. edksetup.sh
> Loading previous configuration from 
> /Volumes/Case/edk2-github/Conf/BuildEnv.sh
> WORKSPACE: /Volumes/Case/edk2-github
> EDK_TOOLS_PATH: /Volumes/Case/edk2-github/BaseTools
> CONF_PATH: /Volumes/Case/edk2-github/Conf
> /Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>GenFw -h
> GenFw Version 0.2 Developer Build based on Revision: Unknown
>
> Usage: GenFw [options] <input_file>
>
> Copyright (c) 2007 - 2018, Intel Corporation. All rights reserved.
>
> Options:
>   -o FileName, --outputfile FileName
>                         File will be created to store the output content.
>   -e EFI_FILETYPE, --efiImage EFI_FILETYPE
>                         Create Efi Image. EFI_FILETYPE is one of 
> BASE,SMM_CORE,
>                         PEI_CORE, PEIM, DXE_CORE, DXE_DRIVER, 
> UEFI_APPLICATION,
>                         SEC, DXE_SAL_DRIVER, UEFI_DRIVER, 
> DXE_RUNTIME_DRIVER,
>                         DXE_SMM_DRIVER, SECURITY_CORE, 
> COMBINED_PEIM_DRIVER,
>                         MM_STANDALONE, MM_CORE_STANDALONE,
>                         PIC_PEIM, RELOCATABLE_PEIM, BS_DRIVER, RT_DRIVER,
>                         APPLICATION, SAL_RT_DRIVER to support all 
> module types
>                         It can only be used together with 
> --keepexceptiontable,
>                         --keepzeropending, --keepoptionalheader, -r, 
> -o option.
>                         It is a action option. If it is combined with 
> other action options,
>                         the later input action option will override 
> the previous one.
>   -c, --acpi            Create Acpi table.
>                         It can't be combined with other action options
>                         except for -o, -r option. It is a action option.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   -t, --terse           Create Te Image.
>                         It can only be used together with 
> --keepexceptiontable,
>                         --keepzeropending, --keepoptionalheader, -r, 
> -o option.
>                         It is a action option. If it is combined with 
> other action options,
>                         the later input action option will override 
> the previous one.
>   -u, --dump            Dump TeImage Header.
>                         It can't be combined with other action options
>                         except for -o, -r option. It is a action option.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   -z, --zero            Zero the Debug Data Fields in the PE input 
> image file.
>                         It also zeros the time stamp fields.
>                         This option can be used to compare the binary 
> efi image.
>                         It can't be combined with other action options
>                         except for -o, -r option. It is a action option.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   -b, --exe2bin         Convert the input EXE to the output BIN file.
>                         It can't be combined with other action options
>                         except for -o, -r option. It is a action option.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   -l, --stripped        Strip off the relocation info from PE or TE image.
>                         It can't be combined with other action options
>                         except for -o, -r option. It is a action option.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   -s timedate, --stamp timedate
>                         timedate format is "yyyy-mm-dd 00:00:00". if 
> timedata
>                         is set to NOW, current system time is used. 
> The support
>                         date scope is 1970-01-01 00+timezone:00:00
>                         ~ 2038-01-19 03+timezone:14:07
>                         The scope is adjusted according to the 
> different zones.
>                         It can't be combined with other action options
>                         except for -o, -r option. It is a action option.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   -m, --mcifile         Convert input microcode txt file to microcode 
> bin file.
>                         It can't be combined with other action options
>                         except for -o option. It is a action option.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   -j, --join            Combine multi microcode bin files to one file.
>                         It can be specified with -a, -p, -o option.
>                         No other options can be combined with it.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   -a NUM, --align NUM   NUM is one HEX or DEC format alignment value.
>                         This option is only used together with -j option.
>   -p NUM, --pad NUM     NUM is one HEX or DEC format padding value.
>                         This option is only used together with -j option.
>   --keepexceptiontable  Don't clear exception table.
>                         This option can be used together with -e or -t.
>                         It doesn't work for other options.
>   --keepoptionalheader  Don't zero PE/COFF optional header fields.
>                         This option can be used together with -e or -t.
>                         It doesn't work for other options.
>   --keepzeropending     Don't strip zero pending of .reloc.
>                         This option can be used together with -e or -t.
>                         It doesn't work for other options.
>   -r, --replace         Overwrite the input file with the output content.
>                         If more input files are specified,
>                         the last input file will be as the output file.
>   -g HiiPackageListGuid, --hiiguid HiiPackageListGuid
>                         Guid is used to specify hii package list guid.
>                         Its format is xxxxxxxx-xxxx-xxxx-xxxx-xxxxxxxxxxxx
>                         If not specified, the first Form FormSet guid 
> is used.
>   --hiipackage          Combine all input binary hii packages into
>                         a single package list as the text resource 
> data(RC).
>                         It can't be combined with other action options
>                         except for -o option. It is a action option.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   --hiibinpackage       Combine all input binary hii packages into
>                         a single package list as the binary resource 
> section.
>                         It can't be combined with other action options
>                         except for -o option. It is a action option.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   --rc FlieName         Append a Hii resource section to the
>                         last PE/COFF section. The FileName is the 
> resource section to append
>                         If FileName does not exist this operation is 
> skipped. This feature is
>                         only intended for toolchains, like XCODE, that 
> don't suport $(RC).
>                         This option can only be combined with -e
>   --rebase NewAddress   Rebase image to new base address. New address
>                         is also set to the first none code section header.
>                         It can't be combined with other action options
>                         except for -o or -r option. It is a action option.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   --address NewAddress  Set new address into the first none code
>                         section header of the input image.
>                         It can't be combined with other action options
>                         except for -o or -r option. It is a action option.
>                         If it is combined with other action options, 
> the later
>                         input action option will override the previous 
> one.
>   -v, --verbose         Turn on verbose output with informational 
> messages.
>   -q, --quiet           Disable all messages except key message and 
> fatal error
>   -d, --debug level     Enable debug messages, at input debug level.
>   --version             Show program's version number and exit
>   -h, --help            Show this help message and exit
>
> Thanks,
>
> Andrew Fish
>
>> 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.
>>>
>>>
>>>
>>>> On Apr 8, 2021, at 4:16 AM, Laszlo Ersek <lersek@redhat.com 
>>>> <mailto: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 <mailto:devel@edk2.groups.io> 
>>>>>>> <devel@edk2.groups.io <mailto:devel@edk2.groups.io>> On Behalf 
>>>>>>> Of Marvin
>>>>>>> Häuser
>>>>>>> Sent: Sunday, April 4, 2021 4:02 PM
>>>>>>> To: devel@edk2.groups.io <mailto:devel@edk2.groups.io>; Laszlo 
>>>>>>> Ersek <lersek@redhat.com <mailto:lersek@redhat.com>>; Andrew Fish
>>>>>>> <afish@apple.com <mailto:afish@apple.com>>; Kinney, Michael D 
>>>>>>> <michael.d.kinney@intel.com <mailto: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 
>>>>>>> <https://github.com/mhaeuser/ISPRASOpen-SecurePE>
>>>>>>> [2] https://arxiv.org/pdf/2012.05471.pdf 
>>>>>>> <https://arxiv.org/pdf/2012.05471.pdf>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>
>>>>
>>>>
>>>>
>>
>>
>>
>
> 

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Andrew Fish]

> On Apr 8, 2021, at 10:02 AM, Marvin Häuser <mhaeuser@posteo.de> wrote:
> 
> On 08.04.21 18:44, Andrew Fish via groups.io wrote:
>> 
>> 
>>> On Apr 8, 2021, at 9:06 AM, Marvin Häuser <mhaeuser@posteo.de <mailto:mhaeuser@posteo.de>> wrote:
>>> 
>>> 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. :)
>>> 
>> 
>> Marvin,
>> 
>> The BaseTools can easily build C command line tools that are cross platform?
>> 
>> Actually GenFw [1] already does a lot of PE/COFF magic, so it should be relatively easy to add a -I, —info, and dump out an overview of a PE/COFF image, and make comments on things that are not secure. It would also probably be useful to dump out information about the Debug Directory entries, His sections, etc. for general debug.
> 
> I did not look at the code much, but I do know that BaseTools duplicates the PE/COFF code from MdePkg. Whether it was changed or not I cannot tell.
> 

GenFw does the ELF to PE/COFF conversion, zeroing out Debug Directory Entries etc. so it should be correct. It is not like the PE/COFF spec is a moving target. 

Thanks,

Andrew Fish

> Best regards,
> Marvin
> 
>> 
>> [1] https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/GenFw <https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/GenFw>
>> /Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>. edksetup.sh
>> Loading previous configuration from /Volumes/Case/edk2-github/Conf/BuildEnv.sh
>> WORKSPACE: /Volumes/Case/edk2-github
>> EDK_TOOLS_PATH: /Volumes/Case/edk2-github/BaseTools
>> CONF_PATH: /Volumes/Case/edk2-github/Conf
>> /Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>GenFw -h
>> GenFw Version 0.2 Developer Build based on Revision: Unknown
>> 
>> Usage: GenFw [options] <input_file>
>> 
>> Copyright (c) 2007 - 2018, Intel Corporation. All rights reserved.
>> 
>> Options:
>>   -o FileName, --outputfile FileName
>>                         File will be created to store the output content.
>>   -e EFI_FILETYPE, --efiImage EFI_FILETYPE
>>                         Create Efi Image. EFI_FILETYPE is one of BASE,SMM_CORE,
>>                         PEI_CORE, PEIM, DXE_CORE, DXE_DRIVER, UEFI_APPLICATION,
>>                         SEC, DXE_SAL_DRIVER, UEFI_DRIVER, DXE_RUNTIME_DRIVER,
>>                         DXE_SMM_DRIVER, SECURITY_CORE, COMBINED_PEIM_DRIVER,
>>                         MM_STANDALONE, MM_CORE_STANDALONE,
>>                         PIC_PEIM, RELOCATABLE_PEIM, BS_DRIVER, RT_DRIVER,
>>                         APPLICATION, SAL_RT_DRIVER to support all module types
>>                         It can only be used together with --keepexceptiontable,
>>                         --keepzeropending, --keepoptionalheader, -r, -o option.
>>                         It is a action option. If it is combined with other action options,
>>                         the later input action option will override the previous one.
>>   -c, --acpi            Create Acpi table.
>>                         It can't be combined with other action options
>>                         except for -o, -r option. It is a action option.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   -t, --terse           Create Te Image.
>>                         It can only be used together with --keepexceptiontable,
>>                         --keepzeropending, --keepoptionalheader, -r, -o option.
>>                         It is a action option. If it is combined with other action options,
>>                         the later input action option will override the previous one.
>>   -u, --dump            Dump TeImage Header.
>>                         It can't be combined with other action options
>>                         except for -o, -r option. It is a action option.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   -z, --zero            Zero the Debug Data Fields in the PE input image file.
>>                         It also zeros the time stamp fields.
>>                         This option can be used to compare the binary efi image.
>>                         It can't be combined with other action options
>>                         except for -o, -r option. It is a action option.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   -b, --exe2bin         Convert the input EXE to the output BIN file.
>>                         It can't be combined with other action options
>>                         except for -o, -r option. It is a action option.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   -l, --stripped        Strip off the relocation info from PE or TE image.
>>                         It can't be combined with other action options
>>                         except for -o, -r option. It is a action option.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   -s timedate, --stamp timedate
>>                         timedate format is "yyyy-mm-dd 00:00:00". if timedata
>>                         is set to NOW, current system time is used. The support
>>                         date scope is 1970-01-01 00+timezone:00:00
>>                         ~ 2038-01-19 03+timezone:14:07
>>                         The scope is adjusted according to the different zones.
>>                         It can't be combined with other action options
>>                         except for -o, -r option. It is a action option.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   -m, --mcifile         Convert input microcode txt file to microcode bin file.
>>                         It can't be combined with other action options
>>                         except for -o option. It is a action option.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   -j, --join            Combine multi microcode bin files to one file.
>>                         It can be specified with -a, -p, -o option.
>>                         No other options can be combined with it.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   -a NUM, --align NUM   NUM is one HEX or DEC format alignment value.
>>                         This option is only used together with -j option.
>>   -p NUM, --pad NUM     NUM is one HEX or DEC format padding value.
>>                         This option is only used together with -j option.
>>   --keepexceptiontable  Don't clear exception table.
>>                         This option can be used together with -e or -t.
>>                         It doesn't work for other options.
>>   --keepoptionalheader  Don't zero PE/COFF optional header fields.
>>                         This option can be used together with -e or -t.
>>                         It doesn't work for other options.
>>   --keepzeropending     Don't strip zero pending of .reloc.
>>                         This option can be used together with -e or -t.
>>                         It doesn't work for other options.
>>   -r, --replace         Overwrite the input file with the output content.
>>                         If more input files are specified,
>>                         the last input file will be as the output file.
>>   -g HiiPackageListGuid, --hiiguid HiiPackageListGuid
>>                         Guid is used to specify hii package list guid.
>>                         Its format is xxxxxxxx-xxxx-xxxx-xxxx-xxxxxxxxxxxx
>>                         If not specified, the first Form FormSet guid is used.
>>   --hiipackage          Combine all input binary hii packages into
>>                         a single package list as the text resource data(RC).
>>                         It can't be combined with other action options
>>                         except for -o option. It is a action option.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   --hiibinpackage       Combine all input binary hii packages into
>>                         a single package list as the binary resource section.
>>                         It can't be combined with other action options
>>                         except for -o option. It is a action option.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   --rc FlieName         Append a Hii resource section to the
>>                         last PE/COFF section. The FileName is the resource section to append
>>                         If FileName does not exist this operation is skipped. This feature is
>>                         only intended for toolchains, like XCODE, that don't suport $(RC).
>>                         This option can only be combined with -e
>>   --rebase NewAddress   Rebase image to new base address. New address
>>                         is also set to the first none code section header.
>>                         It can't be combined with other action options
>>                         except for -o or -r option. It is a action option.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   --address NewAddress  Set new address into the first none code
>>                         section header of the input image.
>>                         It can't be combined with other action options
>>                         except for -o or -r option. It is a action option.
>>                         If it is combined with other action options, the later
>>                         input action option will override the previous one.
>>   -v, --verbose         Turn on verbose output with informational messages.
>>   -q, --quiet           Disable all messages except key message and fatal error
>>   -d, --debug level     Enable debug messages, at input debug level.
>>   --version             Show program's version number and exit
>>   -h, --help            Show this help message and exit
>> 
>> Thanks,
>> 
>> Andrew Fish
>> 
>>> 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.
>>>> 
>>>> 
>>>> 
>>>>> On Apr 8, 2021, at 4:16 AM, Laszlo Ersek <lersek@redhat.com <mailto: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 <mailto:devel@edk2.groups.io> <devel@edk2.groups.io <mailto:devel@edk2.groups.io>> On Behalf Of Marvin
>>>>>>>> Häuser
>>>>>>>> Sent: Sunday, April 4, 2021 4:02 PM
>>>>>>>> To: devel@edk2.groups.io <mailto:devel@edk2.groups.io>; Laszlo Ersek <lersek@redhat.com <mailto:lersek@redhat.com>>; Andrew Fish
>>>>>>>> <afish@apple.com <mailto:afish@apple.com>>; Kinney, Michael D <michael.d.kinney@intel.com <mailto: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 <https://github.com/mhaeuser/ISPRASOpen-SecurePE>
>>>>>>>> [2] https://arxiv.org/pdf/2012.05471.pdf <https://arxiv.org/pdf/2012.05471.pdf>
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>> 
>>>>> 
>>>>> 
>>>>> 
>>> 
>>> 
>>> 
>> 
>> 
> 

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Marvin Häuser]

08.04.2021 19:39:16 Andrew Fish <afish@apple.com>:

>
>
>> On Apr 8, 2021, at 10:02 AM, Marvin Häuser <mhaeuser@posteo.de> wrote:
>>
>> On 08.04.21 18:44, Andrew Fish via groups.io wrote:
>>>
>>>
>>>> On Apr 8, 2021, at 9:06 AM, Marvin Häuser <mhaeuser@posteo.de <mailto:mhaeuser@posteo.de>> wrote:
>>>>
>>>> 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. :)
>>>>
>>>
>>> Marvin,
>>>
>>> The BaseTools can easily build C command line tools that are cross platform?
>>>
>>> Actually GenFw [1] already does a lot of PE/COFF magic, so it should be relatively easy to add a -I, —info, and dump out an overview of a PE/COFF image, and make comments on things that are not secure. It would also probably be useful to dump out information about the Debug Directory entries, His sections, etc. for general debug.
>>
>> I did not look at the code much, but I do know that BaseTools duplicates the PE/COFF code from MdePkg. Whether it was changed or not I cannot tell.
>>
>
> GenFw does the ELF to PE/COFF conversion, zeroing out Debug Directory Entries etc. so it should be correct. It is not like the PE/COFF spec is a moving target.


PE is not a moving target, but EDK II is. The fact that even old and proven code sometimes needs maintanance is evidental from the proposal and its so far positive feedback. I'm not ready to duplicate code, I'd rather take the utilities out of the current scope and discuss ways to consume MdePkg libraries later. In fact, I want to reduce code duplication as a "free benefit" from the changes, especially image hashing.

I know it takes time, but I think it will be worth it. We have been debugging and fuzztesting our EDK II packages in userland for a while, and found it to be a great help. I hope you will agree. :)

Best regards,
Marvin

>
> Thanks,
>
> Andrew Fish
>
>> Best regards,
>> Marvin
>>
>>>
>>> [1] https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/GenFw <https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/GenFw>
>>> /Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>. edksetup.sh
>>> Loading previous configuration from /Volumes/Case/edk2-github/Conf/BuildEnv.sh
>>> WORKSPACE: /Volumes/Case/edk2-github
>>> EDK_TOOLS_PATH: /Volumes/Case/edk2-github/BaseTools
>>> CONF_PATH: /Volumes/Case/edk2-github/Conf
>>> /Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>GenFw -h
>>> GenFw Version 0.2 Developer Build based on Revision: Unknown
>>>
>>> Usage: GenFw [options] <input_file>
>>>
>>> Copyright (c) 2007 - 2018, Intel Corporation. All rights reserved.
>>>
>>> Options:
>>>   -o FileName, --outputfile FileName
>>>                         File will be created to store the output content.
>>>   -e EFI_FILETYPE, --efiImage EFI_FILETYPE
>>>                         Create Efi Image. EFI_FILETYPE is one of BASE,SMM_CORE,
>>>                         PEI_CORE, PEIM, DXE_CORE, DXE_DRIVER, UEFI_APPLICATION,
>>>                         SEC, DXE_SAL_DRIVER, UEFI_DRIVER, DXE_RUNTIME_DRIVER,
>>>                         DXE_SMM_DRIVER, SECURITY_CORE, COMBINED_PEIM_DRIVER,
>>>                         MM_STANDALONE, MM_CORE_STANDALONE,
>>>                         PIC_PEIM, RELOCATABLE_PEIM, BS_DRIVER, RT_DRIVER,
>>>                         APPLICATION, SAL_RT_DRIVER to support all module types
>>>                         It can only be used together with --keepexceptiontable,
>>>                         --keepzeropending, --keepoptionalheader, -r, -o option.
>>>                         It is a action option. If it is combined with other action options,
>>>                         the later input action option will override the previous one.
>>>   -c, --acpi            Create Acpi table.
>>>                         It can't be combined with other action options
>>>                         except for -o, -r option. It is a action option.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   -t, --terse           Create Te Image.
>>>                         It can only be used together with --keepexceptiontable,
>>>                         --keepzeropending, --keepoptionalheader, -r, -o option.
>>>                         It is a action option. If it is combined with other action options,
>>>                         the later input action option will override the previous one.
>>>   -u, --dump            Dump TeImage Header.
>>>                         It can't be combined with other action options
>>>                         except for -o, -r option. It is a action option.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   -z, --zero            Zero the Debug Data Fields in the PE input image file.
>>>                         It also zeros the time stamp fields.
>>>                         This option can be used to compare the binary efi image.
>>>                         It can't be combined with other action options
>>>                         except for -o, -r option. It is a action option.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   -b, --exe2bin         Convert the input EXE to the output BIN file.
>>>                         It can't be combined with other action options
>>>                         except for -o, -r option. It is a action option.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   -l, --stripped        Strip off the relocation info from PE or TE image.
>>>                         It can't be combined with other action options
>>>                         except for -o, -r option. It is a action option.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   -s timedate, --stamp timedate
>>>                         timedate format is "yyyy-mm-dd 00:00:00". if timedata
>>>                         is set to NOW, current system time is used. The support
>>>                         date scope is 1970-01-01 00+timezone:00:00
>>>                         ~ 2038-01-19 03+timezone:14:07
>>>                         The scope is adjusted according to the different zones.
>>>                         It can't be combined with other action options
>>>                         except for -o, -r option. It is a action option.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   -m, --mcifile         Convert input microcode txt file to microcode bin file.
>>>                         It can't be combined with other action options
>>>                         except for -o option. It is a action option.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   -j, --join            Combine multi microcode bin files to one file.
>>>                         It can be specified with -a, -p, -o option.
>>>                         No other options can be combined with it.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   -a NUM, --align NUM   NUM is one HEX or DEC format alignment value.
>>>                         This option is only used together with -j option.
>>>   -p NUM, --pad NUM     NUM is one HEX or DEC format padding value.
>>>                         This option is only used together with -j option.
>>>   --keepexceptiontable  Don't clear exception table.
>>>                         This option can be used together with -e or -t.
>>>                         It doesn't work for other options.
>>>   --keepoptionalheader  Don't zero PE/COFF optional header fields.
>>>                         This option can be used together with -e or -t.
>>>                         It doesn't work for other options.
>>>   --keepzeropending     Don't strip zero pending of .reloc.
>>>                         This option can be used together with -e or -t.
>>>                         It doesn't work for other options.
>>>   -r, --replace         Overwrite the input file with the output content.
>>>                         If more input files are specified,
>>>                         the last input file will be as the output file.
>>>   -g HiiPackageListGuid, --hiiguid HiiPackageListGuid
>>>                         Guid is used to specify hii package list guid.
>>>                         Its format is xxxxxxxx-xxxx-xxxx-xxxx-xxxxxxxxxxxx
>>>                         If not specified, the first Form FormSet guid is used.
>>>   --hiipackage          Combine all input binary hii packages into
>>>                         a single package list as the text resource data(RC).
>>>                         It can't be combined with other action options
>>>                         except for -o option. It is a action option.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   --hiibinpackage       Combine all input binary hii packages into
>>>                         a single package list as the binary resource section.
>>>                         It can't be combined with other action options
>>>                         except for -o option. It is a action option.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   --rc FlieName         Append a Hii resource section to the
>>>                         last PE/COFF section. The FileName is the resource section to append
>>>                         If FileName does not exist this operation is skipped. This feature is
>>>                         only intended for toolchains, like XCODE, that don't suport $(RC).
>>>                         This option can only be combined with -e
>>>   --rebase NewAddress   Rebase image to new base address. New address
>>>                         is also set to the first none code section header.
>>>                         It can't be combined with other action options
>>>                         except for -o or -r option. It is a action option.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   --address NewAddress  Set new address into the first none code
>>>                         section header of the input image.
>>>                         It can't be combined with other action options
>>>                         except for -o or -r option. It is a action option.
>>>                         If it is combined with other action options, the later
>>>                         input action option will override the previous one.
>>>   -v, --verbose         Turn on verbose output with informational messages.
>>>   -q, --quiet           Disable all messages except key message and fatal error
>>>   -d, --debug level     Enable debug messages, at input debug level.
>>>   --version             Show program's version number and exit
>>>   -h, --help            Show this help message and exit
>>>
>>> Thanks,
>>>
>>> Andrew Fish
>>>
>>>> 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.
>>>>>
>>>>>
>>>>>
>>>>>> …
>>>>
>>>>
>>>>
>>>
>>> 
>>

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Andrew Fish]

[-- Attachment #1: Type: text/plain, Size: 13593 bytes --]



> On Apr 8, 2021, at 2:07 PM, Marvin Häuser <mhaeuser@posteo.de> wrote:
> 
> 
> 08.04.2021 19:39:16 Andrew Fish <afish@apple.com <mailto:afish@apple.com>>:
> 
>> 
>> 
>>> On Apr 8, 2021, at 10:02 AM, Marvin Häuser <mhaeuser@posteo.de> wrote:
>>> 
>>> On 08.04.21 18:44, Andrew Fish via groups.io wrote:
>>>> 
>>>> 
>>>>> On Apr 8, 2021, at 9:06 AM, Marvin Häuser <mhaeuser@posteo.de <mailto:mhaeuser@posteo.de>> wrote:
>>>>> 
>>>>> 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. :)
>>>>> 
>>>> 
>>>> Marvin,
>>>> 
>>>> The BaseTools can easily build C command line tools that are cross platform?
>>>> 
>>>> Actually GenFw [1] already does a lot of PE/COFF magic, so it should be relatively easy to add a -I, —info, and dump out an overview of a PE/COFF image, and make comments on things that are not secure. It would also probably be useful to dump out information about the Debug Directory entries, His sections, etc. for general debug.
>>> 
>>> I did not look at the code much, but I do know that BaseTools duplicates the PE/COFF code from MdePkg. Whether it was changed or not I cannot tell.
>>> 
>> 
>> GenFw does the ELF to PE/COFF conversion, zeroing out Debug Directory Entries etc. so it should be correct. It is not like the PE/COFF spec is a moving target.
> 
> 
> PE is not a moving target, but EDK II is. The fact that even old and proven code sometimes needs maintanance is evidental from the proposal and its so far positive feedback. I'm not ready to duplicate code, I'd rather take the utilities out of the current scope and discuss ways to consume MdePkg libraries later. In fact, I want to reduce code duplication as a "free benefit" from the changes, especially image hashing.
> 

Marvin,

I was thinking more about tooling to introspect PE/COFF images. 

Trying to consolidate the BaseTools to use the common edk2 libraries would be doable, but I agree that is a separate project. The inspection tool feature could be a separate project too. 

> I know it takes time, but I think it will be worth it. We have been debugging and fuzztesting our EDK II packages in userland for a while, and found it to be a great help. I hope you will agree. :)
> 

Yea I’ve build emulators before that are just native OS C applications and they pull in the edk2 libs, not the BaseTools libs and it makes things like fuzzing much easier. Have a project to have only one validated PE/COFF lib seems very reasonable, I guess a lot of us are too trusting of our build servers. 

Thanks,

Andrew Fish

> Best regards,
> Marvin
> 
>> 
>> Thanks,
>> 
>> Andrew Fish
>> 
>>> Best regards,
>>> Marvin
>>> 
>>>> 
>>>> [1] https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/GenFw <https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/GenFw>
>>>> /Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>. edksetup.sh
>>>> Loading previous configuration from /Volumes/Case/edk2-github/Conf/BuildEnv.sh
>>>> WORKSPACE: /Volumes/Case/edk2-github
>>>> EDK_TOOLS_PATH: /Volumes/Case/edk2-github/BaseTools
>>>> CONF_PATH: /Volumes/Case/edk2-github/Conf
>>>> /Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>GenFw -h
>>>> GenFw Version 0.2 Developer Build based on Revision: Unknown
>>>> 
>>>> Usage: GenFw [options] <input_file>
>>>> 
>>>> Copyright (c) 2007 - 2018, Intel Corporation. All rights reserved.
>>>> 
>>>> Options:
>>>>   -o FileName, --outputfile FileName
>>>>                         File will be created to store the output content.
>>>>   -e EFI_FILETYPE, --efiImage EFI_FILETYPE
>>>>                         Create Efi Image. EFI_FILETYPE is one of BASE,SMM_CORE,
>>>>                         PEI_CORE, PEIM, DXE_CORE, DXE_DRIVER, UEFI_APPLICATION,
>>>>                         SEC, DXE_SAL_DRIVER, UEFI_DRIVER, DXE_RUNTIME_DRIVER,
>>>>                         DXE_SMM_DRIVER, SECURITY_CORE, COMBINED_PEIM_DRIVER,
>>>>                         MM_STANDALONE, MM_CORE_STANDALONE,
>>>>                         PIC_PEIM, RELOCATABLE_PEIM, BS_DRIVER, RT_DRIVER,
>>>>                         APPLICATION, SAL_RT_DRIVER to support all module types
>>>>                         It can only be used together with --keepexceptiontable,
>>>>                         --keepzeropending, --keepoptionalheader, -r, -o option.
>>>>                         It is a action option. If it is combined with other action options,
>>>>                         the later input action option will override the previous one.
>>>>   -c, --acpi            Create Acpi table.
>>>>                         It can't be combined with other action options
>>>>                         except for -o, -r option. It is a action option.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   -t, --terse           Create Te Image.
>>>>                         It can only be used together with --keepexceptiontable,
>>>>                         --keepzeropending, --keepoptionalheader, -r, -o option.
>>>>                         It is a action option. If it is combined with other action options,
>>>>                         the later input action option will override the previous one.
>>>>   -u, --dump            Dump TeImage Header.
>>>>                         It can't be combined with other action options
>>>>                         except for -o, -r option. It is a action option.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   -z, --zero            Zero the Debug Data Fields in the PE input image file.
>>>>                         It also zeros the time stamp fields.
>>>>                         This option can be used to compare the binary efi image.
>>>>                         It can't be combined with other action options
>>>>                         except for -o, -r option. It is a action option.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   -b, --exe2bin         Convert the input EXE to the output BIN file.
>>>>                         It can't be combined with other action options
>>>>                         except for -o, -r option. It is a action option.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   -l, --stripped        Strip off the relocation info from PE or TE image.
>>>>                         It can't be combined with other action options
>>>>                         except for -o, -r option. It is a action option.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   -s timedate, --stamp timedate
>>>>                         timedate format is "yyyy-mm-dd 00:00:00". if timedata
>>>>                         is set to NOW, current system time is used. The support
>>>>                         date scope is 1970-01-01 00+timezone:00:00
>>>>                         ~ 2038-01-19 03+timezone:14:07
>>>>                         The scope is adjusted according to the different zones.
>>>>                         It can't be combined with other action options
>>>>                         except for -o, -r option. It is a action option.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   -m, --mcifile         Convert input microcode txt file to microcode bin file.
>>>>                         It can't be combined with other action options
>>>>                         except for -o option. It is a action option.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   -j, --join            Combine multi microcode bin files to one file.
>>>>                         It can be specified with -a, -p, -o option.
>>>>                         No other options can be combined with it.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   -a NUM, --align NUM   NUM is one HEX or DEC format alignment value.
>>>>                         This option is only used together with -j option.
>>>>   -p NUM, --pad NUM     NUM is one HEX or DEC format padding value.
>>>>                         This option is only used together with -j option.
>>>>   --keepexceptiontable  Don't clear exception table.
>>>>                         This option can be used together with -e or -t.
>>>>                         It doesn't work for other options.
>>>>   --keepoptionalheader  Don't zero PE/COFF optional header fields.
>>>>                         This option can be used together with -e or -t.
>>>>                         It doesn't work for other options.
>>>>   --keepzeropending     Don't strip zero pending of .reloc.
>>>>                         This option can be used together with -e or -t.
>>>>                         It doesn't work for other options.
>>>>   -r, --replace         Overwrite the input file with the output content.
>>>>                         If more input files are specified,
>>>>                         the last input file will be as the output file.
>>>>   -g HiiPackageListGuid, --hiiguid HiiPackageListGuid
>>>>                         Guid is used to specify hii package list guid.
>>>>                         Its format is xxxxxxxx-xxxx-xxxx-xxxx-xxxxxxxxxxxx
>>>>                         If not specified, the first Form FormSet guid is used.
>>>>   --hiipackage          Combine all input binary hii packages into
>>>>                         a single package list as the text resource data(RC).
>>>>                         It can't be combined with other action options
>>>>                         except for -o option. It is a action option.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   --hiibinpackage       Combine all input binary hii packages into
>>>>                         a single package list as the binary resource section.
>>>>                         It can't be combined with other action options
>>>>                         except for -o option. It is a action option.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   --rc FlieName         Append a Hii resource section to the
>>>>                         last PE/COFF section. The FileName is the resource section to append
>>>>                         If FileName does not exist this operation is skipped. This feature is
>>>>                         only intended for toolchains, like XCODE, that don't suport $(RC).
>>>>                         This option can only be combined with -e
>>>>   --rebase NewAddress   Rebase image to new base address. New address
>>>>                         is also set to the first none code section header.
>>>>                         It can't be combined with other action options
>>>>                         except for -o or -r option. It is a action option.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   --address NewAddress  Set new address into the first none code
>>>>                         section header of the input image.
>>>>                         It can't be combined with other action options
>>>>                         except for -o or -r option. It is a action option.
>>>>                         If it is combined with other action options, the later
>>>>                         input action option will override the previous one.
>>>>   -v, --verbose         Turn on verbose output with informational messages.
>>>>   -q, --quiet           Disable all messages except key message and fatal error
>>>>   -d, --debug level     Enable debug messages, at input debug level.
>>>>   --version             Show program's version number and exit
>>>>   -h, --help            Show this help message and exit
>>>> 
>>>> Thanks,
>>>> 
>>>> Andrew Fish
>>>> 
>>>>> 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.
>>>>>> 
>>>>>> 
>>>>>> 
>>>>>>> …
>>>>> 
>>>>> 
>>>>> 
>>>> 
>>>> 
>>> 
> 
> 
> 


[-- Attachment #2: Type: text/html, Size: 42113 bytes --]

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Michael Brown]

On 08/04/2021 22:07, Marvin Häuser wrote:
> PE is not a moving target, but EDK II is. The fact that even old and proven code sometimes needs maintanance is evidental from the proposal and its so far positive feedback. I'm not ready to duplicate code, I'd rather take the utilities out of the current scope and discuss ways to consume MdePkg libraries later. In fact, I want to reduce code duplication as a "free benefit" from the changes, especially image hashing.
> 
> I know it takes time, but I think it will be worth it. We have been debugging and fuzztesting our EDK II packages in userland for a while, and found it to be a great help. I hope you will agree. :)

In case any of it happens to be helpful:

   https://github.com/ipxe/efikit

is a proof-of-concept build of portions of EDK2 (specifically, several 
of the MdePkg libraries) as cross-platform libraries that can be linked 
against by standard Linux, Windows, or Mac userspace applications.

It's quite satisfying to be able to use

   #include <Library/DevicePathLib.h>
   ...
   size_t len = UefiDevicePathLibGetDevicePathSize ( path );

from otherwise perfectly normal-looking userspace C code.

It uses GNU autotools, so just download 
https://github.com/ipxe/efikit/releases/download/v0.3/efikit-0.3.tar.gz 
and run the standard:

   ./configure
   make

Totally undocumented (for now), but if you're curious then good places 
to dig in are probably

https://github.com/ipxe/efikit/blob/master/src/Makefile.am#L186-L237
https://github.com/ipxe/efikit/blob/master/src/libefidevpath.c#L187-L215

Michael

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Marvin Häuser]

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
>>
>>
>>
>>
>
>
> 
>
>

Re: [EXTERNAL] Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Bret Barkelew]

[-- Attachment #1: Type: text/plain, Size: 16553 bytes --]

As always, we volunteer the UEFI Talkbox Discord for conversations of this nature. 😉

https://discord.gg/cuqjER3Juw

- Bret

From: Marvin Häuser via groups.io<mailto:mhaeuser=posteo.de@groups.io>
Sent: Monday, April 12, 2021 10:24 AM
To: devel@edk2.groups.io<mailto:devel@edk2.groups.io>; Desimone, Nathaniel L<mailto:nathaniel.l.desimone@intel.com>; Laszlo Ersek<mailto:lersek@redhat.com>; Andrew Fish<mailto:afish@apple.com>; Kinney, Michael D<mailto:michael.d.kinney@intel.com>
Subject: [EXTERNAL] 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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3315&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446516854%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=xkAIi7yRQfRtw3pKELUzpb1oo9EN4kyroCdadjEzPLQ%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3316&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446516854%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=cFAacXfo69cDMpxSggXjnVpoRqYdIj21QYg%2Ffo5jp9Y%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3317&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446516854%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=Ssf4h8yn3zee1IaK5%2BwI5WwvOvUW4gAtjikil0pS3Fw%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3318&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446516854%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=2KKVA6qqHIP2skLSLXo56av1%2FS9pL1MMJbt%2FPI9BBPM%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3319&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446516854%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=ERrMCAigrcP0pkORLcNzFRPw74YxmHlZFohsvmpeXpE%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3320&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=4yKviWdeKCojn7cVTsHE5xQbflvX7TdnML07D67NdYc%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3321&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=KSt0vUz1VioMOEfcagubQjh0YjVIljpyxJHiKWVklXc%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3322&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=FFVnp5Np6xQHhKt8dpKGPlU9dV5BEMQBQ8qb1Sd6g5Q%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3323&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=3PRwMITWczBZ5ioQC6MP%2BnLbywvU2hTMlEQA%2F5u9%2FlI%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3324&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=werYWbqTbEQfVc7C1ujWYNZlDbG%2BEykDppDi5TL8fg0%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3326&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=F9f%2FGvEvqBPpTWewflQ2OGlTSpE5CGl5yA%2B705X%2BV78%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3327&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=eTbDLsN3UymQHBZqyzBkyBDHerHF1RbigQwy6r50PaE%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3328&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=DSHRyWvAoxTFN2xaLbonm1yh2eOAvf9GvLezG2kOQfs%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3329&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=DEvvfOQsVQiQIbHL919g0QKNU%2Fr2%2FXi64zfESo2EOn8%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3330&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=lIcbok5gDUg5kcmqUQvmQLKIkGHQhg05MPn07ayQAXk%3D&amp;reserved=0
https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3331&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=b6mWPdfFR53ZXKkUWiWrwWGyRFllWe7gfpQz0zRy%2F9w%3D&amp;reserved=0

[2] https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fipxe%2Fipxe%2Fpull%2F313&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=Kyz14TkQ1YUexm9Xm7eSQEXSaDCioZk9xSdmEZ17Qfs%3D&amp;reserved=0

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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fmhaeuser%2FISPRASOpen-SecurePE&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=BlF8x5mleNL5mFSYGBmKT8aVIt1Jl0pjUlzTI%2Fu49AM%3D&amp;reserved=0
>> [2] https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Farxiv.org%2Fpdf%2F2012.05471.pdf&amp;data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446526809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&amp;sdata=flmu2cOW7z1A2c%2FpM3Hc1N3tvVLlx44kMKDw8U%2BAmC8%3D&amp;reserved=0
>>
>>
>>
>>
>
>
>
>
>







[-- Attachment #2: Type: text/html, Size: 28770 bytes --]

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Michael D Kinney]

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
> >>
> >>
> >>
> >>
> >
> >
> > 
> >
> >

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Nate DeSimone]

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
> >>
> >>
> >>
> >>
> >
> >
> > 
> >
> >

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Marvin Häuser]

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
>>>> 
>>>> 
>>>> 
>>>> 
>>> 
>>> 
>>> 
>>> 
>>> 

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Andrew Fish]

[-- Attachment #1: Type: text/plain, Size: 13227 bytes --]

Marvin,

School of hard knocks… Bug rates have gone up around the world as the security experts show up with security fixes. Most commonly the bugs are around functionality and not security. While a brick is very secure (since the customer can’t use it), customers generally don’t like their products turning into bricks. Thus we tend to be conservative on larger changes. 

There is a large ecosystem surrounding edk2, and you need to factor in things like products that are in sustaining for large number of years (these products may be more conservative) and people may want to be conservative. The edi2  does not generally deprecate things right away. We generally add new extra things and slowly deprecate over time. 

It might be useful to review the LibraryClass (API) changes and try and understand the issues in the current design. 

Thanks,

Andrew Fish

> 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 <mailto: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
>>>>> 
>>>>> 
>>>>> 
>>>>> 
>>>> 
>>>> 
>>>> 


[-- Attachment #2: Type: text/html, Size: 25196 bytes --]

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Nate DeSimone]

Hi Marvin,

What Mike and I were thinking is having a FixedAtBuildPcd which chooses whether to use the new loader or the old loader at compile time. We were also thinking the same thing of shimming the old loader into the new interface. I completely agree with you that it is unlikely the new loader is "broken"... it is more likely that broken images exist out in the world somewhere and that we won't know that they are broken until someone tries to build their system's firmware with the new loader included. Once the broken images are found, it can take some time to get them fixed. A lot of times they come from outside vendors and the source code for those binaries is not readily available. Because of that, there may be a need to fallback to the old loader in the interim period while a fixed binary is being acquired.

This could become very difficult for OpROMs on PCIe add-in cards since they are stored on a separate device rom and most of the time are completely non-upgradable. We should think about how we can handle the case where we find an old graphics or network card built in 2014 that has a UEFI OpROM that contains a broken PE/COFF header which cannot be fixed.

Thanks,
Nate

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

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
>>>> 
>>>> 
>>>> 
>>>> 
>>> 
>>> 
>>> 
>>> 
>>> 

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Michael D Kinney]

Hi Nate,

Yes.  A FixedAtBuild PCD or a FeatureFlag PCD is one way.  However, that approach does add some risk to the existing PE/COFF loader functionality.

My suggestion was to add a new library instance as a peer to the existing library instance.

I believe Marvin is also suggesting some changes to the PE/COFF Library Class APIs, which would be more challenging to support old and news.  

I agree with Andrew that the proposed changes to the PE/COFF Library Class need to be reviewed to see if there is a path to support old and new.

Mike

> -----Original Message-----
> From: Desimone, Nathaniel L <nathaniel.l.desimone@intel.com>
> Sent: Tuesday, April 13, 2021 11:05 AM
> To: Marvin Häuser <mhaeuser@posteo.de>
> Cc: Kinney, Michael D <michael.d.kinney@intel.com>; devel@edk2.groups.io; Laszlo Ersek <lersek@redhat.com>; Andrew Fish
> <afish@apple.com>
> Subject: RE: [edk2-devel] [GSoC proposal] Secure Image Loader
> 
> Hi Marvin,
> 
> What Mike and I were thinking is having a FixedAtBuildPcd which chooses whether to use the new loader or the old loader at
> compile time. We were also thinking the same thing of shimming the old loader into the new interface. I completely agree
> with you that it is unlikely the new loader is "broken"... it is more likely that broken images exist out in the world
> somewhere and that we won't know that they are broken until someone tries to build their system's firmware with the new
> loader included. Once the broken images are found, it can take some time to get them fixed. A lot of times they come from
> outside vendors and the source code for those binaries is not readily available. Because of that, there may be a need to
> fallback to the old loader in the interim period while a fixed binary is being acquired.
> 
> This could become very difficult for OpROMs on PCIe add-in cards since they are stored on a separate device rom and most
> of the time are completely non-upgradable. We should think about how we can handle the case where we find an old graphics
> or network card built in 2014 that has a UEFI OpROM that contains a broken PE/COFF header which cannot be fixed.
> 
> Thanks,
> Nate
> 
> -----Original Message-----
> From: Marvin Häuser <mhaeuser@posteo.de>
> Sent: Tuesday, April 13, 2021 12:32 AM
> To: Desimone, Nathaniel L <nathaniel.l.desimone@intel.com>
> Cc: Kinney, Michael D <michael.d.kinney@intel.com>; devel@edk2.groups.io; Laszlo Ersek <lersek@redhat.com>; Andrew Fish
> <afish@apple.com>
> Subject: Re: [edk2-devel] [GSoC proposal] Secure Image Loader
> 
> 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
> >>>>
> >>>>
> >>>>
> >>>>
> >>>
> >>>
> >>> 
> >>>
> >>>

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Andrew Fish]

> On Apr 13, 2021, at 11:04 AM, Desimone, Nathaniel L <nathaniel.l.desimone@intel.com> wrote:
> 
> Hi Marvin,
> 
> What Mike and I were thinking is having a FixedAtBuildPcd which chooses whether to use the new loader or the old loader at compile time. We were also thinking the same thing of shimming the old loader into the new interface. I completely agree with you that it is unlikely the new loader is "broken"... it is more likely that broken images exist out in the world somewhere and that we won't know that they are broken until someone tries to build their system's firmware with the new loader included. Once the broken images are found, it can take some time to get them fixed. A lot of times they come from outside vendors and the source code for those binaries is not readily available. Because of that, there may be a need to fallback to the old loader in the interim period while a fixed binary is being acquired.
> 
> This could become very difficult for OpROMs on PCIe add-in cards since they are stored on a separate device rom and most of the time are completely non-upgradable. We should think about how we can handle the case where we find an old graphics or network card built in 2014 that has a UEFI OpROM that contains a broken PE/COFF header which cannot be fixed.
> 

Don’t forget Thunderbolt dongles, docks, and devices. 

Thanks,

Andrew Fish

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

Re: [edk2-devel] [GSoC proposal] Secure Image Loader

[Marvin Häuser]

Good day everyone,

Sorry for the late reply, but somehow my mail filter is malfunctioning. 
I have two folders for edk2-devel, one where all mails with me in To/CC 
go, and one for the rest. And somehow, multiple times in this 
conversation already, mails end up in the latter. While I try to figure 
out why this happens, if you ever feel like I take too long to answer, 
please ping me outside the list so I get a mail in my main inbox. Thanks 
and sorry!

I'm still not sure whether I misunderstand your intention, or whether I 
am not properly communicating the design. This loader does *not* expect 
all images to be pitch-perfect in all situations. In fact, while I want 
to add more, it already has a couple of FixedAtBuild PCDs to ignore 
certain kinds of malformation. One example is a heavily malformed macOS 
bootloader binary from I think a decade ago, which is completely 
misaligned. For this we have what is currently called "tolerant load" (I 
will refactor and rename PCDs to make more sense once their 
functionality is stabilised), which ignores section alignment entirely. 
The code is also written in a tolerant fashion to my best knowledge, 
e.g. zero'ing the end of a section (i.e. when size of data in file < 
size of loaded section) always extends to the start of the next section, 
or the end of the buffer, if no such exist. So even when a binary is 
malformed, it still ensures the safest possible behaviour.

So, when encountering more broken binaries in the future (for which I 
already have mentioned the EFI image database I am planning to build, 
but obviously would gladly take any outside help I can getting it tested 
on as much real-world hardware as possible), I expect those PCDs to be 
tuned to accept them, and not to revert to known-broken code. The 
tightest of settings possible do not obviously increase security, but 
they are there to not take any chances. A good candidate for this is 
project Amaranth at ISP RAS. Real-world consumer platforms unlikely will 
benefit from some of the constraints, and they can be relaxed, possibly 
forever, just fine. As I have stated in the proposal, the defaults I 
will propose will aim for maximum compatibility, excluding obvious 
security threats. Of course I am trying to fix images like iPXE at the 
moment, but so long as there exist important external images that are 
likely to not be updated (iPXE I believe one could expect to just 
update, GPU OROMs not so much), I will also try my best to provide PCDs 
to have them be allowed. Honestly, the only constraint I can think of we 
do not allow relaxation of is virtual section order, which I never in my 
life have seen violated anywhere. By this I mean that sections are 
ordered with VirtualAddress in ascending order. Things like 
out-of-binary offsets or overlapping sections cannot be tolerated, sorry 
(not that I have seen them, but our loader is a little stricter than the 
old one with this).

In case I actually do misunderstand, the changes to the API are minimal 
(e.g. adding size parameters where there were none), so shimming the old 
loader into it will not be a huge issue. I also added a couple of 
functions to move all PE operations that are currently outside (sections 
for permissions, cert directory for SB, ...) inside, so that would 
merely be a copy+paste from other places of the code. Yet, I *strongly* 
would not like to implement this as the code is very flawed, and not 
just regarding security. If you believe(d) you needed the old loader to 
accept malformed images, I hope I could explain why I believe otherwise.

Thank your for your feedback and considerations!

Best regards,
Marvin

On 13.04.21 20:14, Andrew Fish wrote:
>
>> On Apr 13, 2021, at 11:04 AM, Desimone, Nathaniel L <nathaniel.l.desimone@intel.com> wrote:
>>
>> Hi Marvin,
>>
>> What Mike and I were thinking is having a FixedAtBuildPcd which chooses whether to use the new loader or the old loader at compile time. We were also thinking the same thing of shimming the old loader into the new interface. I completely agree with you that it is unlikely the new loader is "broken"... it is more likely that broken images exist out in the world somewhere and that we won't know that they are broken until someone tries to build their system's firmware with the new loader included. Once the broken images are found, it can take some time to get them fixed. A lot of times they come from outside vendors and the source code for those binaries is not readily available. Because of that, there may be a need to fallback to the old loader in the interim period while a fixed binary is being acquired.
>>
>> This could become very difficult for OpROMs on PCIe add-in cards since they are stored on a separate device rom and most of the time are completely non-upgradable. We should think about how we can handle the case where we find an old graphics or network card built in 2014 that has a UEFI OpROM that contains a broken PE/COFF header which cannot be fixed.
>>
> Don’t forget Thunderbolt dongles, docks, and devices.
>
> Thanks,
>
> Andrew Fish
>
>> Thanks,
>> Nate
>>
>> -----Original Message-----
>> From: Marvin Häuser <mhaeuser@posteo.de>
>> Sent: Tuesday, April 13, 2021 12:32 AM
>> To: Desimone, Nathaniel L <nathaniel.l.desimone@intel.com>
>> Cc: Kinney, Michael D <michael.d.kinney@intel.com>; devel@edk2.groups.io; Laszlo Ersek <lersek@redhat.com>; Andrew Fish <afish@apple.com>
>> Subject: Re: [edk2-devel] [GSoC proposal] Secure Image Loader
>>
>> 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
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>
>>>>> 
>>>>>
>>>>>