Trustworthiness of build farms (was Re: CDN performance)

[Mark H Weaver <mhw@netris.org>]

Hi Giovanni,

Giovanni Biscuolo <g@xelera.eu> writes:

> Mark H Weaver <mhw@netris.org> writes:
>
>> Giovanni Biscuolo <g@xelera.eu> writes:
>>> with a solid infrastructure of "scientifically" trustable build farms,
>>> there are no reasons not to trust substitutes servers (this implies
>>> working towards 100% reproducibility of GuixSD)
>>
>> What does "scientifically trustable" mean?
>
> I'm still not able to elaborate on that (working on it, a sort of
> self-research-hack project) but I'm referencing to this message related
> to reduced bootstrap tarballs:
>
>   https://lists.gnu.org/archive/html/guix-devel/2018-11/msg00347.html
>
> and the related reply by Jeremiah (unfortunately cannot find it in
> archives, Message-ID: <877eh81tm4.fsf@ITSx01.pdp10.guru>)
>
> in particular Jeremiah replied this:
>
>> so, if I don't get it wrong, every skilled engineer will be able to
>> build an "almost analogic" (zero bit of software preloaded) computing
>> machine ad use stage0/mes [1] as the "metre" [2] to calibrate all other
>> computing machines (thanks to reproducible builds)?
>
> well, I haven't thought of it in those terms but yes I guess that is one
> of the properties of the plan.
>
>
> and
>
>> so, having the scientific proof that binary conforms to source, there
>> will be noo need to trust (the untrastable)
>
> Well, that is what someone else could do with it but not a direct goal
> of the work.
>
> maybe a more correct definition of the above "scientific proof" should be
> "mathematical proof"

I agree that a mathematical proof is what we should be aiming for, and
the only kind of proof that I could trust in, in this scenario.

However, it's important to note several caveats:

* A mathematical proof showing that the binary conforms to the source
  requires a proof of correctness of the language implementation, which
  in turn requires formal semantics for both the source language and the
  underlying machine code.  As far as I know, the current
  bootstrappable.org effort does not include anything like this.
  Existing projects that provide this include CakeML and Jitawa.

* One must assume that the hardware behaves according to its formal
  specification.  The veracity of this assumption is not something we
  can currently verify, and even if we could, it would be invalidated if
  someone gained physical access to the machine and modified it.

* The hardware initialization program (e.g. coreboot) and the kernel
  used to perform the bootstrap must still be trusted, and unless I'm
  mistaken, the bootstrappable.org effort does not currently address
  these issues.

* The software running on the substitute servers could be compromised by
  stealing SSH keys from someone with root access.

* If the private signing key of the substitute server can be stolen,
  e.g. by gaining physical access to the machine for a short time, then
  a man-in-the-middle can deliver to users compromised binaries that
  appear to come from the substitute server itself.

* Not only the substitute server, but also all of its build slaves, must
  be trusted as well.

So, while I certainly agree that it will be a *major* improvement to
avoid the need to blindly trust precompiled bootstrap binaries, we
should be clear that the current efforts fall far short of a proof, and
there still remain several valid reasons not to place one's trust in
substitute servers.

Does that make sense?

    Regards,
      Mark