> On Apr 8, 2021, at 10:02 AM, Marvin Häuser <mhaeu...@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 <mhaeu...@posteo.de
>>> <mailto:mhaeu...@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 <ler...@redhat.com
>>>>> <mailto:ler...@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
>>>>>>>> <ler...@redhat.com <mailto:ler...@redhat.com>>; Andrew Fish
>>>>>>>> <af...@apple.com <mailto:af...@apple.com>>; Kinney, Michael D
>>>>>>>> <michael.d.kin...@intel.com <mailto:michael.d.kin...@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>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>
>>>
>>>
>>
>>
>
-=-=-=-=-=-=-=-=-=-=-=-
Groups.io Links: You receive all messages sent to this group.
View/Reply Online (#73874): https://edk2.groups.io/g/devel/message/73874
Mute This Topic: https://groups.io/mt/81853302/21656
Group Owner: devel+ow...@edk2.groups.io
Unsubscribe: https://edk2.groups.io/g/devel/unsub [arch...@mail-archive.com]
-=-=-=-=-=-=-=-=-=-=-=-
