Re: Trustworthiness of build farms (was Re: CDN performance)

[Mark H Weaver]

Hi Jeremiah,

If you could add an "In-Reply-To:" header to your responses, that would
be very helpful.  It's easy to add it manually if needed: just copy the
"Message-ID:" header from the original message and replace "Message-ID:"
with "In-Reply-To:".  As is, it's very difficult for me to keep track of
any conversation with you.

address@hidden writes:

>> 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.
>
> A formal proof would be just one piece used in building layers of trust,
> each of them indpendent and reinforcing of each other like layers of
> kevlar in a bullet proof vest; thus even if some of the layers break,
> the bullet doesn't get in to do damage.

Agreed.

>> However, it's important to note several caveats:
> Of course, we always miss things.
>
>> * 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.
> Well hex2's entire language is:
[...]
> The M1-macro language is even smaller:
[...]

I'm not worried about those languages.  Very little code is written in
them anyway, only a small part of the early bootstrap.  My concern is
the correspondence between the source code and machine code for the
majority of the operating system and applications.

It's important to note that even a relatively obscure bug in the
compiler is enough to create an exploitable bug in the machine code of
compiled programs that's not present in the source code.  Such compiler
bugs and the resulting exploits could be systematically searched for by
well-resourced attackers.

So, if we want to *truly* solve the problem of exploitable bugs existing
only in the machine code and not in the corresponding source, it is not
enough to eliminate the possibility of code deliberately inserted in our
toolchain that inserts trojan horses in other software.

To truly solve that problem, we need bug-free compilers.  In practice,
this requires provably correct compilers.

Does that make sense?

       Mark