Re: Verifying Toolchain Semantics

[Ian Grant]

On Fri, Oct 3, 2014 at 2:23 AM, Mark H Weaver <address@hidden> wrote:
>>     http://livelogic.blogspot.com/2014/10/the-foundation-part-i.html
> I downloaded the PDF linked in that blog entry and attempted to view it
> using Emacs's docview mode, which reported that the pdf->png process
> died with a segfault.

This means that there is a bug in that program. PDF (or ISO 32000) is
a well-defined text file format. See
http://www.adobe.com/devnet/pdf/pdf_reference.html

So no software tools should ever segfault reading a PDF file. Even one
that contained a trojan program. If the software were properly
designed and written then it would be _impossible_ for there to be a
trojan in a PDF file.

> It's ironic that someone who claims to be so concerned with security
> steadfastly refuses to provide his most important essays in a simple,
> transparent format.  Instead, he insists to distribute them in an opaque
> format that can only be interpreted by a small handful of very complex
> programs with a large attack surface.

The "attack surface" is indeed huge, but only because of the shoddy
standards of the software developers who implement it!

> For that matter, it's also interesting that someone concerned about
> Thompson viruses would suggest that Guile should distribute it's
> compiler in the form of pre-compiled intermediate C code (compiled from
> Scheme) instead of bootstrapping from source code, in order to speed up
> the compilation process.

I have already explained why this is an invalid argument. It is also
hypocritical, because the guile source distribution already includes
over 50,000 lines of intermediate shell script. This is unintelligible
(I have tried reading ./configure, there are these functions which
construct strings of 512 backslashes, and stuff like that, and _no_
explanation for why that is necessary!)

On the contrary, the intermediate code I suggest shipping need not
necessarily be unintelligible. It would be very clear, and quite
concise. For an example (in Standard ML) of the sort of
code-generating code I am talking about, see

   http://livelogic.blogspot.com/2014/07/writing-assembler-using-standardml.html

Basically, the inductive structure of the parser and interpreter will
still be very clear in the application of the assembler-generating
primitives. Now Standard ML is nothing much more than than typed
scheme, with a _very_ powerful "module system" which has a sound
formal basis in constructive logic: an ML functor application is
essentiallya formal correctness proof. So we could quite easily
translate Standard ML to scheme, and the generated scheme would be
perfectly readable and auditable.

> I've wasted more time than I should have reading Ian's writings, looking
> for an answer to this apparent contradiction in his views, and I haven't
> found it.

You have indeed wasted your time, because the contradiction is not in
my writing, it's only in your own mind.

> While we're on the subject of paranoid theories, here's one for you:
> maybe Ian Grant's true motive is to induce some of the most important
> developers of free toolchains and the Linux kernel to load PDFs that
> infect their computers with malware, in order to subvert our core
> infrastructure.

Well, if I do succeed in distributing malware, it will be a good
demonstration of what I have been arguing for months now, which is
that your "core infrastructure" is _very,_ _very_ flaky, and that far
from being "the most important developers," you are in fact just
part-time amateur hackers playing at your 'hobbies'.

What I am trying to do here is wake you people up from what will
otherwise prove to be terminal sleep. This is not a hobby, you are
combatants in a global information war, and it will cost some of you
your lives,

> Ian: tell me again, why do you refuse to distribute your essays in plain
> text?  I read GNU Thunder and I don't remember seeing anything in there
> that justifies the use of such a complex format.  As I recall, it's just
> plain text anyway.

I don't distribute plain text because it is too easy to alter. Once I
send one of these "essays" out I have no control over what happens to
it. So I try to make it as hard as I reasonably can for people to edit
what I have written.

If you were "the most important developers" you would be able to write
a program to reliably display PDF.

Ian