[coreboot] Remote security exploit in all 2008+ Intel platforms

[Sam Kuper]

On 02/05/2017, Youness Alaoui <kakaroto at kakaroto.homelinux.net> wrote:
> For actual ME-related work that wasn't done by someone else, I will point
> you to this file :
> https://github.com/kakaroto/purism-playground/blob/master/me_re/romp.c
> That is a full C re-implementation of the ROMP module (the smallest of the
> two modules that me_cleaner does not remove).
> This is the RAPI header it uses :
> https://github.com/kakaroto/purism-playground/blob/master/me_re/rapi.h
> That code is a C reimplementation with every instruction accounted for. It
> has not been compiled (it serves more as a proof of concept/pseudocode,
> although it should probably compile), and it's not meant to generate a
> binary-compatible file (that could be a long term goal to generate binary
> compatible images from C source with official intel-provided images).
> Note that I have done the entire Assembly->C conversion myself
>
> [...]
>
> Ultimately I hope we can get full unsigned code execution running, and full
> auditable C code equivalent of any binary code that gets executed between
> power-on and the exploit/custom code being executed.

Kudos for this work. It would be great to have auditable code running there.

Forgive my noob question, but: why C instead of a safer language or
language subset (e.g. Coq, Agda, Idris, SPARK, Compcert (if you don't
mind the non-free license), or even Go or Rust), especially given how
small yet fundamental that code is to the system?

Within and outside Coreboot, the desire to use safer techniques than C
programming, and the actual shift to using them, is, thankfully,
starting to happen. See:


Nico Huber's use of SPARK for Coreboot graphics:

- https://firmwaresecurity.com/2016/09/20/coreboot-now-supports-ada/


Trammell Hudson's wish for a formally-verifiable Coreboot payload such
as sel4 or CertiKOS:

- https://mail.coreboot.org/pipermail/coreboot/2016-December/082606.html


Ron Minnich points out the advantage of using Go rather than C for u-root:

- https://mail.coreboot.org/pipermail/coreboot/2017-April/083891.html


Quinn Norton's epigram, "C is good for two things: being beautiful and
creating catastrophic 0days in memory management." (N.B. I'm not sure
about the first thing):

- https://medium.com/message/everything-is-broken-81e5f33a24e1


Reasons why Xen should consider taking langsec seriously:

- http://trevorjim.com/deconstructing-xen-snark/