Re: GNU Thunder

[William ML Leslie]

On 6 September 2014 11:40, Ian Grant <address@hidden> wrote:
> The problem is this: it is impossible to bootstrap the GNU tool-chain from
> scratch because it's all written in C, and C is too complex a language to
> use for a definitional interpreter. So we always rely on the semantics
> determined by some C compiler binary, which semantics is what you call an
> imponderable.

Actually, I think GCC is quite remarkable as a semantic fixpoint.  As
someone interested in runtime implementation, I'd poked around in GCC
a bunch of times for different reasons without ever comprehending how
it really /worked/.  After reading the Moxie Project blog, I had a
very different opinion.  The blog explained that porting GCC to an
architecture involves, among other things, writing an interpreter for
the target platform (for gdb to use) in C, as well as providing
instructions for GCC to lower into.  So, in a sense, GCC has a number
of semantic fixed points, one per platform.

Incidentally, I don't think semantic fixpoints are sufficient to
protect you from this crack.  As you mentioned, it is possible to
compromise the system's hash functions, file open operations, and exec
server in such a way that you're lied to whenever you ask questions
that could reveal the difference.  The inelegant form of the crack,
manifesting itself in the object files, may be easy enough to discover
via disassembly on another box.  If that is all you're trying to
defend against, verified compilers already get you there.
Unfortunately there are no Free Software verified C compilers, but
there could be I guess.

The more complicated form of the crack - where several system
functions are compromised - is much harder to detect.  There is one
way I know about, namely using the amount of storage space on the
system as a means to ensure that there is nothing you've missed.  That
is, fill up all but a few kilobytes of the system with data that you
can read back out and verify.  Modern systems include so many caches
that such detection would require you to run such a check directly off
the hard disk controller or so (even many of these have enough RAM to
boot a small GNU/Linux system) if you wanted to have real assurance.

> What we need is a language with a simple semantics for which we can write
> interpreters from scratch. It will be slow, but that doesn't matter. All we
> need it for is to generate the reference compiler that we know is secure,
> and the reference tools that we use to verify that the object code produced
> by the full 740 MB of GCC source when compiled by the 74MB gcc binaries, is
> the same object code our reference compiler produces.

As an aside:  this has always been a little fantasy of mine (and I
know I'm not alone).  I've written little lisps in all sorts of
languages (including C and m68k assembler), ostensibly to experiment
with different optimisations or kill time on a train trip, but
secretly to prove to myself that if I ever find I am in some
twighlight-zone situation where I'm a child in the early 90's again
and *this time* I can really convince my parents to buy me a computer,
I can bootstrap myself up from machine code if need be (:

> Now I think we can do this with GNU Guile and GNU Lightning. What we need is
> the semantics of lightning to be defined as program data: so we define the
> expansions of the lightning primitives as assembler in the various target
> architectures, and we formally define the mapping the instruction encoders
> for the various architectures use to map assembler to binary machine code
> instructions. Then we can automatically generate lightning assemblers in any
> source language for which we need it.

Ok, that's a cool idea.  You're a pretty decent hacker, you should do
it.  I'm busy with other things.

>From a security point of view, I'm now slowly working toward verified
runtimes (including verified JIT), replacing C as the low-level
language de jure, and a verified kernel for GNU.  My opinion that
these were TRT to do *next* formed over many years, and only slowly it
became clear to me that they are possible (if a lifetime of train
trips in length).

There are other opinions, and many problems to be solved.  I don't
think they are invalid.

> Now do you think this is pie in the sky, and "an interesting subject for
> research." If so, then why don't you explain to us all _why_ it is that you
> think that?

Of the many things that we can do to make things better for software
developers, you have one idea.  Please understand that our lack of
enthusiasm for it is not without our own individual commitments to the
security and freedoms of users; rather while the extra assurances your
project may provide sound nice, they are frankly rather minimal and
don't have much additional utility, and so are not priority one.

-- 
William Leslie

Notice:
Likely much of this email is, by the nature of copyright, covered
under copyright law.  You absolutely MAY reproduce any part of it in
accordance with the copyright law of the nation you are reading this
in.  Any attempt to DENY YOU THOSE RIGHTS would be illegal without
prior contractual agreement.