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 <ler...@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 <ler...@redhat.com>; Andrew Fish >>>> <af...@apple.com>; Kinney, Michael D <michael.d.kin...@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 >>>> >>>> >>>> >>>> >>> >>> >>> >>> >>> >> > > > > > >
-=-=-=-=-=-=-=-=-=-=-=- Groups.io Links: You receive all messages sent to this group. View/Reply Online (#73855): https://edk2.groups.io/g/devel/message/73855 Mute This Topic: https://groups.io/mt/81853302/21656 Group Owner: devel+ow...@edk2.groups.io Unsubscribe: https://edk2.groups.io/g/devel/unsub [arch...@mail-archive.com] -=-=-=-=-=-=-=-=-=-=-=-
