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.web09.80.1617903551234581805 for ; Thu, 08 Apr 2021 10:39:11 -0700 Authentication-Results: mx.groups.io; dkim=pass header.i=@apple.com header.s=20180706 header.b=K7TvbWMw; 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 138Hcs0x036204; Thu, 8 Apr 2021 10:39:10 -0700 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=apple.com; h=content-type : mime-version : subject : from : in-reply-to : date : cc : content-transfer-encoding : message-id : references : to; s=20180706; bh=Hpa9d8N2Ag3mUn4mV2tWlDbWZiDAK7q9ZP8TYbQRFjU=; b=K7TvbWMwb/KW0Ou5oKhiex/mBXrc2YhCgP78o6hAsWqZp8M8Fvhy/opX73GGJViHMjH+ f0XkXVZlGoUd/2KgniIl48sYQsxUvBd0EeJ1vgSNLeZJ6/z0o+uwKzHBPtlam1TYIrRZ 9yzndupSTdOCEvc3TlJQsjkCmTVFGLcgX/v91VftbE6uX6I+aOmmwdZ8x+5N0K/R2juC dYHeZ6/CKa4q0Cudxs4aa9137ILoFRjtrt3AiURMb4I4oBUoZuv1DJAE7jwhUPZxUyB3 v5r+TuzXco/8KGRYEssvZS91k95NIDw0VMyMO9moHt/Uh6J8U2nJOu+84kXu9x5GIy6y 4g== 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 37t4nt9q8h-26 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NO); Thu, 08 Apr 2021 10:39:10 -0700 Received: from rn-mailsvcp-mmp-lapp04.rno.apple.com (rn-mailsvcp-mmp-lapp04.rno.apple.com [17.179.253.17]) 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 <0QR900CZOAD9UM70@rn-mailsvcp-mta-lapp01.rno.apple.com>; Thu, 08 Apr 2021 10:39:09 -0700 (PDT) Received: from process_milters-daemon.rn-mailsvcp-mmp-lapp04.rno.apple.com by rn-mailsvcp-mmp-lapp04.rno.apple.com (Oracle Communications Messaging Server 8.1.0.7.20201203 64bit (built Dec 3 2020)) id <0QR900000A9CV400@rn-mailsvcp-mmp-lapp04.rno.apple.com>; Thu, 08 Apr 2021 10:39:09 -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: 4a5f5338-a9b3-4200-ad6a-e136e9d46efd 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: 293c9cf5-bbc3-4753-b474-c418545031cf X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:6.0.391,18.0.761 definitions=2021-04-08_04:2021-04-08,2021-04-08 signatures=0 Received: from [17.235.44.237] (unknown [17.235.44.237]) by rn-mailsvcp-mmp-lapp04.rno.apple.com (Oracle Communications Messaging Server 8.1.0.7.20201203 64bit (built Dec 3 2020)) with ESMTPSA id <0QR900Z6RAD3YW00@rn-mailsvcp-mmp-lapp04.rno.apple.com>; Thu, 08 Apr 2021 10:39:04 -0700 (PDT) MIME-version: 1.0 (Mac OS X Mail 14.0 \(3654.20.0.2.1\)) Subject: Re: [edk2-devel] [GSoC proposal] Secure Image Loader From: "Andrew Fish" In-reply-to: <2e051761-c7ed-c6c6-e8e6-fb45ba3d0a2d@posteo.de> Date: Thu, 08 Apr 2021 10:39:03 -0700 Cc: edk2-devel-groups-io , Laszlo Ersek , Nate DeSimone , Mike Kinney Message-id: <2B908E95-EF9D-43DA-B31E-CD90C2D8C98D@apple.com> References: <259a114d-7132-1774-d46a-8e8d9b4ff5e2@redhat.com> <8dcae34e-e975-9233-3738-62662201aae9@posteo.de> <00A00172-982E-4989-8AE3-EF390DB4E531@apple.com> <2e051761-c7ed-c6c6-e8e6-fb45ba3d0a2d@posteo.de> To: =?utf-8?Q?Marvin_H=C3=A4user?= 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-08_04:2021-04-08,2021-04-08 signatures=0 Content-type: text/plain; charset=utf-8 Content-transfer-encoding: quoted-printable > On Apr 8, 2021, at 10:02 AM, Marvin H=C3=A4user wro= te: >=20 > On 08.04.21 18:44, Andrew Fish via groups.io wrote: >>=20 >>=20 >>> On Apr 8, 2021, at 9:06 AM, Marvin H=C3=A4user > wrote: >>>=20 >>> We use the loader code in userspace anyway for fuzzing and such. I als= o want to build a database of all sorts of UEFI binaries some time before t= he merge to confirm they are all accepted (Windows / macOS / Linux bootload= ers, tools like memtest, drivers like iPXE). As part of that, I'm sure we c= an have a userspace tool that uses the code to emit parsing information. >>>=20 >>> But as the EDK II build system is very... not so userspace friendly, I= will not promise it will be very nice. :) >>>=20 >>=20 >> Marvin, >>=20 >> The BaseTools can easily build C command line tools that are cross plat= form? >>=20 >> Actually GenFw [1] already does a lot of PE/COFF magic, so it should be= relatively easy to add a -I, =E2=80=94info, and dump out an overview of a = PE/COFF image, and make comments on things that are not secure. It would al= so probably be useful to dump out information about the Debug Directory ent= ries, His sections, etc. for general debug. >=20 > I did not look at the code much, but I do know that BaseTools duplicates= the PE/COFF code from MdePkg. Whether it was changed or not I cannot tell. >=20 GenFw does the ELF to PE/COFF conversion, zeroing out Debug Directory Entr= ies etc. so it should be correct. It is not like the PE/COFF spec is a movi= ng target.=20 Thanks, Andrew Fish > Best regards, > Marvin >=20 >>=20 >> [1] https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/Ge= nFw >> /Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>. edksetup.= sh >> Loading previous configuration from /Volumes/Case/edk2-github/Conf/Buil= dEnv.sh >> WORKSPACE: /Volumes/Case/edk2-github >> EDK_TOOLS_PATH: /Volumes/Case/edk2-github/BaseTools >> CONF_PATH: /Volumes/Case/edk2-github/Conf >> /Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>GenFw -h >> GenFw Version 0.2 Developer Build based on Revision: Unknown >>=20 >> Usage: GenFw [options] >>=20 >> Copyright (c) 2007 - 2018, Intel Corporation. All rights reserved. >>=20 >> Options: >> -o FileName, --outputfile FileName >> File will be created to store the output conten= t. >> -e EFI_FILETYPE, --efiImage EFI_FILETYPE >> Create Efi Image. EFI_FILETYPE is one of BASE,S= MM_CORE, >> PEI_CORE, PEIM, DXE_CORE, DXE_DRIVER, UEFI_APPL= ICATION, >> SEC, DXE_SAL_DRIVER, UEFI_DRIVER, DXE_RUNTIME_D= RIVER, >> DXE_SMM_DRIVER, SECURITY_CORE, COMBINED_PEIM_DR= IVER, >> MM_STANDALONE, MM_CORE_STANDALONE, >> PIC_PEIM, RELOCATABLE_PEIM, BS_DRIVER, RT_DRIVE= R, >> APPLICATION, SAL_RT_DRIVER to support all modul= e types >> It can only be used together with --keepexcepti= ontable, >> --keepzeropending, --keepoptionalheader, -r, -o= option. >> It is a action option. If it is combined with o= ther action options, >> the later input action option will override the= previous one. >> -c, --acpi Create Acpi table. >> It can't be combined with other action options >> except for -o, -r option. It is a action option= . >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> -t, --terse Create Te Image. >> It can only be used together with --keepexcepti= ontable, >> --keepzeropending, --keepoptionalheader, -r, -o= option. >> It is a action option. If it is combined with o= ther action options, >> the later input action option will override the= previous one. >> -u, --dump Dump TeImage Header. >> It can't be combined with other action options >> except for -o, -r option. It is a action option= . >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> -z, --zero Zero the Debug Data Fields in the PE input imag= e file. >> It also zeros the time stamp fields. >> This option can be used to compare the binary e= fi image. >> It can't be combined with other action options >> except for -o, -r option. It is a action option= . >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> -b, --exe2bin Convert the input EXE to the output BIN file. >> It can't be combined with other action options >> except for -o, -r option. It is a action option= . >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> -l, --stripped Strip off the relocation info from PE or TE ima= ge. >> It can't be combined with other action options >> except for -o, -r option. It is a action option= . >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> -s timedate, --stamp timedate >> timedate format is "yyyy-mm-dd 00:00:00". if ti= medata >> is set to NOW, current system time is used. The= support >> date scope is 1970-01-01 00+timezone:00:00 >> ~ 2038-01-19 03+timezone:14:07 >> The scope is adjusted according to the differen= t zones. >> It can't be combined with other action options >> except for -o, -r option. It is a action option= . >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> -m, --mcifile Convert input microcode txt file to microcode b= in file. >> It can't be combined with other action options >> except for -o option. It is a action option. >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> -j, --join Combine multi microcode bin files to one file. >> It can be specified with -a, -p, -o option. >> No other options can be combined with it. >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> -a NUM, --align NUM NUM is one HEX or DEC format alignment value. >> This option is only used together with -j optio= n. >> -p NUM, --pad NUM NUM is one HEX or DEC format padding value. >> This option is only used together with -j optio= n. >> --keepexceptiontable Don't clear exception table. >> This option can be used together with -e or -t. >> It doesn't work for other options. >> --keepoptionalheader Don't zero PE/COFF optional header fields. >> This option can be used together with -e or -t. >> It doesn't work for other options. >> --keepzeropending Don't strip zero pending of .reloc. >> This option can be used together with -e or -t. >> It doesn't work for other options. >> -r, --replace Overwrite the input file with the output conten= t. >> If more input files are specified, >> the last input file will be as the output file. >> -g HiiPackageListGuid, --hiiguid HiiPackageListGuid >> Guid is used to specify hii package list guid. >> Its format is xxxxxxxx-xxxx-xxxx-xxxx-xxxxxxxxx= xxx >> If not specified, the first Form FormSet guid i= s used. >> --hiipackage Combine all input binary hii packages into >> a single package list as the text resource data= (RC). >> It can't be combined with other action options >> except for -o option. It is a action option. >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> --hiibinpackage Combine all input binary hii packages into >> a single package list as the binary resource se= ction. >> It can't be combined with other action options >> except for -o option. It is a action option. >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> --rc FlieName Append a Hii resource section to the >> last PE/COFF section. The FileName is the resou= rce section to append >> If FileName does not exist this operation is sk= ipped. This feature is >> only intended for toolchains, like XCODE, that = don't suport $(RC). >> This option can only be combined with -e >> --rebase NewAddress Rebase image to new base address. New address >> is also set to the first none code section head= er. >> It can't be combined with other action options >> except for -o or -r option. It is a action opti= on. >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> --address NewAddress Set new address into the first none code >> section header of the input image. >> It can't be combined with other action options >> except for -o or -r option. It is a action opti= on. >> If it is combined with other action options, th= e later >> input action option will override the previous = one. >> -v, --verbose Turn on verbose output with informational messa= ges. >> -q, --quiet Disable all messages except key message and fat= al error >> -d, --debug level Enable debug messages, at input debug level. >> --version Show program's version number and exit >> -h, --help Show this help message and exit >>=20 >> Thanks, >>=20 >> Andrew Fish >>=20 >>> Best regards, >>> Marvin >>>=20 >>> 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 t= he security faults with a given PE/COFF file layout. >>>>=20 >>>>=20 >>>>=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 interest= ed! >>>>>>> Completing a formal verification of a PE/COFF loader is certainly >>>>>>> impressive. Was this done with some sort of automated theorem prov= ing? >>>>>>> It would seem a rather arduous task doing an inductive proof for a= n >>>>>>> algorithm like that by hand! >>>>>> I would call it "semi-automated", a great deal of intermediate goal= s >>>>>> (preconditions, postconditions, invariants, assertions, ...) were >>>>>> required to show all interesting properties. But yes, the actual pr= oof >>>>>> steps are automated by common SMT solvers. It was done using the >>>>>> AstraVer Toolset and ACSL, latter basically a language to express l= ogic >>>>>> statements with C-like syntax. >>>>>>=20 >>>>>>> I completely agree with you that getting a formally verified PE/CO= FF >>>>>>> loader into mainline is undoubtably valuable and would pay securit= y >>>>>>> dividends for years to come. >>>>>> 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 to= pic >>>>>>> is writing out proofs for simple algorithms on exams in my Algorit= hms >>>>>>> class in college. Regardless you have a much better idea of what t= he >>>>>>> current status is of the work that you and Vitaly have done. I gue= ss >>>>>>> my only question is do you think there is sufficient work remainin= g to >>>>>>> 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. = While >>>>>> 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 under= lying >>>>>> 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 i= t can >>>>>> be narrowed/widened as you see fit really. This is one of *the* cor= e >>>>>> components used on millions of device, and many package maintainers= need >>>>>> 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 yo= u >>>>>>> believe are needed. >>>>>> 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 a= nd >>>>>>> come back with any questions I still have. >>>>>> Thank you, I will gladly explain anything unclear. Just try to not = give >>>>>> Laszlo too many flashbacks. :) >>>>> I haven't commented yet in this thread, as I thought my stance on th= is >>>>> undertaking was (or should be) obvious. >>>>>=20 >>>>> I very much welcome a replacement for the PE/COFF parser (as I consi= der >>>>> its security issues unfixable in an incremental manner). From my rea= ding >>>>> 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 wi= th >>>>> minimal actual code review. If fixing the pervasive security problem= s >>>>> around this area cannot avoid spiraling out to other core code in ed= k2, >>>>> 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 bes= t >>>>> framework for upstreaming such a large undertaking, but if it can he= lp, >>>>> we should use it as much as possible. >>>>>=20 >>>>> Thanks >>>>> Laszlo >>>>>=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 Er= sek >; 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 w= hile >>>>>>>> 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 ag= ain >>>>>>>> Laszlo >>>>>>>> for your *incredible* review work on the publication part. >>>>>>>>=20 >>>>>>>> I now want to make an effort to mainline it, preferably as part o= f >>>>>>>> the current >>>>>>>> Google Summer of Code event. To be clear, my internship at ISP RA= S has >>>>>>>> concluded, and while Vitaly will be available for design discussi= on, >>>>>>>> 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 t= ake >>>>>>>> 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 U= EFI >>>>>>>> PI and >>>>>>>> UEFI specifications. Changes need to be discussed, settled on, an= d >>>>>>>> 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 fe= w >>>>>>>> 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 fix= ed >>>>>>>> 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 invo= ke >>>>>>>> undefined >>>>>>>> behaviour. >>>>>>>> H. I already managed to identify a malformed image in OVMF with i= ts 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-on= ly data >>>>>>>> segments when enabled. >>>>>>>>=20 >>>>>>>> There are likely more points for both lists, but I hope this give= s a >>>>>>>> decent >>>>>>>> starting point for discussion. What are your thoughts on the matt= er? >>>>>>>> I strongly >>>>>>>> encourage everyone to read the section regarding defects of our >>>>>>>> publication[2] >>>>>>>> to better understand the motivation. The vague points above can o= f >>>>>>>> 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 >>=20 >=20