From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Ian Grant Newsgroups: gmane.comp.gnu.lightning.general,gmane.lisp.guile.devel Subject: Re: GNU Thunder Date: Fri, 5 Sep 2014 21:40:16 -0400 Message-ID: References: NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============0597645743584253746==" X-Trace: ger.gmane.org 1409967635 11172 80.91.229.3 (6 Sep 2014 01:40:35 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sat, 6 Sep 2014 01:40:35 +0000 (UTC) To: Richard Stallman , guile-devel-mXXj517/zsQ@public.gmane.org, lightning , Markus Kuhn , Theo deRaadt , Linus Torvalds , schellr-EkmVulN54Sk@public.gmane.org Original-X-From: lightning-bounces+gcglg-lightning=m.gmane.org-mXXj517/zsQ@public.gmane.org Sat Sep 06 03:40:30 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 1XQ4zN-0005bc-Ux for gcglg-lightning@m.gmane.org; Sat, 06 Sep 2014 03:40:30 +0200 Original-Received: from localhost ([::1]:60801 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XQ4zN-0003eP-7Q for gcglg-lightning@m.gmane.org; Fri, 05 Sep 2014 21:40:29 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:57941) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XQ4zG-0003eC-8Q for lightning-mXXj517/zsQ@public.gmane.org; Fri, 05 Sep 2014 21:40:24 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1XQ4zB-0005up-Qm for lightning-mXXj517/zsQ@public.gmane.org; Fri, 05 Sep 2014 21:40:22 -0400 Original-Received: from mail-wi0-x22a.google.com ([2a00:1450:400c:c05::22a]:39890) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XQ4zB-0005uY-Eq; Fri, 05 Sep 2014 21:40:17 -0400 Original-Received: by mail-wi0-f170.google.com with SMTP id cc10so326200wib.3 for ; Fri, 05 Sep 2014 18:40:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; bh=+YUeqaD5p1dl+vfoKVbZ6VN3m+qQNdpzwZ3mLlQwTrk=; b=sKcXiJha8aHnfU+ZNC4+WXXOu+67OYNAnhXz6cz5XHrYF8e/6dVpaowhzkxoa/1y3G W5oELeHF6fomCMxKvxtOqqxsl7m5hQPzmNjJ0xGAJdc8RHrAS8WRaBw3It4ppYJyGJMY 0GiLES95BUHdvJ6kGLXMCcMFx4esyXO+Qk3UqihzpDXEQlzWhuR5lum+KFJAzm28Xqh/ 203zunRCod9iLypi7wzsddrBIVWe5QBA28Bepuyb0QE9RV02aOBB06Ld6WRd8RJqGE8l g04EIW+m5t1lgspgs5Iay+nRbvVAso+DLrSbJpeI/yvXQtoBSJZ5JjIo04h1zqYuV0i7 yyCw== X-Received: by 10.194.77.212 with SMTP id u20mr18639409wjw.27.1409967616301; Fri, 05 Sep 2014 18:40:16 -0700 (PDT) Original-Received: by 10.194.219.234 with HTTP; Fri, 5 Sep 2014 18:40:16 -0700 (PDT) In-Reply-To: X-detected-operating-system: by eggs.gnu.org: Error: Malformed IPv6 address (bad octet value). X-Received-From: 2a00:1450:400c:c05::22a 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:572 gmane.lisp.guile.devel:17418 Archived-At: --===============0597645743584253746== Content-Type: multipart/alternative; boundary=047d7bfcf858ea230905025baa61 --047d7bfcf858ea230905025baa61 Content-Type: text/plain; charset=UTF-8 On Thu, Sep 4, 2014 at 9:50 PM, Richard Stallman wrote: > There are limits to how much effort we should make to deal with the > imponderable possibilities of sabotage. Especially since there is so > much else we know that we need to do. To throw away all our software > because of these possibilities would not make sense. > At no point did I say you _have_ to throw away your software. On the contrary, I have explained to you precisely how you could have a means by which you can gain assurance, whenever you need it and at very little effort, that in fact the software has very probably not been sabotaged. So instead of putting up what are quite frankly feeble arguments as to the unlikelihood of such an attack, you could have assurance that it was _in fact_ improbable, and you would be able to put a figure on the improbability, and you would be able to explain to anyone who cared to listen, how you had arrived at that figure. But you think this is a research project. Well I am telling you now, for free, that it is not a research project, it is something that we can actually implement. Just because _you_ don't see how it could be done, does not mean it's impossible, because it may just be the case that there is something about semantics that _you_ don't know. Now it is clear to everyone that you do not yet understand the problem because you write > I think our community's distributed build practices would > make it difficult for such a sabotage to hit the whole > community. Many GCC developers and redistributors > have been bootstrapping for decades using their old versions. The GCC developers don't ship object code, do they? So the compiler the GCC developers use is irrelevant. This is an object code trap door, it does not need to be in the source code. But I sincerely doubt that the GCC developers have in fact bootstrapped from their old binaries for decades. What reason would they have to do that? They are just like me: I use whatever compiler binary is on the distribution, as long as it is capable of compiling my source, and their source can be compiled by any old gcc binary. But as I say, this is irrelevant. 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. 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. 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. So we can have interpreters for languages that are capable of compiling their own bytecode interpreters and primitives. For example, Guile will be able to JIT compile all of what it now ships as C code, from scheme. So all it will need to bootstrap is a simple scheme interpreter. It could in in fact write that scheme interpreter itself, just by shipping out lightning codes implementing its bytecode interpreter, to a lightning compiler. Of course this scheme interpreter would be susceptible to sabotage if the lightning compiler were written in C. The thing is A LIGHTNING COMPILER COULD BE TRIVIAL TO WRITE FROM SCRATCH IF WE ONLY HAD A MACHINE READABLE DEFINITION OF LIGHTNING SEMANTICS. I explained all of this in the PDF I sent to you two weeks ago, and which I sent to these lists. All we need to do to implement this is to extract the data defining the instruction encoding that the assembler carries out for the various architectures, and get Paulo to write a data file formally defining the process by which lightning translates the lightning opcodes into assembler in the various architectures it supports. I explained in a post to that list that this need not be too hard to do: we only need a core subset of primitives with universal architecture support. 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? Ian --047d7bfcf858ea230905025baa61 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
On Thu, Sep 4, 2014 at 9:50 PM, Richard Stallman <rms-mXXj517/zsQ@public.gmane.org> wrote:
There are limits to how much effort we should make to deal with the
imponderable possibilities of sabotage.=C2=A0 Especially since there is so<= br> much else we know that we need to do.=C2=A0 To throw away all our software<= br> because of these possibilities would not make sense.
<= br>
At no point did I say you _have_ to throw away your software.= On the contrary, I have explained to you precisely how you could have a me= ans by which you can gain assurance, whenever you need it and at very littl= e effort, that in fact the software has very probably not been sabotaged. S= o instead of putting up what are quite frankly feeble arguments as to the u= nlikelihood of such an attack, you could have assurance that it was _in fac= t_ improbable, and you would be able to put a figure on the improbability, = and you would be able to explain to anyone who cared to listen, how you had= arrived at that figure.

