From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from rn-mailsvcp-ppex-lapp14.apple.com (rn-mailsvcp-ppex-lapp14.apple.com [17.179.253.33]) by mx.groups.io with SMTP id smtpd.web08.8616.1617891199487218875 for ; Thu, 08 Apr 2021 07:13:19 -0700 Authentication-Results: mx.groups.io; dkim=pass header.i=@apple.com header.s=20180706 header.b=wq/h7kWV; spf=pass (domain: apple.com, ip: 17.179.253.33, mailfrom: afish@apple.com) Received: from pps.filterd (rn-mailsvcp-ppex-lapp14.rno.apple.com [127.0.0.1]) by rn-mailsvcp-ppex-lapp14.rno.apple.com (8.16.1.2/8.16.1.2) with SMTP id 138E8ce6016443; Thu, 8 Apr 2021 07:13:19 -0700 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=apple.com; h=content-type : content-transfer-encoding : from : mime-version : subject : date : message-id : references : cc : in-reply-to : to; s=20180706; bh=cPzxQ+nh4a7ILxYiZH9DY+D1XDhka6/NfoYQEz85YaM=; b=wq/h7kWVDSofNSnvHPDpH4TFBTWBWjM3jMYZ0Tezv9AEPD0Szz2QS6ygHBno4k1uKYIz 1OxSAkTEab9KthuFnJzMDMVF8+HYRqAqkxJJ8Ljxx5UnnOocHOovpnTe8SOQshiya4A9 hyWJJW1OrSJFc6SncNTGf8Uq36rpfG/LDrQPb2ADaK/KsNVc1giFrE51/BiLSY/oyEUU 4QU8kbUZOnZ4kQRShtoT+LhhRT9U2cld1EcjmhBDJ9oe9mzO3+gIqYldewnAF4zpuQZO AP/7GQfRUjEKgyazoC//Mmj5xx2ljZoU1d1Q8j2HQF5Al7sIvelwalp/E6L2+c+XqLg6 dw== Received: from rn-mailsvcp-mta-lapp02.rno.apple.com (rn-mailsvcp-mta-lapp02.rno.apple.com [10.225.203.150]) by rn-mailsvcp-ppex-lapp14.rno.apple.com with ESMTP id 37rvcnkr9y-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NO); Thu, 08 Apr 2021 07:13:19 -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-lapp02.rno.apple.com (Oracle Communications Messaging Server 8.1.0.7.20201203 64bit (built Dec 3 2020)) with ESMTPS id <0QR900LA80U6D0B0@rn-mailsvcp-mta-lapp02.rno.apple.com>; Thu, 08 Apr 2021 07:13:18 -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 <0QR900S000RS2K00@rn-mailsvcp-mmp-lapp01.rno.apple.com>; Thu, 08 Apr 2021 07:13:18 -0700 (PDT) X-Va-A: X-Va-T-CD: 076955f3becce2df77d006c843a15678 X-Va-E-CD: 6a647426990f4fc248f9d9721cb161d4 X-Va-R-CD: 3db871e426e13968f3f555110583bf18 X-Va-CD: 0 X-Va-ID: d0f2f36d-9c90-4170-ad1a-c52c9a33ac0e X-V-A: X-V-T-CD: 076955f3becce2df77d006c843a15678 X-V-E-CD: 6a647426990f4fc248f9d9721cb161d4 X-V-R-CD: 3db871e426e13968f3f555110583bf18 X-V-CD: 0 X-V-ID: 0b0b6f6d-ef88-4d93-a82a-e822698d55cf X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.391,18.0.761 definitions=2021-04-08_03:2021-04-08,2021-04-08 signatures=0 Received: from [10.104.112.97] (unknown [10.104.112.97]) 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 <0QR900BCX0U5S400@rn-mailsvcp-mmp-lapp01.rno.apple.com>; Thu, 08 Apr 2021 07:13:18 -0700 (PDT) From: "Andrew Fish" MIME-version: 1.0 (1.0) Subject: Re: [edk2-devel] [GSoC proposal] Secure Image Loader Date: Thu, 08 Apr 2021 07:13:15 -0700 Message-id: References: <259a114d-7132-1774-d46a-8e8d9b4ff5e2@redhat.com> Cc: =?utf-8?Q?Marvin_H=C3=A4user?= , nathaniel.l.desimone@intel.com, "Kinney, Michael D" In-reply-to: <259a114d-7132-1774-d46a-8e8d9b4ff5e2@redhat.com> To: devel@edk2.groups.io, lersek@redhat.com X-Mailer: iPhone Mail (18D70) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.391,18.0.761 definitions=2021-04-08_03:2021-04-08,2021-04-08 signatures=0 Content-type: text/plain; charset=utf-8 Content-transfer-encoding: quoted-printable At a minimum it would be nice if we had a tool that would point out the sec= urity faults with a given PE/COFF file layout.=20 > On Apr 8, 2021, at 4:16 AM, Laszlo Ersek wrote: >=20 > =EF=BB=BFOn 04/06/21 12:06, Marvin H=C3=A4user wrote: >> Good day Nate, >>=20 >> Comments are inline. >>=20 >> Best regards, >> Marvin >>=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! >>=20 >> 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 logic >> statements with C-like syntax. >>=20 >>> 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. >>=20 >> I'm glad to hear that. :) >>=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? >>=20 >> 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. Whil= e >> 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 underlyin= g >> 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), and >> so on. I was rather worried the scope is too broad time-wise, but it ca= n >> be narrowed/widened as you see fit really. This is one of *the* core >> components used on millions of device, and many package maintainers nee= d >> to review and validate the changes, this must really be done right the >> first try. :) >>=20 >>> Certainly we can use some of that time to perform the code reviews you >>> mention and write up formal ECRs for the UEFI spec changes that you >>> believe are needed. >>=20 >> I believed that was part of the workload, yes, but even without it I >> think there is plenty to do. >>=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 >> Thank you, I will gladly explain anything unclear. Just try to not give >> Laszlo too many flashbacks. :) >=20 > I haven't commented yet in this thread, as I thought my stance on this > undertaking was (or should be) obvious. >=20 > I very much welcome a replacement for the PE/COFF parser (as I consider > its security issues unfixable in an incremental manner). From my reading > 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. >=20 > 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. >=20 > Thanks > Laszlo >=20 >=20 >=20 >=20 >=20 >>=20 >>>=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 Fi= sh >>>> ; 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 ha= s >>>> 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 >>>> 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. >>>>=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 boo= t >>>> 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 h= elp >>>> (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 d= ata >>>> 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 >>=20 >=20 >=20 >=20 >=20 >=20 >=20