From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from rn-mailsvcp-ppex-lapp44.apple.com (rn-mailsvcp-ppex-lapp44.apple.com [17.179.253.48]) by mx.groups.io with SMTP id smtpd.web08.410.1617900256230987129 for ; Thu, 08 Apr 2021 09:44:16 -0700 Authentication-Results: mx.groups.io; dkim=pass header.i=@apple.com header.s=20180706 header.b=GW1yBBVx; spf=pass (domain: apple.com, ip: 17.179.253.48, mailfrom: afish@apple.com) Received: from pps.filterd (rn-mailsvcp-ppex-lapp44.rno.apple.com [127.0.0.1]) by rn-mailsvcp-ppex-lapp44.rno.apple.com (8.16.1.2/8.16.1.2) with SMTP id 138Ggl0V009888; Thu, 8 Apr 2021 09:44:15 -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=dJn1u78bPa3sveB2Bg2JgQ+oHhU8GtybYti3Qjd52Yc=; b=GW1yBBVxY2Y3CyEiUxcMcEvmCfKzGi+ieIdWxWQkCg6oFLyVqnEYqumirNbIFOVRaJ6V GCThLom+0gtG0/EDpM+WE5sA1c/rbR4yqdk74mXYnrSonOQBDJ0vIRkztI9i1rGh829m gOZ8MMnsi0usRRoFy4vFgU4WHtn05uK5tSOmFwjDPBK7Abd7RnxxI0GfDjf2jec3qVq0 7I5UVroJCdza2klWhAYvdYeJbScVPK3NjKtRmx4XyqPp9vAPZSuUuj6Fz+4JrGsT8iXA bAFw5iH3ohwQwFXUw2NlOTSiPmDKab6CKeObr0fbRues6sHvpotK10piyyj4rOTi8zD1 eA== Received: from rn-mailsvcp-mta-lapp02.rno.apple.com (rn-mailsvcp-mta-lapp02.rno.apple.com [10.225.203.150]) by rn-mailsvcp-ppex-lapp44.rno.apple.com with ESMTP id 37rvcm3cd6-1 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128 verify=NO); Thu, 08 Apr 2021 09:44:15 -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-lapp02.rno.apple.com (Oracle Communications Messaging Server 8.1.0.7.20201203 64bit (built Dec 3 2020)) with ESMTPS id <0QR9010GH7TRW130@rn-mailsvcp-mta-lapp02.rno.apple.com>; Thu, 08 Apr 2021 09:44:15 -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 <0QR9000007SAWF00@rn-mailsvcp-mmp-lapp04.rno.apple.com>; Thu, 08 Apr 2021 09:44:15 -0700 (PDT) X-Va-A: X-Va-T-CD: 9ad46be6e1c3c1a24e92ea4dad46d58d X-Va-E-CD: 6a647426990f4fc248f9d9721cb161d4 X-Va-R-CD: 0ee6c4a95a2e1248d03989c9ba42fe98 X-Va-CD: 0 X-Va-ID: 9531ecaa-66ad-421a-8377-87107cca7181 X-V-A: X-V-T-CD: 9ad46be6e1c3c1a24e92ea4dad46d58d X-V-E-CD: 6a647426990f4fc248f9d9721cb161d4 X-V-R-CD: 0ee6c4a95a2e1248d03989c9ba42fe98 X-V-CD: 0 X-V-ID: 22e362f4-8450-482b-b91b-52853dac3f5c 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 [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 <0QR900BOU7TPOD00@rn-mailsvcp-mmp-lapp04.rno.apple.com>; Thu, 08 Apr 2021 09:44:15 -0700 (PDT) From: "Andrew Fish" Message-id: <00A00172-982E-4989-8AE3-EF390DB4E531@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: Thu, 08 Apr 2021 09:44:13 -0700 In-reply-to: <8dcae34e-e975-9233-3738-62662201aae9@posteo.de> Cc: Laszlo Ersek , Nate DeSimone , Mike Kinney To: edk2-devel-groups-io , =?utf-8?Q?Marvin_H=C3=A4user?= References: <259a114d-7132-1774-d46a-8e8d9b4ff5e2@redhat.com> <8dcae34e-e975-9233-3738-62662201aae9@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-08_04:2021-04-08,2021-04-08 signatures=0 Content-type: multipart/alternative; boundary="Apple-Mail=_8B441E26-92A9-42CC-BD08-9075A1B89731" --Apple-Mail=_8B441E26-92A9-42CC-BD08-9075A1B89731 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 > On Apr 8, 2021, at 9:06 AM, Marvin H=C3=A4user wrot= e: >=20 > We use the loader code in userspace anyway for fuzzing and such. I also = want to build a database of all sorts of UEFI binaries some time before the= merge to confirm they are all accepted (Windows / macOS / Linux bootloader= s, tools like memtest, drivers like iPXE). As part of that, I'm sure we can= 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 w= ill not promise it will be very nice. :) >=20 Marvin, The BaseTools can easily build C command line tools that are cross platfor= m? Actually GenFw [1] already does a lot of PE/COFF magic, so it should be re= latively 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 also = probably be useful to dump out information about the Debug Directory entrie= s, His sections, etc. for general debug. [1] https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/GenFw /Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>. edksetup.sh Loading previous configuration from /Volumes/Case/edk2-github/Conf/BuildEn= v.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] Copyright (c) 2007 - 2018, Intel Corporation. All rights reserved. Options: -o FileName, --outputfile FileName File will be created to store the output content. -e EFI_FILETYPE, --efiImage EFI_FILETYPE Create Efi Image. EFI_FILETYPE is one of BASE,SMM_= CORE, PEI_CORE, PEIM, DXE_CORE, DXE_DRIVER, UEFI_APPLICA= TION, SEC, DXE_SAL_DRIVER, UEFI_DRIVER, DXE_RUNTIME_DRIV= ER, DXE_SMM_DRIVER, SECURITY_CORE, COMBINED_PEIM_DRIVE= R, MM_STANDALONE, MM_CORE_STANDALONE, PIC_PEIM, RELOCATABLE_PEIM, BS_DRIVER, RT_DRIVER, APPLICATION, SAL_RT_DRIVER to support all module t= ypes It can only be used together with --keepexceptiont= able, --keepzeropending, --keepoptionalheader, -r, -o op= tion. It is a action option. If it is combined with othe= r action options, the later input action option will override the pr= evious 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, the l= ater input action option will override the previous one= . -t, --terse Create Te Image. It can only be used together with --keepexceptiont= able, --keepzeropending, --keepoptionalheader, -r, -o op= tion. It is a action option. If it is combined with othe= r action options, the later input action option will override the pr= evious 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, the l= ater input action option will override the previous one= . -z, --zero Zero the Debug Data Fields in the PE input image f= ile. It also zeros the time stamp fields. This option can be used to compare the binary efi = 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, the l= ater 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, the l= ater input action option will override the previous one= . -l, --stripped Strip off the relocation info from PE or TE 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, the l= ater input action option will override the previous one= . -s timedate, --stamp timedate timedate format is "yyyy-mm-dd 00:00:00". if timed= ata=20 is set to NOW, current system time is used. The su= pport date scope is 1970-01-01 00+timezone:00:00 ~ 2038-01-19 03+timezone:14:07 The scope is adjusted according to the different z= ones. 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, the l= ater input action option will override the previous one= . -m, --mcifile Convert input microcode txt file to microcode bin = 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, the l= ater 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, the l= ater 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 option. -p NUM, --pad NUM NUM is one HEX or DEC format padding value. This option is only used together with -j option. --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 content. 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-xxxxxxxxxxxx If not specified, the first Form FormSet guid is u= sed. --hiipackage Combine all input binary hii packages into=20 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, the l= ater input action option will override the previous one= . --hiibinpackage Combine all input binary hii packages into=20 a single package list as the binary resource secti= on. 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, the l= ater 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 resource= section to append If FileName does not exist this operation is skipp= ed. 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=20 is also set to the first none code section header. It can't be combined with other action options except for -o or -r option. It is a action option. If it is combined with other action options, the l= ater input action option will override the previous one= . --address NewAddress Set new address into the first none code=20 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 option. If it is combined with other action options, the l= ater input action option will override the previous one= . -v, --verbose Turn on verbose output with informational messages= . -q, --quiet Disable all messages except key message and fatal = 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 Thanks, Andrew Fish > 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 the= security faults with a given PE/COFF file layout. >>=20 >> Sent from my iPhone >>=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 provin= g? >>>>> 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 proo= f >>>> steps are automated by common SMT solvers. It was done using the >>>> AstraVer Toolset and ACSL, latter basically a language to express log= ic >>>> 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. >>>> 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 topi= c >>>>> is writing out proofs for simple algorithms on exams in my Algorithm= s >>>>> 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? >>>> 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. Wh= ile >>>> 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 underly= ing >>>> 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), a= nd >>>> so on. I was rather worried the scope is too broad time-wise, but it = can >>>> be narrowed/widened as you see fit really. This is one of *the* core >>>> components used on millions of device, and many package maintainers n= eed >>>> to review and validate the changes, this must really be done right th= e >>>> first try. :) >>>>=20 >>>>> Certainly we can use some of that time to perform the code reviews y= ou >>>>> 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. >>>>=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. >>>> Thank you, I will gladly explain anything unclear. Just try to not gi= ve >>>> 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. >>>=20 >>> I very much welcome a replacement for the PE/COFF parser (as I conside= r >>> its security issues unfixable in an incremental manner). From my readi= ng >>> 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 >>>>> With Best Regards, >>>>> Nate >>>>>=20 >>>>>> -----Original Message----- >>>>>> From: devel@edk2.groups.io On Behalf Of Marv= in >>>>>> 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 whi= le >>>>>> 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] du= e >>>>>> to various >>>>>> defects we outlined in the corresponding paper. Thank you once agai= n >>>>>> 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 ha= ve >>>>>> 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 tak= e >>>>>> 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 UEF= I >>>>>> 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 ma= y >>>>>> 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 i= n >>>>>> 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 b= oot >>>>>> 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 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 --Apple-Mail=_8B441E26-92A9-42CC-BD08-9075A1B89731 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8

