Re: [edk2-devel] [GSoC proposal] Secure Image Loader

["Andrew Fish" <afish@apple.com>]

> On Apr 8, 2021, at 10:02 AM, Marvin Häuser <mhaeuser@posteo.de> wrote:
> 
> On 08.04.21 18:44, Andrew Fish via groups.io wrote:
>> 
>> 
>>> On Apr 8, 2021, at 9:06 AM, Marvin Häuser <mhaeuser@posteo.de <mailto:mhaeuser@posteo.de>> wrote:
>>> 
>>> 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 bootloaders, 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.
>>> 
>>> But as the EDK II build system is very... not so userspace friendly, 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, —info, 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 entries, His sections, etc. for general debug.
> 
> 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.
> 

GenFw does the ELF to PE/COFF conversion, zeroing out Debug Directory Entries etc. so it should be correct. It is not like the PE/COFF spec is a moving target. 

Thanks,

Andrew Fish

> Best regards,
> Marvin
> 
>> 
>> [1] https://github.com/tianocore/edk2/tree/master/BaseTools/Source/C/GenFw <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/BuildEnv.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
>> 
>> Usage: GenFw [options] <input_file>
>> 
>> 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_APPLICATION,
>>                         SEC, DXE_SAL_DRIVER, UEFI_DRIVER, DXE_RUNTIME_DRIVER,
>>                         DXE_SMM_DRIVER, SECURITY_CORE, COMBINED_PEIM_DRIVER,
>>                         MM_STANDALONE, MM_CORE_STANDALONE,
>>                         PIC_PEIM, RELOCATABLE_PEIM, BS_DRIVER, RT_DRIVER,
>>                         APPLICATION, SAL_RT_DRIVER to support all module types
>>                         It can only be used together with --keepexceptiontable,
>>                         --keepzeropending, --keepoptionalheader, -r, -o option.
>>                         It is a action option. If it is combined with other 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, the later
>>                         input action option will override the previous one.
>>   -t, --terse           Create Te Image.
>>                         It can only be used together with --keepexceptiontable,
>>                         --keepzeropending, --keepoptionalheader, -r, -o option.
>>                         It is a action option. If it is combined with other 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, the later
>>                         input action option will override the previous one.
>>   -z, --zero            Zero the Debug Data Fields in the PE input image file.
>>                         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 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, the later
>>                         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 later
>>                         input action option will override the previous one.
>>   -s timedate, --stamp timedate
>>                         timedate format is "yyyy-mm-dd 00:00:00". if timedata
>>                         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 different 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, the later
>>                         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 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, the 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 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 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, the 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 section.
>>                         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 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 resource section to append
>>                         If FileName does not exist this operation is skipped. 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 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 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 option.
>>                         If it is combined with other action options, the later
>>                         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
>>> 
>>> 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.
>>>> 
>>>> 
>>>> 
>>>>> On Apr 8, 2021, at 4:16 AM, Laszlo Ersek <lersek@redhat.com <mailto:lersek@redhat.com>> wrote:
>>>>> 
>>>>> On 04/06/21 12:06, Marvin Häuser 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 logic
>>>>>> 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 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 underlying
>>>>>> 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 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 need
>>>>>> 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 you
>>>>>>> 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 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 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.
>>>>> 
>>>>> 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 <mailto:devel@edk2.groups.io> <devel@edk2.groups.io <mailto:devel@edk2.groups.io>> On Behalf Of Marvin
>>>>>>>> Häuser
>>>>>>>> Sent: Sunday, April 4, 2021 4:02 PM
>>>>>>>> To: devel@edk2.groups.io <mailto:devel@edk2.groups.io>; Laszlo Ersek <lersek@redhat.com <mailto:lersek@redhat.com>>; Andrew Fish
>>>>>>>> <afish@apple.com <mailto:afish@apple.com>>; Kinney, Michael D <michael.d.kinney@intel.com <mailto:michael.d.kinney@intel.com>>
>>>>>>>> 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
>>>>>>>> now. :) I'm
>>>>>>>> Marvin Häuser, 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 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
>>>>>>>> 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 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
>>>>>>>> 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 <https://github.com/mhaeuser/ISPRASOpen-SecurePE>
>>>>>>>> [2] https://arxiv.org/pdf/2012.05471.pdf <https://arxiv.org/pdf/2012.05471.pdf>
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>> 
>>>>> 
>>>>> 
>>>>> 
>>> 
>>> 
>>> 
>> 
>> 
>