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

[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.

Sorry abou that, was not something I generally even consider as emacs
handles that bit of tracking for me but I will try to add that in the
future.

> I'm not worried about those languages.  Very little code is written in
> them anyway, only a small part of the early bootstrap.
Yet also the point where the trusting trust attacks can most effectively
be inserted. Hence more concern and less trust needs to be placed there.


> My concern is the correspondence between the source code and machine code for 
> the
> majority of the operating system and applications.
That seems more like a feature request for GCC and guile than the
bootstrap or the trustworthiness of the build farms.

> 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.
Absolutely and we already have dozens of living examples due to
performance optimizations done by GCC and Clang exploiting undefined
behavior in the C language and in some cases violating the spec for sake
of compatibility.

> Such compiler bugs and the resulting exploits could be systematically 
> searched for by
> well-resourced attackers.
And actively exploiting as they are already doing.

> 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.
Very true, we need formally defined languages which do not have
undefined behavior and rigourous tests that prevent optimizations from
violating the spec. In essense a series of acid tests that ensure the
resulting mental model always exactly matches the computing model that
the compilers will be based upon.


> To truly solve that problem, we need bug-free compilers.
Impossible for all but the simplest of languages as the complexity of
implementing a compiler/assembler/interpreter is ln(c)+a but the
complexity of implementing a bug-free compiler/assembler/interpreter is
(e^(c))! - a. Where a is the complexity cost of supporting it's host 
architecture.


> In practice, this requires provably correct compilers.
Which in practice turn out *NOT* to be bug free nor complete in regards
to the standard specification. Now, don't get me wrong; provably correct
compilers are a correct step in the right direction but the real
solution is to first generate simplified languages that don't have
undefined behavior and human model first behavior.

> Does that make sense?
Absolutely, certainly something possible to do; but extremely human
effort intensive and I don't see anyone willing to throw 2+ years of
human effort at the problem outside of non-free Businesses like
CompCert.

I'd love to see someone do it, I'd even throw in a few dollars into a
pot to fund it but it is so low down on my list of priorities, I'm not
going to be touching it in the next 2 decades...

-Jeremiah