On Apr 8, 20= 21, at 9:06 AM, Marvin H=C3=A4user <mhaeuser@posteo.de> wrote:

= We use the loader code in userspace anyway for fuzzing and such. I also wan= t to build a database of all sorts of UEFI binaries some time before the me= rge to confirm they are all accepted (Windows / macOS / Linux bootloaders, = tools like memtest, drivers like iPXE). As part of that, I'm sure we can ha= ve a userspace tool that uses the code to emit parsing information.<= br style=3D"caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 1= 2px; font-style: normal; font-variant-caps: normal; font-weight: normal; le= tter-spacing: normal; text-align: start; text-indent: 0px; text-transform: = none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0p= x; text-decoration: none;" class=3D"">
But as the EDK II build system is very... not so userspace friendl= y, I will not promise it will be very nice. :)

=

Marvin,

= The BaseTools can easily build C command line tools that are cross platform= ?

Actually GenFw [1] already does a lot= of PE/COFF magic, so it should be relatively easy to add a -I, =E2=80=94in= fo, and dump out an overview of a PE/COFF image, and make comments on thing= s that are not secure. It would also probably be useful to dump out informa= tion about the Debug Directory entries, His sections, etc. for general debu= g.

/Volumes/Case/edk2-github(eng/PR-557-XcodeResourceSections)>. edksetup.sh
Loading previous configuration from /Volumes= /Case/edk2-github/Conf/BuildEnv.sh
WORKSPACE: /Volumes/Case/edk2-github
EDK_TOOLS_PATH: /Volumes/Case/edk2-github/BaseToo= ls
CONF_PATH: /Volumes/= Case/edk2-github/Conf
/Volumes/Case/edk2-github(eng/PR= -557-XcodeResourceSections)>GenFw = -h
GenFw Version 0.2 De= veloper Build based on Revision: Unknown 

