From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from ma1-aaemail-dr-lapp02.apple.com (ma1-aaemail-dr-lapp02.apple.com [17.171.2.68]) by mx.groups.io with SMTP id smtpd.web11.428.1618326343470156995 for ; Tue, 13 Apr 2021 08:05:43 -0700 Authentication-Results: mx.groups.io; dkim=pass header.i=@apple.com header.s=20180706 header.b=HhbmCiXZ; spf=pass (domain: apple.com, ip: 17.171.2.68, mailfrom: afish@apple.com) Received: from pps.filterd (ma1-aaemail-dr-lapp02.apple.com [127.0.0.1]) by ma1-aaemail-dr-lapp02.apple.com (8.16.0.42/8.16.0.42) with SMTP id 13DEnEtg053485; Tue, 13 Apr 2021 08:05:42 -0700 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=apple.com; h=from : message-id : content-type : mime-version : subject : date : in-reply-to : cc : to : references; s=20180706; bh=HbtKavIjleso0kb7BsCllm00KPKywbyFC28ffJZZHX4=; b=HhbmCiXZeLtaW/DyW1v3gno7OJaugLx/8bT8kIFzIm4Sg3biz0ObLc9LTiwE6x4/a5z7 WBCQRIyLYI+9wHBD96vRiJ4OhxgmwNDVbG8/f7KmOH8JVHeC+MK4YyqIgC3UBIwTrkIB hvlheUSGOh2eWJr2NFGWevjQLinUctVad8JWa/dnTLSYt94OQ+hrur/eo4pMOxCd7Y9S jei/WxqdZDU+cy5JjHv5DFwjIEjxYEaTRL85a3AaSe9UJbQyCLym9TCgwJkTFznVOKVD 1Ss1FuMBDKmlxKeoUAWP6UoYR+xGtkjFuKHZe02bHrdEhxGrvDWgT8MRr4v2oli9S+He yA== Received: from rn-mailsvcp-mta-lapp01.rno.apple.com (rn-mailsvcp-mta-lapp01.rno.apple.com [10.225.203.149]) by ma1-aaemail-dr-lapp02.apple.com with ESMTP id 37u8psketa-22 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NO); Tue, 13 Apr 2021 08:05:42 -0700 Received: from rn-mailsvcp-mmp-lapp01.rno.apple.com (rn-mailsvcp-mmp-lapp01.rno.apple.com [17.179.253.14]) by rn-mailsvcp-mta-lapp01.rno.apple.com (Oracle Communications Messaging Server 8.1.0.7.20201203 64bit (built Dec 3 2020)) with ESMTPS id <0QRI00J86CLGP6F0@rn-mailsvcp-mta-lapp01.rno.apple.com>; Tue, 13 Apr 2021 08:05:40 -0700 (PDT) Received: from process_milters-daemon.rn-mailsvcp-mmp-lapp01.rno.apple.com by rn-mailsvcp-mmp-lapp01.rno.apple.com (Oracle Communications Messaging Server 8.1.0.7.20201203 64bit (built Dec 3 2020)) id <0QRI00300CBYQZ00@rn-mailsvcp-mmp-lapp01.rno.apple.com>; Tue, 13 Apr 2021 08:05:40 -0700 (PDT) X-Va-A: X-Va-T-CD: cb83049425a79c8a5fb9f1dafa0fda92 X-Va-E-CD: 6a647426990f4fc248f9d9721cb161d4 X-Va-R-CD: 0ee6c4a95a2e1248d03989c9ba42fe98 X-Va-CD: 0 X-Va-ID: b554189f-d9c6-4b78-9dec-be09fca68189 X-V-A: X-V-T-CD: cb83049425a79c8a5fb9f1dafa0fda92 X-V-E-CD: 6a647426990f4fc248f9d9721cb161d4 X-V-R-CD: 0ee6c4a95a2e1248d03989c9ba42fe98 X-V-CD: 0 X-V-ID: bad6acd6-abfb-4d38-880a-6f921a6ca409 X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.391,18.0.761 definitions=2021-04-13_08:2021-04-13,2021-04-13 signatures=0 Received: from [17.235.15.59] (unknown [17.235.15.59]) by rn-mailsvcp-mmp-lapp01.rno.apple.com (Oracle Communications Messaging Server 8.1.0.7.20201203 64bit (built Dec 3 2020)) with ESMTPSA id <0QRI00YD6CLEBH00@rn-mailsvcp-mmp-lapp01.rno.apple.com>; Tue, 13 Apr 2021 08:05:40 -0700 (PDT) From: "Andrew Fish" Message-id: <91547B14-AD84-4229-8A5D-A1941294EE06@apple.com> MIME-version: 1.0 (Mac OS X Mail 14.0 \(3654.20.0.2.1\)) Subject: Re: [edk2-devel] [GSoC proposal] Secure Image Loader Date: Tue, 13 Apr 2021 08:05:38 -0700 In-reply-to: <4fa3c0fc-8865-447e-96ec-7286b0fd9a7f@posteo.de> Cc: "Desimone, Nathaniel L" , Mike Kinney , devel@edk2.groups.io, Laszlo Ersek To: =?utf-8?Q?Marvin_H=C3=A4user?= References: <055bcd6f-c055-25a8-f258-6581ccbbd591@posteo.de> <4fa3c0fc-8865-447e-96ec-7286b0fd9a7f@posteo.de> X-Mailer: Apple Mail (2.3654.20.0.2.1) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.391,18.0.761 definitions=2021-04-13_08:2021-04-13,2021-04-13 signatures=0 Content-type: multipart/alternative; boundary="Apple-Mail=_594EB1AC-F78E-4DFE-8678-FC18CFF697A6" --Apple-Mail=_594EB1AC-F78E-4DFE-8678-FC18CFF697A6 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Marvin, School of hard knocks=E2=80=A6 Bug rates have gone up around the world as = the security experts show up with security fixes. Most commonly the bugs ar= e around functionality and not security. While a brick is very secure (sinc= e the customer can=E2=80=99t use it), customers generally don=E2=80=99t lik= e their products turning into bricks. Thus we tend to be conservative on la= rger changes.=20 There is a large ecosystem surrounding edk2, and you need to factor in thi= ngs like products that are in sustaining for large number of years (these p= roducts may be more conservative) and people may want to be conservative. T= he edi2 does not generally deprecate things right away. We generally add n= ew extra things and slowly deprecate over time.=20 It might be useful to review the LibraryClass (API) changes and try and un= derstand the issues in the current design.=20 Thanks, Andrew Fish > On Apr 13, 2021, at 12:31 AM, Marvin H=C3=A4user wr= ote: >=20 > Hey Mike, > Hey Nate, >=20 > I'm not 100 % sure I get what you mean. The interfaces of the two soluti= ons are not compatible (however I could write wrapper code to shim the old = into the new I suppose?), so on-the-fly switching between the two would be = inconvenient. I do plan to keep the old library around and guard it with th= e deprecated interfaces macro, for out-of-tree code, however. The new libra= ry interfaces will probably be something like PeCoffLib2, PeCoffDebugLib2, = maybe more. >=20 > I'm also not sure what on-the-fly switching would accomplish, as testing= with the old loader allows broken images to be loaded, i.e. just because s= omething "works" with the old code but not the new, it doesn't mean that th= e new code is broken. >=20 > Instead of debugging with two libraries, I rather want to make sure this= thing is rock-solid before even sending out the patches. For this I would = like to build a small EFI file database to parse and load from userland, ch= ecking for image acceptance and memory safety. This would include several v= ersions of Windows and macOS bootloaders, Option ROMs (NVIDIA and AMD GOP, = iPXE), tools (memtest), and so on. If you have anything you want to have es= pecially tested, please let me know. >=20 > Best regards, > Marvin >=20 > 13.04.2021 02:56:22 Desimone, Nathaniel L >: >=20 >> Hi Marvin, >>=20 >> I agree with Mike K that having both the new strict loader and the old = loader co-exist for some time may be the best option. That will give the ec= osystem time to test the new loader and correct any issues that arise from = its 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; Desi= mone, 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 in= stance 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 pr= oposal and gives the ecosystem time to evaluate and decide when/if to switc= h 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 approac= h. >>>=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 pas= ses 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 ag= ree with you that getting a formally verified PE/COFF loader into mainline = is 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 men= tion and write up formal ECRs for the UEFI spec changes that you believe ar= e 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 pr= otocols (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. >>>>>=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 = 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. >>>>>=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 du= e 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 --Apple-Mail=_594EB1AC-F78E-4DFE-8678-FC18CFF697A6 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 Marvin,
School of hard knocks=E2=80=A6 Bug rates= have gone up around the world as the security experts show up with securit= y fixes. Most commonly the bugs are around functionality and not security. = While a brick is very secure (since the customer can=E2=80=99t use it), cus= tomers generally don=E2=80=99t like their products turning into bricks. Thu= s we tend to be conservative on larger changes. 
=
There is a large ecosystem surrounding= edk2, and you need to factor in things like products that are in sustainin= g for large number of years (these products may be more conservative) and p= eople may want to be conservative. The edi2  does not generally deprec= ate things right away. We generally add new extra things and slowly depreca= te over time. 

