<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"> <head> <meta http-equiv="Content-Type" content="text/html; charset=Windows-1252"> <meta name="Generator" content="Microsoft Word 15 (filtered medium)"> <style></style> </head> <body lang="EN-US" link="blue" vlink="#954F72" style="word-wrap:break-word"> <div class="WordSection1"> You’ve got my vote! This sounds amazing! <o:p> </o:p> - Bret <o:p></o:p> <o:p> </o:p> <div style="mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in"> From: <a href="mailto:mhaeuser=posteo.de@groups.io">Marvin Häuser via groups.io</a> Sent: Tuesday, April 6, 2021 3:10 AM To: <a href="mailto:devel@edk2.groups.io">devel@edk2.groups.io</a>; <a href="mailto:nathaniel.l.desimone@intel.com"> Desimone, Nathaniel L</a>; <a href="mailto:lersek@redhat.com">Laszlo Ersek</a>; <a href="mailto:afish@apple.com"> Andrew Fish</a>; <a href="mailto:michael.d.kinney@intel.com">Kinney, Michael D</a> Subject: [EXTERNAL] Re: [edk2-devel] [GSoC proposal] Secure Image Loader </div> <o:p> </o:p> 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] <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fmhaeuser%2FISPRASOpen-SecurePE&data=04%7C01%7Cbret.barkelew%40microsoft.com%7C85d20ecd77ca4c34d8ca08d8f8e41eb5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637533006571825642%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=oWA5TZaj9Tpm6%2FtDGOYLj%2FmFIrUdKh943uMl6Z5f8YM%3D&reserved=0"> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fmhaeuser%2FISPRASOpen-SecurePE&data=04%7C01%7Cbret.barkelew%40microsoft.com%7C85d20ecd77ca4c34d8ca08d8f8e41eb5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637533006571825642%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=oWA5TZaj9Tpm6%2FtDGOYLj%2FmFIrUdKh943uMl6Z5f8YM%3D&reserved=0</a> >> [2] <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Farxiv.org%2Fpdf%2F2012.05471.pdf&data=04%7C01%7Cbret.barkelew%40microsoft.com%7C85d20ecd77ca4c34d8ca08d8f8e41eb5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637533006571825642%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=zge5VG18wDyu6IexsugW4o243PPUTh2UywXWhJTR0Wo%3D&reserved=0"> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Farxiv.org%2Fpdf%2F2012.05471.pdf&data=04%7C01%7Cbret.barkelew%40microsoft.com%7C85d20ecd77ca4c34d8ca08d8f8e41eb5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637533006571825642%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=zge5VG18wDyu6IexsugW4o243PPUTh2UywXWhJTR0Wo%3D&reserved=0</a> >> >> >> >> > > > > > <o:p></o:p> <o:p> </o:p> </div> </body> </html> <div width="1" style="color:white;clear:both">_._,_._,_</div> <hr> Groups.io Links: You receive all messages sent to this group. <a target="_blank" href="https://edk2.groups.io/g/devel/message/73731">View/Reply Online (#73731)</a> | | <a target="_blank" href="https://groups.io/mt/81893826/1813853">Mute This Topic</a> | <a href="https://edk2.groups.io/g/devel/post">New Topic</a> <a href="https://edk2.groups.io/g/devel/editsub/1813853">Your Subscription</a> | <a href="mailto:devel+owner@edk2.groups.io">Contact Group Owner</a> | <a href="https://edk2.groups.io/g/devel/unsub">Unsubscribe</a> [edk2-devel-archive@redhat.com] <div width="1" style="color:white;clear:both">_._,_._,_</div>