Usage: GenFw [options] <input_file>= ;

Copyright = (c) 2007 - 2018, Intel Corporation. All rights reserved.

<= /div>
Options:
  -o FileName, --outputfile FileName
      &nbs= p;                 File will be cre= ated to store the output content.
  -e EFI_FILETYPE, --efiImage EFI_FILETYPE
          &nbs= p;             Create Efi Image. EFI_FILETYPE= is one of BASE,SMM_CORE,
                    &n= bsp;   PEI_CORE, PEIM, DXE_CORE, DXE_DRIVER, UEFI_APPLICATION,<= /div>
        &n= bsp;               SEC, DXE_SAL_DRIVER, = UEFI_DRIVER, DXE_RUNTIME_DRIVER,
                  &n= bsp;     DXE_SMM_DRIVER, SECURITY_CORE, COMBINED_PEIM_DRIVER,
       = ;                 MM_STANDALONE, MM= _CORE_STANDALONE,
<= span style=3D"font-variant-ligatures: no-common-ligatures" class=3D""> = ;                     &nb= sp; PIC_PEIM, RELOCATABLE_PEIM, BS_DRIVER, RT_DRIVER,
            &n= bsp;           APPLICATION, SAL_RT_DRIVER to suppo= rt all module types
&nb= sp;                     &= nbsp; It can only be used together with --keepexceptiontable,
<= div style=3D"margin: 0px; font-stretch: normal; font-size: 11px; line-heigh= t: normal; font-family: Menlo;" class=3D"">          &= nbsp;             --keepzeropending, --keepop= tionalheader, -r, -o option.
                   = ;     It is a action option. If it is combined with other action = options,
    =                     the l= ater input action option will override the previous one.
  -c, --acpi      &nb= sp;     Create Acpi table.
                 = ;       It can't be combined with other action options
        =                 except for -o, -r o= ption. It is a action option.
                   = ;     If it is combined with other action options, the later
       =                 input action optio= n will override the previous one.
  -t, --terse           Create Te = Image.
    =                     It ca= n only be used together with --keepexceptiontable,
            &n= bsp;           --keepzeropending, --keepoptionalhe= ader, -r, -o option.