It might be useful to review the LibraryClass (API) changes and try and = understand the issues in the current design. 
Thanks,

Andrew Fish

On Apr 13, 2021, at 12:31 = AM, Marvin H=C3=A4user <mhaeuser@posteo.de> wrote:

Hey Mike,
Hey Nate,

I'm not 100 % sure I get what you mean. The interfaces of the two solutio= ns are not compatible (however I could write wrapper code to shim the old i= nto the new I suppose?), so on-the-fly switching between the two would be i= nconvenient. 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 librar= y interfaces will probably be something like PeCoffLib2, PeCoffDebugLib2, m= aybe more.

I'm also not sure what on-the-fly switching woul= d accomplish, as testing with the old loader allows broken images to be loa= ded, i.e. just because something "works" with the old code but not the new,= it doesn't mean that the new code is broken.

Instead of de= bugging with two libraries, I rather want to make sure this thing is rock-s= olid before even sending out the patches. For this I would like to build a = small EFI file database to parse and load from userland, checking for image= acceptance and memory safety. This would include several versions of Windo= ws and macOS bootloaders, Option ROMs (NVIDIA and AMD GOP, iPXE), tools (me= mtest), and so on. If you have anything you want to have especially tested,= please let me know.

Best regards,
Marvin

13.04.2021 02:56:22 De= simone, Nathaniel L <nathaniel.l.desimone@in= tel.com>:

