From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mout01.posteo.de (mout01.posteo.de [185.67.36.65]) by mx.groups.io with SMTP id smtpd.web11.9827.1617703790432187882 for ; Tue, 06 Apr 2021 03:09:51 -0700 Authentication-Results: mx.groups.io; dkim=fail reason="body hash did not verify" header.i=@posteo.de header.s=2017 header.b=aX6V0FmZ; spf=pass (domain: posteo.de, ip: 185.67.36.65, mailfrom: mhaeuser@posteo.de) Received: from submission (posteo.de [89.146.220.130]) by mout01.posteo.de (Postfix) with ESMTPS id 9C8F31605FA for ; Tue, 6 Apr 2021 12:06:24 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.de; s=2017; t=1617703585; bh=uZN8xFLJjoc/ZdsCXDttyxrzy96Tvls9uHxKq5JG1R4=; h=Subject:To:From:Date:From; b=aX6V0FmZB7fq0YiZ5w/YOgPoUP8Om6cV5GEKsIZD9xfMwzoXoSlEM9gridsSV7xXy Dk99+i6VUsUaYyLydCbGAFfbuKkfb6zinUr9MQq0Fz4S5jmNu09Y4o+oCpmupye76a rH4XmBUonjnZSuUAZkl7l6JRW41tHCT/d5bGHaQ6zaqc43N0qfGm3du6zhSNpG17Ll dBOpN2Yky+ltLH9EzdgUPQUFoMtlzbv2KPixHru8cGPJTvefI4zlBDCdVOws7bjlpb jvqqMmogzirMeHKVIQJOd1s+Y8oHe5sWwxL/XrVi1f9L1W6f8BNfskvj4pGq5TLTyq aCy5Jjvn1jlIg== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 4FF38D72PKz9rxf; Tue, 6 Apr 2021 12:06:20 +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: <58da76c7-5e2e-8e21-9e20-b17523cfa837@posteo.de> Date: Tue, 6 Apr 2021 12:06:17 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.8.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, 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! 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 would call it "semi-automated", a great deal of intermediate goals=20 (preconditions, postconditions, invariants, assertions, ...) were=20 required to show all interesting properties. But yes, the actual proof=20 steps are automated by common SMT solvers. It was done using the=20 AstraVer Toolset and ACSL, latter basically a language to express logic=20 statements with C-like syntax. > I completely agree with you that getting a formally verified PE/COFF loa= der 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 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? Please don't get me wrong, but I would be surprised if the UEFI=20 specification changes I'd like to discuss alone would be completed=20 within 10 weeks, let alone implementation throughout the codebase. While= =20 I think the plain amount of code may be a bit less than say a=20 MinPlatform port, the changes are much deeper and require much more=20 caution to avoid regressions (e.g. by invalidating undocumented=20 assertions). This sadly is not a matter of just replacing the underlying= =20 library implementation or "plug-in and play" at all. It furthermore=20 affects many parts of the stack, the core dispatchers used for all=20 platforms, image emulation (EBC), UEFI userland emulation (EmuPkg), and=20 so on. I was rather worried the scope is too broad time-wise, but it can= =20 be narrowed/widened as you see fit really. This is one of *the* core=20 components used on millions of device, and many package maintainers need= =20 to review and validate the changes, this must really be done right the=20 first try. :) > Certainly we can use some of that time to perform the code reviews you m= ention 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=20 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 w= ith any questions I still have. Thank you, I will gladly explain anything unclear. Just try to not give=20 Laszlo too many flashbacks. :) > > 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 > >