&n= bsp;                     =   It is a action option. If it is combined with other action options,<= /span>
      &n= bsp;                 the later inpu= t 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.
                    &n= bsp;   If it is combined with other action options, the later
        &nb= sp;               input action option wi= ll override the previous one.
  -z, --zero            Zero the = Debug Data Fields in the PE input image file.
              &nb= sp;         It also zeros the time stamp fields.=
        &= nbsp;               This option can be u= sed to compare the binary efi image.
                 = ;       It can't be combined with other action options
        =                 except for -o, -r o= ption. It is a action option.
                   = ;     If it is combined with other action options, the later
       =                 input action optio= n will override the previous one.
  -b, --exe2bin         Convert the inp= ut EXE to the output BIN file.
                  &nbs= p;     It can't be combined with other action options
         =               except for -o, -r option.= It is a action option.
                    &n= bsp;   If it is combined with other action options, the later
        &nb= sp;               input action option wi= ll override the previous one.
  -l, --stripped        Strip off the reloc= ation info from PE or TE image.
                  &nb= sp;     It can't be combined with other action options
         = ;               except for -o, -r option= . It is a action option.
                    &n= bsp;   If it is combined with other action options, the later
        &nb= sp;               input action option wi= ll override the previous one.
  -s timedate, --stamp timedate
               = ;         timedate format is "yyyy-mm-dd 00:00:00". if = timedata 
  &= nbsp;                    = is set to NOW, current system time is used. The support
           =             date scope is 1970-01-01 00+time= zone:00:00
   = ;                     ~ 2= 038-01-19 03+timezone:14:07
                   = ;     The scope is adjusted according to the different zones.
       = ;                 It can't be combi= ned with other action options
                   = ;     except for -o, -r option. It is a action option.
         = ;               If it is combined with o= ther action options, the later
                  &nbs= p;     input action option will override the previous one.=
  -m, --mcifile   &= nbsp;     Convert input microcode txt file to microcode bin file.=
      &= nbsp;                 It can't be c= ombined with other action options
                  &= nbsp;     except for -o option. It is a action option.
         = ;               If it is combined with o= ther action options, the later
                  &nbs= p;     input action option will override the previous one.=
  -j, --join   = ;         Combine multi microcode bin files to one file= .
      =                   It can be sp= ecified with -a, -p, -o option.
                  &nb= sp;     No other options can be combined with it.
          &nb= sp;             If it is combined with other = action options, the later
                    &n= bsp;   input action option will override the previous one.
  -a NUM, --align NUM   = NUM is one HEX or DEC format alignment value.
              &nb= sp;         This option is only used together with -j o= ption.
  -p NUM,= --pad NUM     NUM is one HEX or DEC format padding value.=
        &= nbsp;               This option is only = used together with -j option.
  --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.
                  &n= bsp;     This option can be used together with -e or -t.
        &nb= sp;               It doesn't work for ot= her options.
  --k= eepzeropending     Don't strip zero pending of .reloc.
         = ;               This option can be used = together with -e or -t.
                    &n= bsp;   It doesn't work for other options.
  -r, --replace         Ov= erwrite the input file with the output content.
              &= nbsp;         If more input files are specified,=
        &= nbsp;               the last input file = will be as the output file.
  -g HiiPackageListGuid, --hiiguid HiiPackageListGuid
        &nbs= p;               Guid is used to specify= hii package list guid.
                    &n= bsp;   Its format is xxxxxxxx-xxxx-xxxx-xxxx-xxxxxxxxxxxx
