Re: Verifying Toolchain Semantics

[Ian Grant]

Taylan wrote:
> In your PDF analogy, the solution is to write a spurious
> amount of PDF implementations.  Or for C, to implement
> a spurious amount of C compilers.  That is impractical
> because C is complex.

It's not as complex as you might think. In the space of a couple of
months, I wrote what I reckon is 50% of a C interpreter all on my own.
And I have the basis of an abstract language for specifying semantics
as just sets of term-rewriting rules, which work on AST
representations of program source.

https://github.com/IanANGrant/red-october/blob/master/src/dynlibs/ffi/CPPLexer.lex
https://github.com/IanANGrant/red-october/blob/master/src/dynlibs/ffi/CParser.grm
https://github.com/IanANGrant/red-october/blob/master/src/dynlibs/ffi/CSyntax.sml

> What might be practical might be to write one new C
> compiler (guaranteed clean, since it's new), and verify
> GCC with that[*].

It will take a year or so to get a C compiler written in C working. So
it won't be new once you've got it to the point of being able to
compile GCC. And by the time that happens, if there has been a
compiler trap door, then the GCC binaries, and probably your "new" C
compiler binaries would "know about" each other. So you would not have
any more reason to believe the
new binaries are good than you had at the beginning. You will have
wasted a year.

> What's more useful in the
> long term is to define a much simpler language, and base
> our everything on that instead of on C.  Then we can verify
> our toolchain more often, since we needn't write a whole
> freaking C compiler every time. :-)

Almost, but that "Much Simpler Language" needs to be one designed to
write language interpreters by reading abstract specifications of the
syntax and semantics from "metadata" files. Then a standard
"interpreter interpreter for the 'MSL'" can be defined to do this job
automatically, and it could even implement itself. See the Reynolds'
paper I referenced in my first reply to William.

Then we will be able to write "a spurious number of whole freakin' C
interpreters" So for example, as I said to Richard a month ago, we
will be able to implement a C compiler in Microsoft Word BASIC, or in
COBOL, and that will be capable of compiling GCC, if we had a year or
so to wait while it does it ... but it could still be capable of
compiling checksumming programs, or diff programs, or unzipping
programs, and these would be extra data points to check whether other
tools like binary file viewers etc, have been compromised by a
compiler trap door.

Ian