On 02/05/2017, Youness Alaoui kakaroto@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:
-
Sam Kuper