=
          =               If not specified, the firs= t Form FormSet guid is used.
  --hiipackage          Combine all in= put binary hii packages into 
                  =       a single package list as the text resource data(RC).
      &nb= sp;                 It can't be com= bined with other action options
                  &nb= sp;     except for -o option. It is a action option.
=
          =               If it is combined with oth= er action options, the later
                   = ;     input action option will override the previous one.<= /div>
  --hiibinpackage   =     Combine all input binary hii packages into 
=
          =               a single package list as t= he binary resource section.
                   = ;     It can't be combined with other action options
=
          =               except for -o option. It i= s a action option.
= &nbs= p;                     &n= bsp; If it is combined with other action options, the later
          &nb= sp;             input action option will over= ride the previous one.
  --rc FlieName         Append a Hii resource s= ection to the
  &n= bsp;                     = last PE/COFF section. The FileName is the resource section to append=
        &= nbsp;               If FileName does not= exist this operation is skipped. This feature is
             =           only intended for toolchains, like XCOD= E, that don't suport $(RC).
                   = ;     This option can only be combined with -e
  --rebase NewAddress   Rebase = image to new base address. New address 
              &nbs= p;         is also set to the first none code section h= eader.
    =                     It ca= n't be combined with other action options
                =         except for -o or -r option. It is a action opti= on.
     = ;                   If it is c= ombined with other action options, the later
              &nbs= p;         input action option will override the previo= us one.
  --addre= ss NewAddress  Set new address into the first none code 
        &nb= sp;               section header of the = input image.
  &nb= sp;                     I= t can't be combined with other action options
              &nb= sp;         except for -o or -r option. It is a action = option.
    =                     If it= is combined with other action options, the later
             =           input action option will override the p= revious one.
  -v,= --verbose         Turn on verbose output with informat= ional messages.
  = -q, --quiet           Disable all messages except = key message and fatal error
  -d, --debug level     Enable debug messages, at inp= ut debug level.
  = --version             Show program's version = number and exit
  = -h, --help            Show this help message = and exit

Tha= nks,

Andrew Fish

Best regards,
Marvin

On = 08.04.21 16:13, Andrew (EFI) Fish wrote:
At a minimum it would be nice if we had a to= ol that would point out the security faults with a given PE/COFF file layou= t.



