Re: [EXTERNAL] Re: [edk2-devel] [GSoC proposal] Secure Image Loader
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...@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.desim...@intel.com>; Laszlo Ersek<mailto:ler...@redhat.com>; Andrew Fish<mailto:af...@apple.com>; Kinney, Michael D<mailto:michael.d.kin...@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%3D3315data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446516854%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000sdata=xkAIi7yRQfRtw3pKELUzpb1oo9EN4kyroCdadjEzPLQ%3Dreserved=0 https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3316data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446516854%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000sdata=cFAacXfo69cDMpxSggXjnVpoRqYdIj21QYg%2Ffo5jp9Y%3Dreserved=0 https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3317data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446516854%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000sdata=Ssf4h8yn3zee1IaK5%2BwI5WwvOvUW4gAtjikil0pS3Fw%3Dreserved=0 https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3318data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637538450446516854%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000sdata=2KKVA6qqHIP2skLSLXo56av1%2FS9pL1MMJbt%2FPI9BBPM%3Dreserved=0 https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fbugzilla.tianocore.org%2Fshow_bug.cgi%3Fid%3D3319data=04%7C01%7Cbret.barkelew%40microsoft.com%7C045c38141f1e443d1e4b08d8fdd78e23%7C72f98
Re: [EXTERNAL] Re: [edk2-devel] [GSoC proposal] Secure Image Loader
You’ve got my vote! This sounds amazing! - Bret From: Marvin Häuser via groups.io<mailto:mhaeuser=posteo...@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.desim...@intel.com>; Laszlo Ersek<mailto:ler...@redhat.com>; Andrew Fish<mailto:af...@apple.com>; Kinney, Michael D<mailto:michael.d.kin...@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 On Behalf Of Marvin >> Häuser >> Sent: Sunday, April 4, 2021 4:02 PM >> To: devel@edk2.groups.io; Laszlo Ersek ; Andrew Fish >> ; Kinney, Michael D >> 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 vi
