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

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

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> 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 <devel@edk2.groups.io> On Behalf Of Marvin
>>>> Häuser
>>>> Sent: Sunday, April 4, 2021 4:02 PM
>>>> To: devel@edk2.groups.io; Laszlo Ersek <lersek@redhat.com>; Andrew Fish
>>>> <afish@apple.com>; Kinney, Michael D <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
>>>> [2] https://arxiv.org/pdf/2012.05471.pdf
>>>> 
>>>> 
>>>> 
>>>> 
>>> 
>>> 
>>> 
>>> 
>>> 
>> 
> 
> 
> 
> 
> 
>