Re: Verifying Toolchain Semantics

[Mark H Weaver]

Ian Grant <address@hidden> writes:

> On Tue, Oct 7, 2014 at 1:28 PM, Mark H Weaver <address@hidden> wrote:
>> Ian, please stop posting to guile-devel.  You've made your points, and
>> I've even called attention to what I think is the best exposition of
>> your ideas.  At this point you're just repeating yourself and hurling
>> gratuitous insults.  Enough!
>
> Well, it's insulting when you speak to me like a child, and when you
> make childish suggestions about my motives for posting to this list.

I don't see how either of these claims applies to what I wrote above.
I do, however, feel as though you're treating all of us in an extremely
condescending manner.  You're also acting like a bully.

But more relevantly to the points you wish to discuss: you have not
adequately responded to the excellent points by William ML Leslie.
Specifically, he made a persuasive argument that semantic fixed-points
are still vulnerable to variants of the Thompson hack.  You have failed
to explain why this is not the case.

And what about the hardware?  Even setting aside blatant back doors like
Intel ME/AMT, the semantics of our hardware is unknown to us.  In case
you don't know, there's a huge amount of proprietary software running
inside of every mainstream processor, which implements the "machine
code" in terms of a lower level "microcode", and we don't know the
semantics of the microcode either.  The actual hardware designs are
generated by something very analogous to software, written in languages
like Verilog and VHDL.

Personally, I won't have much confidence in our machines until they are
based on free designs all the way down to the physical transistors, and
when we have widely available tools to verify that a physical machine
precisely matches the published designs.  If we must destroy a machine
to verify it, we can still acquire N identical machines and randomly
choose some subset of them to verify.

Now, suppose we accomplish this, and *every* part of the implementation
down to the physical layer was automatically generated from formal
specifications.  FWIW, I think this would be quite satisfactory, but I
still don't understand how you'd know anything at all about the
semantics of the resulting machine, by the standards you've set for us.

The problem you'd then run into is that we cannot be sure what the
physical laws actually are, as you've already pointed out.  But suppose
for the moment that Quantum Electrodynamics (QED) truly is an adequate
theory to model our machine, as I've been led to believe.  We still have
the problems that (1) we lack the means to solve the equations for any
system of non-trivial size, (2) we can't know whether the actual
physical configuration of our machine corresponds to what we've been
told about it to the level relevant to QED, and (3) even if we had
solutions to (1) and (2), we cannot produce a machine that will be
completely reliable, because quantum mechanics only allows us to compute
the *probabilities* of various outcomes.

In summary, given our current understanding of physical law, we have no
way (even in principle) to build a machine that reliably follows our
instructions.

And if you really want to blow your mind, consider that we have no
knowledge whatsoever of whether the "die rolls" in quantum mechanics are
truly random.  All we have is *absence of knowledge* of any discernable
pattern to these die rolls.

For all we know, our entire universe could be running as a simulation
inside of a machine in some other universe, and the beings who control
that simulation are rolling the dice for us.  They could then control
*anything* in our universe that they wish to, simply by selecting the
results of those die rolls in carefully selected situations of
importance.

Or perhaps it's just your own mind that is in a simulator, and all of us
are just puppets designed to perform experiments on you as part of some
evolutionary programming process, to create a better tool for some
larger machine.

The unfortunate fact is that none of us has truly reliable knowledge of
anything at all.  I think you are understandably uncomfortable with
this, and are trying mightily to establish a solid base on which to
stand.  I sympathize with this, believe me, but I think it's impossible,
even in principle.

Anyway, coming back down to the realm of realistic vulnerabilities that
we have any hope of addressing: the truth of the matter is that we'll
have to fix more than just our computers.  We'll have to fix
*ourselves*.  How long do you suppose it will be before it is feasible
for someone to introduce some nanobots into your body somehow -- the
possibilities are nearly endless; I've heard of research into using
mosquitoes, but they could also be introduced by food or water -- and
then using them to rewire your neural connections to change your mind in
potentially arbitrary ways?

> I am responding constructively to questions asked me by a guile
> developer who is also an official representative of the FSF. Will the
> FSF prevent me from doing so on an FSF forum.

I don't think anyone could reasonably claim that we haven't given you
ample freedom to post on our forums.  There are limits, however.

> And if so, will any guile developers respond to the mails I sent
> regarding guile?

I intend to do so, yes.  Please understand that we are very busy people,
and that we are volunteers.

You should also understand that when you post such a large volume of
highly redundant and often gratuitously insulting material, people are
likely to filter you out (mentally if not mechanically), and then
everything you write will be ignored, including posts that are relevant
to practical issues concerning Guile.

> Speaking of which, what is the name and version of the program that
> your emacs uses for "pdf->png" conversion? Your report, blaming me for
> sending bad PDF, indicates a fairly fundamental misunderstanding of
> what a program meant to do when it reads a file that supposed to be in
> a defined format.

Sorry, this was my mistake.  Your blog post included a URL that ended
with ".pdf", so I assumed it would actually be a PDF.  Turns out it was
actually a web page with more links to download the actual PDF.

So, what I had was HTML in a file with a .pdf extension.  The program
that crashed when fed this HTML file was GNU Ghostscript 9.06.0.  I've
since switched to another PDF renderer.

     Mark