On Apr 8, 2021, at 4:16 AM, Laszlo Ersek <lersek@redhat.com> wrote:<= br class=3D"">
=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 welco= me back! Glad you hear you are interested!
Completing a forma= l verification of a PE/COFF loader is certainly
impressive. W= as 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
(pre= conditions, 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 ex= press logic
statements with C-like syntax.

I completely agree with you= that getting a formally verified PE/COFF
loader into mainlin= e is undoubtably valuable and would pay security
dividends fo= r years to come.
I'm glad to hear that. :)

Admittedly, th= is is an area of computer science that I don't have a
great d= eal 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 d= one. I guess
my only question is do you think there is suffic= ient work remaining to
fill the 10 week GSoC development wind= ow?
Please don't get me wrong, but I would be su= rprised if the UEFI
specification changes I'd like to discuss= alone would be completed
within 10 weeks, let alone implemen= tation throughout the codebase. While
I think the plain amoun= t of code may be a bit less than say a
MinPlatform port, the = changes are much deeper and require much more
caution to avoi= d regressions (e.g. by invalidating undocumented
assertions).= This sadly is not a matter of just replacing the underlying
= library implementation or "plug-in and play" at all. It furthermore
affects many parts of the stack, the core dispatchers used for allplatforms, image emulation (EBC), UEFI userland emulation (Emu= Pkg), and
so on. I was rather worried the scope is too broad = time-wise, but it can
be narrowed/widened as you see fit real= ly. This is one of *the* core
components used on millions of = device, and many package maintainers need
to review and valid= ate the changes, this must really be done right the
first try= . :)

Cert= ainly 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<= br class=3D"">believe are needed.
I believed tha= t 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 mor= e closely and
come back with any questions I still have.
Thank you, I will gladly explain anything unclear. J= ust try to not give
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 p= arser (as I consider
its security issues unfixable in an incr= emental manner). From my reading
of Marvin's and Vitaly's pap= er (draft), they have my full trust, and I'm
ready to put the= ir upcoming code to use in ArmVirtPkg and OvmfPkg with
minima= l actual code review. If fixing the pervasive security problems
around this area cannot avoid spiraling out to other core code in edk2,<= br class=3D"">such as dispatchers, and even to the PI / UEFI specs, so be i= t.

Regarding GSoC itself: as I stated elsewher= e previously, I support
edk2's participation in GSoC, while a= t the same time I'm not
volunteering for mentorship at all. I= 'm uncertain if GSoC is the best
framework for upstreaming su= ch a large undertaking, but if it can help,
we should use it = as much as possible.

Thanks
Lasz= lo





With Best Regards,
Nate

-----Original Message-----
From: devel@e= dk2.groups.io <de= vel@edk2.groups.io> On Behalf Of Marvin
H=C3=A4userSent: Sunday, April 4, 2021 4:02 PM
To: devel@edk2.groups.io; Lasz= lo Ersek <lersek@redhat.= com>; Andrew Fish
<afish@apple.com>; Kinney, Michael D <michael.d.kinney@intel.com&g= t;
Subject: [edk2-devel] [GSoC proposal] Secure Image Loader<= br class=3D"">
Good day everyone,

I'll keep the introduction brief because I've been around for a while
now. :) I'm
Marvin H=C3=A4user, a third-year Compu= ter Science student from TU
Kaiserslautern,
Ger= many. Late last year, my colleague Vitaly from ISP RAS and me
introduced a
formally verified Image Loader for UEFI usage a= t ISP RAS Open[1] due
to various
defects we out= lined 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, pr= eferably as part of
the current
Google Summer o= f Code event. To be clear, my internship at ISP RAS has
concl= uded, and while Vitaly will be available for design discussion,
he has other
priorities at the moment and the practical pa= rt will be on me. I have
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 cons= umed 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
protocol= s (e.g.
returning data with no corresponding size) originatin= g from the UEFI
PI and
UEFI specifications. Cha= nges need to be discussed, settled on, and
submitted to
the UEFI Forum.
4. Some UEFI APIs like the Security = Architecture protocols are
inconveniently
abstr= act, see 5.
5. Some of the current code does not use the exis= ting context, or
accesses it
outside of the exp= osed 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 con= siderations:
A. The Image Loader is mostly formally verified,= and only very few
changes will
be required fro= m the last proven state. This gives a lot of trust in
its cor= rectness
and safety.
B. All outlined defects th= at are of critical nature have been fixed
successfully.
C. The Image Loader has been tested with real-world code loadingreal-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
p= otentially unsafe operations.
E. Centralising and reduced par= se 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 invok= e
undefined
behaviour.
H. I alrea= dy 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 pl= an 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
decentstarting point for discussion. What are your thoughts on the m= atter?
I strongly
encourage everyone to read th= e 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://a= rxiv.org/pdf/2012.05471.pdf






<= br class=3D"">







--Apple-Mail=_8B441E26-92A9-42CC-BD08-9075A1B89731--