From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mout02.posteo.de (mout02.posteo.de [185.67.36.66]) by mx.groups.io with SMTP id smtpd.web10.5744.1618299137746292903 for ; Tue, 13 Apr 2021 00:32:18 -0700 Authentication-Results: mx.groups.io; dkim=pass header.i=@posteo.de header.s=2017 header.b=CXpQXGcT; spf=pass (domain: posteo.de, ip: 185.67.36.66, mailfrom: mhaeuser@posteo.de) Received: from submission (posteo.de [89.146.220.130]) by mout02.posteo.de (Postfix) with ESMTPS id D428C2400FC for ; Tue, 13 Apr 2021 09:32:05 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.de; s=2017; t=1618299125; bh=LIe6UL64VexqRnnecJna9ZexnBqaCLYNyd92qT7RMBw=; h=Date:From:To:Cc:Subject:From; b=CXpQXGcTAnskRfstUwbekWGBWvtQjpXQ1+XKJ0pTqpQCme17OvZ5D6E3SyJGWiwlk 8zzFhN3dUFQdOEgc8kUw3BPcU3pYeyu1Cune7iHq1Ud2lPazB8WAL6YD+V8SAMSxxb xV1n+jroMn8ktygxNl2SPxfclC3JGHHEB2YE8XWOp4skpMeVQ1GqZo7Fhimg0GhZ/v fl58DAMYHdXYtvMInbW4nqdOWbOHuVJEa8/XuNvXzgPfTfm9TdQFAd9ZOtHAIbrVVY NGjwzSuVwtwYVYKdkiTM6AK8lQ5DjQkOEoL1se8vhstBCqp1ucQfyqjX0WIJR92MYk P+rmMxzn5lBRg== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 4FKHNz1vPRz6tmR; Tue, 13 Apr 2021 09:32:03 +0200 (CEST) Date: Tue, 13 Apr 2021 07:31:59 +0000 (UTC) From: =?UTF-8?B?TWFydmluIEjDpHVzZXI=?= To: "Desimone, Nathaniel L" Cc: "Kinney, Michael D" , devel@edk2.groups.io, Laszlo Ersek , Andrew Fish Message-ID: <4fa3c0fc-8865-447e-96ec-7286b0fd9a7f@posteo.de> In-Reply-To: References: <055bcd6f-c055-25a8-f258-6581ccbbd591@posteo.de> Subject: Re: [edk2-devel] [GSoC proposal] Secure Image Loader MIME-Version: 1.0 X-Correlation-ID: <4fa3c0fc-8865-447e-96ec-7286b0fd9a7f@posteo.de> Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Hey Mike, Hey Nate, I'm not 100 % sure I get what you mean. The interfaces of the two solution= s are not compatible (however I could write wrapper code to shim the old in= to the new I suppose?), so on-the-fly switching between the two would be in= convenient. 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, ma= ybe more. I'm also not sure what on-the-fly switching would accomplish, as testing w= ith the old loader allows broken images to be loaded, i.e. just because som= ething "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 t= hing is rock-solid before even sending out the patches. For this I would li= ke to build a small EFI file database to parse and load from userland, chec= king for image acceptance and memory safety. This would include several ver= sions of Windows and macOS bootloaders, Option ROMs (NVIDIA and AMD GOP, iP= XE), tools (memtest), and so on. If you have anything you want to have espe= cially tested, please let me know. Best regards, Marvin 13.04.2021 02:56:22 Desimone, Nathaniel L = : > Hi Marvin, >=20 > I agree with Mike K that having both the new strict loader and the old l= oader co-exist for some time may be the best option. That will give the eco= system time to test the new loader and correct any issues that arise from i= ts introduction. >=20 > Best Regards, > Nate >=20 > -----Original Message----- > From: Kinney, Michael D > Sent: Monday, April 12, 2021 5:20 PM > To: Marvin H=C3=A4user ; devel@edk2.groups.io; Desim= one, Nathaniel L ; Laszlo Ersek ; Andrew Fish ; Kinney, Michael D > Subject: RE: [edk2-devel] [GSoC proposal] Secure Image Loader >=20 > Hi Marvin, >=20 > If it has not already been considered, one option is to submit a new ins= tance of the PE/COFF Library, so both the existing one and the new one are = available to the ecosystem. >=20 > This allows you to be successful in submitting code outlined in your pro= posal and gives the ecosystem time to evaluate and decide when/if to switch= from the old to the new. >=20 > Mike >=20 >> -----Original Message----- >> From: Marvin H=C3=A4user >> Sent: Monday, April 12, 2021 10:22 AM >> To: devel@edk2.groups.io; Desimone, Nathaniel L >> ; Laszlo Ersek ; >> Andrew Fish ; Kinney, Michael D >> >> Subject: Re: [edk2-devel] [GSoC proposal] Secure Image Loader >>=20 >> Good day Nate, >>=20 >> 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. >>=20 >> 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= . >>=20 >> 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. >>=20 >> 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. >>=20 >> 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]. >>=20 >> 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 pass= es tomorrow. >>=20 >> Thank you in advance! >>=20 >> Best regards, >> Marvin >>=20 >> [1] >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3315 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3316 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3317 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3318 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3319 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3320 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3321 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3322 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3323 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3324 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3326 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3327 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3328 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3329 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3330 >> https://bugzilla.tianocore.org/show_bug.cgi?id=3D3331 >>=20 >> [2] https://github.com/ipxe/ipxe/pull/313 >>=20 >> On 06.04.21 11:41, Nate DeSimone wrote: >>> Hi Marvin, >>>=20 >>> 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 agr= ee with you that getting a formally verified PE/COFF loader into mainline i= s undoubtably valuable and would pay security dividends for years to come. >>>=20 >>> 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 ment= ion and write up formal ECRs for the UEFI spec changes that you believe are= needed. >>>=20 >>> 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. >>>=20 >>> With Best Regards, >>> Nate >>>=20 >>>> -----Original Message----- >>>> From: devel@edk2.groups.io On Behalf Of >>>> Marvin H=C3=A4user >>>> 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 >>>>=20 >>>> Good day everyone, >>>>=20 >>>> I'll keep the introduction brief because I've been around for a >>>> while now. :) I'm Marvin H=C3=A4user, 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. >>>>=20 >>>> 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. >>>>=20 >>>> 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 pro= tocols (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 a= ppropriate APIs. >>>>=20 >>>> 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 s= uccessfully. >>>> 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. >>>>=20 >>>> 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. >>>>=20 >>>> Thank you for your time! >>>>=20 >>>> Best regards, >>>> Marvin >>>>=20 >>>>=20 >>>> [1] https://github.com/mhaeuser/ISPRASOpen-SecurePE >>>> [2] https://arxiv.org/pdf/2012.05471.pdf >>>>=20 >>>>=20 >>>>=20 >>>>=20 >>>=20 >>>=20 >>>=20 >>>=20 >>>=20