But you think this is a research project. <= br>
Well I am telling you now, for free, that it is not a research proje= ct, it is something that we can actually implement. Just because _you_ don&= #39;t see how it could be done, does not mean it's impossible, because = it may just be the case that there is something about semantics that _you_ = don't know.

Now it is clear to everyone that you do n= ot yet understand the problem because you write

> I think our co= mmunity's distributed build practices would
> make it difficult f= or such a sabotage to hit the whole
> community.=C2=A0 Many GCC devel= opers and redistributors
> have been bootstrapping for decades using = their old versions.

The GCC developers don't ship object code, do they? So t= he compiler the GCC developers use is irrelevant. This is an object code tr= ap door, it does not need to be in the source code.

But I= sincerely doubt that the GCC developers have in fact bootstrapped from the= ir old binaries for decades. What reason would they have to do that? They a= re just like me: I use whatever compiler binary is on the distribution, as = long as it is capable of compiling my source, and their source can be compi= led by any old gcc binary. But as I say, this is irrelevant.

<= div>The problem is this: it is impossible to bootstrap the GNU tool-chain f= rom scratch because it's all written in C, and C is too complex a langu= age to use for a definitional interpreter. So we always rely on the semanti= cs determined by some C compiler binary, which semantics is what you call a= n imponderable.

What we need is a language with a simple semantics f= or 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 compile= r that we know is secure, and the reference tools that we use to verify tha= t the object code produced by the full 740 MB of GCC source when compiled b= y the 74MB gcc binaries, is the same object code our reference compiler pro= duces.

Now I think we can do this with GNU Gui= le and GNU Lightning. What we need is the semantics of lightning to be defi= ned as program data: so we define the expansions of the lightning primitive= s as assembler in the various target architectures, and we formally define = the mapping the instruction encoders for the various architectures use to m= ap assembler to binary machine code instructions. Then we can automatically= generate lightning assemblers in any source language for which we need it= .

So we can have interpreters for languages that are capable of comp= iling their own bytecode interpreters and primitives. For example, Guile wi= ll be able to JIT compile all of what it now ships as C code, from scheme. = So all it will need to bootstrap is a simple scheme interpreter. It could i= n in fact write that scheme interpreter itself, just by shipping out lightn= ing codes implementing its bytecode interpreter, to a lightning compiler. O= f course this scheme interpreter would be susceptible to sabotage if the li= ghtning compiler were written in C.

The thing is A LIGHTN= ING COMPILER COULD BE TRIVIAL TO WRITE FROM SCRATCH IF WE ONLY HAD A MACHIN= E READABLE DEFINITION OF LIGHTNING SEMANTICS.

= I explained all of this in the PDF I sent to you two weeks ago, and which I= sent to these lists.

All we need to do to implement thi= s is to extract the data defining the instruction encoding that the assembl= er carries out for the various architectures, and get Paulo to write a data= file formally defining the process by which lightning translates the light= ning opcodes into assembler in the various architectures it supports. I exp= lained in a post to that list that this need not be too hard to do: we only= need a core subset of primitives with universal architecture support.
<= /div>

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

Ian

<= /div>
--047d7bfcf858ea230905025baa61-- --===============0597645743584253746== Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Disposition: inline _______________________________________________ Lightning mailing list Lightning-mXXj517/zsQ@public.gmane.org https://lists.gnu.org/mailman/listinfo/lightning --===============0597645743584253746==--