Hi Marvin,

I agree with Mike K that having both the new strict loade= r and the old loader co-exist for some time may be the best option. That wi= ll give the ecosystem time to test the new loader and correct any issues th= at arise from its introduction.

Best Regards,<= br class=3D"">Nate

-----Original Message-----<= br class=3D"">From: Kinney, Michael D <michael.d.kinney@intel.com>
Se= nt: Monday, April 12, 2021 5:20 PM
To: Marvin H=C3=A4user <= ;mhaeuser@posteo.de>= ;; devel@edk2.groups.io<= /a>; Desimone, Nathaniel L <nathaniel.l.desimone@intel.com>; Laszlo Ersek <<= a href=3D"mailto:lersek@redhat.com" class=3D"">lersek@redhat.com>; A= ndrew Fish <afish@apple.co= m>; Kinney, Michael D <michael.d.kinney@intel.com>
Subject: RE= : [edk2-devel] [GSoC proposal] Secure Image Loader

Hi Marvin,

If it has not already been c= onsidered, one option is to submit a new instance of the PE/COFF Library, s= o both the existing one and the new one are available to the ecosystem.

This allows you to be successful in submitting co= de outlined in your proposal and gives the ecosystem time to evaluate and d= ecide when/if to switch from the old to the new.

Mike

