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.web11.131.1617897991388469043 for ; Thu, 08 Apr 2021 09:06:32 -0700 Authentication-Results: mx.groups.io; dkim=fail reason="body hash did not verify" header.i=@posteo.de header.s=2017 header.b=JHGUb6ZZ; 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 D4C2D240106 for ; Thu, 8 Apr 2021 18:06:27 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.de; s=2017; t=1617897987; bh=zw9IP0lj/h7u0O08Sx+o7E2LDBZ9qc3sUbyctWkyzcM=; h=Subject:To:Cc:From:Date:From; b=JHGUb6ZZkpT+BdppmJ1NI3zIPog/G64xQ6ICk+kanwPUYOVYuIaD9Q6M2Ni86jGw4 faAEjBqIVgIBZGtOM+P7XOyDabpdKV9jXTQFKVuCw0s2WgMJF9p1fCJz6KYP6KD33+ gjos1aySf61xaxUvyowVApxSvrh6x7N14OtdE9sQIXvbQ4ojefPkByMTr0y3wkwlQv CMMWIf1r0w5OjT+MkK6gtBkSBmlcOoU4k2qrMf24JlEGAGpyEuiA/EERqiFcCQb1OY jaMlXRrIw/KST79ZPfr53jBNLpByV5S7ntOUtFJuECJ3Toe0ahqPmXConNfr7Vu9rm GI0zSUP12Vh3w== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 4FGR2p2KQFz6tmH; Thu, 8 Apr 2021 18:06:26 +0200 (CEST) Subject: Re: [edk2-devel] [GSoC proposal] Secure Image Loader To: "Andrew (EFI) Fish" , devel@edk2.groups.io, lersek@redhat.com Cc: nathaniel.l.desimone@intel.com, "Kinney, Michael D" References: <259a114d-7132-1774-d46a-8e8d9b4ff5e2@redhat.com> From: =?UTF-8?B?TWFydmluIEjDpHVzZXI=?= Message-ID: <8dcae34e-e975-9233-3738-62662201aae9@posteo.de> Date: Thu, 8 Apr 2021 18:06:25 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.9.0 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 We use the loader code in userspace anyway for fuzzing and such. I also=20 want to build a database of all sorts of UEFI binaries some time before=20 the merge to confirm they are all accepted (Windows / macOS / Linux=20 bootloaders, tools like memtest, drivers like iPXE). As part of that,=20 I'm sure we can have a userspace tool that uses the code to emit parsing= =20 information. But as the EDK II build system is very... not so userspace friendly, I=20 will not promise it will be very nice. :) Best regards, Marvin On 08.04.21 16:13, Andrew (EFI) Fish wrote: > At a minimum it would be nice if we had a tool that would point out the = security faults with a given PE/COFF file layout. > > Sent from my iPhone > >> On Apr 8, 2021, at 4:16 AM, Laszlo Ersek wrote: >> >> =EF=BB=BFOn 04/06/21 12:06, Marvin H=C3=A4user wrote: >>> 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 logi= c >>> 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 t= o >>>> 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. Whi= le >>> 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 underlyi= ng >>> 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), an= d >>> so on. I was rather worried the scope is too broad time-wise, but it c= an >>> be narrowed/widened as you see fit really. This is one of *the* core >>> components used on millions of device, and many package maintainers ne= ed >>> 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 yo= u >>>> 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 giv= e >>> Laszlo too many flashbacks. :) >> I haven't commented yet in this thread, as I thought my stance on this >> undertaking was (or should be) obvious. >> >> I very much welcome a replacement for the PE/COFF parser (as I consider >> its security issues unfixable in an incremental manner). From my readin= g >> of Marvin's and Vitaly's paper (draft), they have my full trust, and I'= m >> ready to put their upcoming code to use in ArmVirtPkg and OvmfPkg with >> minimal actual code review. If fixing the pervasive security problems >> around this area cannot avoid spiraling out to other core code in edk2, >> such as dispatchers, and even to the PI / UEFI specs, so be it. >> >> Regarding GSoC itself: as I stated elsewhere previously, I support >> edk2's participation in GSoC, while at the same time I'm not >> volunteering for mentorship at all. I'm uncertain if GSoC is the best >> framework for upstreaming such a large undertaking, but if it can help, >> we should use it as much as possible. >> >> Thanks >> Laszlo >> >> >> >> >> >>>> With Best Regards, >>>> Nate >>>> >>>>> -----Original Message----- >>>>> From: devel@edk2.groups.io On Behalf Of Marvi= n >>>>> H=C3=A4user >>>>> Sent: Sunday, April 4, 2021 4:02 PM >>>>> To: devel@edk2.groups.io; Laszlo Ersek ; Andrew F= ish >>>>> ; 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 whil= e >>>>> 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. >>>>> >>>>> 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 h= as >>>>> 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 hav= e >>>>> 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 bo= ot >>>>> 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] https://github.com/mhaeuser/ISPRASOpen-SecurePE >>>>> [2] https://arxiv.org/pdf/2012.05471.pdf >>>>> >>>>> >>>>> >>>>> >>>> >>>> >>>> >>>> >> >> >>=20 >> >>