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.369.1618248144230447955 for ; Mon, 12 Apr 2021 10:22:25 -0700 Authentication-Results: mx.groups.io; dkim=fail reason="body hash did not verify" header.i=@posteo.de header.s=2017 header.b=YitWwpnX; 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 714992400E5 for ; Mon, 12 Apr 2021 19:22:22 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.de; s=2017; t=1618248142; bh=x4NlXpk+ffcevoGeeqaC/QaI5Tiqh9C1vmfn5++OGy0=; h=Subject:To:From:Date:From; b=YitWwpnXOfNRMESg5J//K3VHXkNxVN1BPV7sEp9CBuxIacr6cOY8HJYFRVTHNrwW+ klAa+B7YrEZO7oafMg4ZAMh/k1rkje0arJ6+seVJfWESWcuM3bOXSOkf/RYcErGSrl WI0me9n7rY20Ih92wGaa9fzz223urL1szxvRHsh4zL1ZvUZbf6nV/ZJ3TxhMsYrCft RYXDnNbAwPoER55b+iAAu6Z6RzLWx4JcCoy+YNeqS/zwAsn9z5qmYNXrGoZCdCIZQX wJIfbMCfH5wA9fwyaEAx5uNuRX0+g1/j787dUlPm2gU0WnHLU1ZrhQrKJDFvQctQYC 6U5cx0Y9pB6Gw== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 4FJwXV7061z9rxS; Mon, 12 Apr 2021 19:22:18 +0200 (CEST) Subject: Re: [edk2-devel] [GSoC proposal] Secure Image Loader To: devel@edk2.groups.io, nathaniel.l.desimone@intel.com, Laszlo Ersek , Andrew Fish , "Kinney, Michael D" References: From: =?UTF-8?B?TWFydmluIEjDpHVzZXI=?= Message-ID: <055bcd6f-c055-25a8-f258-6581ccbbd591@posteo.de> Date: Mon, 12 Apr 2021 19:22:17 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.9.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: quoted-printable Good day Nate, As you seem to be mostly in charge of the GSoC side of things, I direct=20 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= =20 deadline. You can find a list of BZs attached[1]. Please note that 1)=20 some are declared security issues and may not be publicly accessible,=20 and 2) that this list is far from complete. I only added items that are=20 a) not implicitly fixed by "simply" deploying the new Image Loader=20 (*some* important prerequisites are listed), and b) I am confident are=20 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= =20 architectural protocols, which I could not find a rationale for. I can=20 prepare something for this matter, but it really needs an active=20 discussion with some of the core people. I'm not sure delayed e-mail=20 discussion is going to be enough, but there is an official IRC I=20 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=20 "fill" 10 weeks, but rather the opposite. This is not a matter of=20 replacing a library instance, but the whole surrounding ecosystem needs=20 to follow for the changes to make sense. And as I tried to make clear in= =20 my discussion with Michael Brown, I am not keen on preserving=20 backwards-compatibility with platform code (i.e. PEI, DXE, things we=20 consider "internal"), as most of it should be controlled by EDK II=20 already. This of course does *not* include user code (OROMs,=20 bootloaders, ...), for which I want to provide the *option* to lock some= =20 of them out for security, but with sane defaults that will ensure good=20 compatibility. I'd like to thank Michael Brown for his cooperation and support, because= =20 we recently landed changes in iPXE to allow for the strictest image=20 format and permission constraints currently possible[2]. I will have to rework the submitted proposal to reflect the new=20 knowledge. To be honest, seeing how the BZs kept rolling in, I am not=20 convinced an amazing amount of mainlining can be accomplished during the= =20 10 weeks. It may have to suffice to have a publicly accessible prototype= =20 (e.g. OVMF) and a subset of the planned patches on the list. I hope you=20 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=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 [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! Co= mpleting 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 divide= nds for years to come. > > Admittedly, this is an area of computer science that I don't have a grea= t deal of experience with. The furthest I have gone on this topic is writin= g out proofs for simple algorithms on exams in my Algorithms class in colle= ge. 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 developm= ent window? Certainly we can use some of that time to perform the code revi= ews 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 w= ith any questions I still have. > > With Best Regards, > Nate > >> -----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 >> >> Good day everyone, >> >> I'll keep the introduction brief because I've been around for a while n= ow. :) I'm >> Marvin H=C3=A4user, a third-year Computer Science student from TU Kaise= rslautern, >> Germany. Late last year, my colleague Vitaly from ISP RAS and me introd= uced 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 La= szlo >> 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 p= reviously >> 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 signif= icant >> 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 proto= cols (e.g. >> returning data with no corresponding size) originating from the UEFI PI= and >> UEFI specifications. Changes need to be discussed, settled on, and subm= itted to >> the UEFI Forum. >> 4. Some UEFI APIs like the Security Architecture protocols are inconven= iently >> abstract, see 5. >> 5. Some of the current code does not use the existing context, or acces= ses it >> outside of the exposed APIs. The control flow of the dispatchers may ne= ed 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 chan= ges will >> be required from the last proven state. This gives a lot of trust in it= s correctness >> and safety. >> B. All outlined defects that are of critical nature have been fixed suc= cessfully. >> C. The Image Loader has been tested with real-world code loading real-w= orld >> OSes on thousands of machines in the past few months, including rejecti= ng >> malformed images (configurable by PCD). >> D. The new APIs will centralise everything PE, reducing code duplicatio= n 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 und= efined >> behaviour. >> H. I already managed to identify a malformed image in OVMF with its hel= p >> (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 dat= a >> segments when enabled. >> >> There are likely more points for both lists, but I hope this gives a de= cent >> starting point for discussion. What are your thoughts on the matter? I = strongly >> encourage everyone to read the section regarding defects of our publica= tion[2] >> to better understand the motivation. The vague points above can of cour= se 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 >> >> >> >> > > >=20 > >