From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Mark H Weaver Newsgroups: gmane.comp.gnu.lightning.general,gmane.lisp.guile.devel Subject: Re: Verifying Toolchain Semantics Date: Wed, 08 Oct 2014 14:26:53 -0400 Message-ID: <87zjd6l8nm.fsf@yeeloong.lan> References: <87mw9dfz8l.fsf@netris.org> <20141005065858.GA16595@fencepost.gnu.org> <20141006042323.GA31390@fencepost.gnu.org> <87y4srlrg6.fsf@yeeloong.lan> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1412792876 19755 80.91.229.3 (8 Oct 2014 18:27:56 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 8 Oct 2014 18:27:56 +0000 (UTC) Cc: Mike Gerwitz , Markus Kuhn , lightning , Richard Stallman , guile-devel To: Ian Grant Original-X-From: lightning-bounces+gcglg-lightning=m.gmane.org-mXXj517/zsQ@public.gmane.org Wed Oct 08 20:27:50 2014 Return-path: Envelope-to: gcglg-lightning@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Xbvxl-0006yV-9h for gcglg-lightning@m.gmane.org; Wed, 08 Oct 2014 20:27:49 +0200 Original-Received: from localhost ([::1]:37807 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Xbvxk-0007Qf-UC for gcglg-lightning@m.gmane.org; Wed, 08 Oct 2014 14:27:48 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:36214) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Xbvxc-0007QI-Gp for lightning-mXXj517/zsQ@public.gmane.org; Wed, 08 Oct 2014 14:27:45 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1XbvxW-0003QE-P0 for lightning-mXXj517/zsQ@public.gmane.org; Wed, 08 Oct 2014 14:27:40 -0400 Original-Received: from world.peace.net ([96.39.62.75]:60416) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XbvxR-0003OC-2L; Wed, 08 Oct 2014 14:27:29 -0400 Original-Received: from c-24-62-95-23.hsd1.ma.comcast.net ([24.62.95.23] helo=yeeloong.lan) by world.peace.net with esmtpsa (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.72) (envelope-from ) id 1XbvxG-0003Db-Vo; Wed, 08 Oct 2014 14:27:19 -0400 In-Reply-To: (Ian Grant's message of "Tue, 7 Oct 2014 13:56:21 -0400") User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3.94 (gnu/linux) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 96.39.62.75 X-BeenThere: lightning-mXXj517/zsQ@public.gmane.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: lightning-bounces+gcglg-lightning=m.gmane.org-mXXj517/zsQ@public.gmane.org Original-Sender: lightning-bounces+gcglg-lightning=m.gmane.org-mXXj517/zsQ@public.gmane.org Xref: news.gmane.org gmane.comp.gnu.lightning.general:612 gmane.lisp.guile.devel:17574 Archived-At: Ian Grant writes: > On Tue, Oct 7, 2014 at 1:28 PM, Mark H Weaver 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