-= ----Original Message-----
From: Marvin H=C3=A4user <mhaeuser@posteo.de>
Sent: Monday, April 12, 2021 10:22 AM
To: devel@edk2.groups.io; Desimone= , Nathaniel L
<nathaniel.l.desimone@intel.com>; Laszlo Ersek <= lersek@redhat.com>;<= br class=3D"">Andrew Fish <afish@apple.com>; Kinney, Michael D
<michael.d.kinney@intel.com&= gt;
Subject: Re: [edk2-devel] [GSoC proposal] Secure Image Lo= ader

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 investigati= ons 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 l= ist 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 confi= dent are
actual issues (or things to consider) I believe to k= now 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 pre= pare 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. Th= is is not a matter of
replacing a library instance, but the w= hole surrounding ecosystem
needs to follow for the changes to= make sense. And as I tried to make
clear in my discussion wi= th Michael Brown, I am not keen on preserving
backwards-compa= tibility with platform code (i.e. PEI, DXE, things we
conside= r "internal"), as most of it should be controlled by EDK II
a= lready. This of course does *not* include user code (OROMs,
b= ootloaders, ...), for which I want to provide the *option* to lock
some of them out for security, but with sane defaults that will ensu= re
good compatibility.

I'd like = to thank Michael Brown for his cooperation and support,
becau= se 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 ref= lect the new
knowledge. To be honest, seeing how the BZs kept= rolling in, I am not
convinced an amazing amount of mainlini= ng 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 to= morrow.

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=3D3316https://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://bugzil= la.tianocore.org/show_bug.cgi?id=3D3321
https://bugzilla.tian= ocore.org/show_bug.cgi?id=3D3322
https://bugzilla.tianocore.o= rg/show_bug.cgi?id=3D3323
https://bugzilla.tianocore.org/show= _bug.cgi?id=3D3324
https://bugzilla.tianocore.org/show_bug.cg= i?id=3D3326
https://bugzilla.tianocore.org/show_bug.cgi?id=3D= 3327
https://bugzilla.tianocore.org/show_bug.cgi?id=3D3328https://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 mee= t you and welcome back! Glad you hear you are
interested! Com= pleting a formal verification of a PE/COFF
loade= r is certainly impressive. Was this done with some sort of
au= tomated 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 mainlin= e is undoubtably valuable and would pay security dividends for years to com= e.

Admitt= edly, 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 muc= h
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 mention and write up formal ECRs for the UEFI spec cha= nges 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 you= r paper
more closely and come back with any ques= tions I still have.

With Best Regards,
Nate

-----Original Message-----
From: devel@edk2.groups.io <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 <lersek@re= dhat.com>; Andrew
Fish <afish@apple.com>; Kinney, Mi= chael D
<michael.d.kinney@intel.com>
Subj= ect: [edk2-devel] [GSoC proposal] Secure Image Loader

Good day everyone,

I'll keep the intro= duction brief because I've been around for a
while now. :) I'= m Marvin H=C3=A4user, a third-year Computer Science
student f= rom TU Kaiserslautern, Germany. Late last year, my
colleague = Vitaly from ISP RAS and me introduced a formally verified
Ima= ge Loader for UEFI usage at ISP RAS Open[1] due to various
de= fects we outlined in the corresponding paper. Thank you once again Laszlo f= or 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 previ= ously submitted a proposal via the GSoC website for your review.

There are many things to consider:
1. T= he 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 e= xploration, I discovered defective PPIs and protocols (e.g.
r= eturning 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 U= EFI APIs like the Security Architecture protocols are
inconve= niently abstract, see 5.
5. Some of the current code does not= use the existing context, or
accesses it outside of the expo= sed 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-w= orld code loading
real-world OSes on thousands of machines in= the past few months,
including rejecting malformed images (c= onfigurable by PCD).
D. The new APIs will centralise everythi= ng PE, reducing code
duplication and potentially unsafe opera= tions.
E. Centralising and reduced parse duplication may impr= ove overall
boot performance.
F. The code has b= een coverage-tested to not contain dead code.
G. The code has= been fuzz-tested including sanitizers to not invoke
undefine= d behaviour.
H. I already managed to identify a malformed ima= ge in OVMF with its
help (incorrectly reported section alignm= ent of an Intel IPXE
driver). A fix will be submitted shortly= .
I. I plan to support PE section permissions, allowing for r= ead-only
data segments when enabled.

There are likely more points for both lists, but I hope this givesa decent starting point for discussion. What are your thoughts= on
the matter? I strongly encourage everyone to read the sec= tion
regarding defects of our publication[2] to better unders= tand 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.0= 5471.pdf







--Apple-Mail=_594EB1AC-F78E-4DFE-8678-FC18CFF697A6--