From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: William ML Leslie Newsgroups: gmane.comp.gnu.lightning.general,gmane.comp.gnu.system,gmane.lisp.guile.devel Subject: Re: GNU Thunder Date: Sat, 6 Sep 2014 18:32:55 +1000 Message-ID: References: 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 1409992388 16841 80.91.229.3 (6 Sep 2014 08:33:08 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sat, 6 Sep 2014 08:33:08 +0000 (UTC) Cc: gnu-system-discuss-mXXj517/zsQ@public.gmane.org, lightning , guile-devel To: Ian Grant Original-X-From: lightning-bounces+gcglg-lightning=m.gmane.org-mXXj517/zsQ@public.gmane.org Sat Sep 06 10:33:02 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 1XQBQc-0002gJ-GF for gcglg-lightning@m.gmane.org; Sat, 06 Sep 2014 10:33:02 +0200 Original-Received: from localhost ([::1]:33792 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XQBQc-0002QI-4R for gcglg-lightning@m.gmane.org; Sat, 06 Sep 2014 04:33:02 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:41309) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XQBQY-0002QB-Cm for lightning-mXXj517/zsQ@public.gmane.org; Sat, 06 Sep 2014 04:32:59 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1XQBQW-0002et-VL for lightning-mXXj517/zsQ@public.gmane.org; Sat, 06 Sep 2014 04:32:58 -0400 Original-Received: from mail-oa0-x236.google.com ([2607:f8b0:4003:c02::236]:41759) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XQBQW-0002ef-OV; Sat, 06 Sep 2014 04:32:56 -0400 Original-Received: by mail-oa0-f54.google.com with SMTP id g18so9382587oah.27 for ; Sat, 06 Sep 2014 01:32:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=p9AbAlM+ezQ1rThGArLt1qKZBrjc61bJvdmPk3r/wq0=; b=LMbD6hW3XsM4k+tYe+rKaImpqEDJUNqRGTpTkSKC9zBl3fCHWmgtEtBoG8J3b3YuX6 GYK8G2Z69yElKZLGTTxPW5XfLVpBNRoCsUV5MAq7KeOajke+4/9Q2wNwXakReYT+XIa5 fl33i/rdHJucBs998w4HN2Sd/7TlMwiIFE87GWfj97oJ1JjtV413UoyBwyViOG++JWVj hteVYIjajX1gWdF53LLOAOOHS4WvqLVieLktwB/LMZk5uqZEelaVqnadsP0byUu16g04 C40tOHrM4tLQmhXpITkxRWC23pvElu2T6YUw9CoczMQmmYA7FOZAhaHcK6XgOJ1C0ofB DR4g== X-Received: by 10.182.114.169 with SMTP id jh9mr18732745obb.25.1409992375179; Sat, 06 Sep 2014 01:32:55 -0700 (PDT) Original-Received: by 10.182.165.196 with HTTP; Sat, 6 Sep 2014 01:32:55 -0700 (PDT) In-Reply-To: X-detected-operating-system: by eggs.gnu.org: Error: Malformed IPv6 address (bad octet value). X-Received-From: 2607:f8b0:4003:c02::236 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:573 gmane.comp.gnu.system:151 gmane.lisp.guile.devel:17419 Archived-At: On 6 September 2014 11:40, Ian Grant wrote: > 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. Actually, I think GCC is quite remarkable as a semantic fixpoint. As someone interested in runtime implementation, I'd poked around in GCC a bunch of times for different reasons without ever comprehending how it really /worked/. After reading the Moxie Project blog, I had a very different opinion. The blog explained that porting GCC to an architecture involves, among other things, writing an interpreter for the target platform (for gdb to use) in C, as well as providing instructions for GCC to lower into. So, in a sense, GCC has a number of semantic fixed points, one per platform. Incidentally, I don't think semantic fixpoints are sufficient to protect you from this crack. As you mentioned, it is possible to compromise the system's hash functions, file open operations, and exec server in such a way that you're lied to whenever you ask questions that could reveal the difference. The inelegant form of the crack, manifesting itself in the object files, may be easy enough to discover via disassembly on another box. If that is all you're trying to defend against, verified compilers already get you there. Unfortunately there are no Free Software verified C compilers, but there could be I guess. The more complicated form of the crack - where several system functions are compromised - is much harder to detect. There is one way I know about, namely using the amount of storage space on the system as a means to ensure that there is nothing you've missed. That is, fill up all but a few kilobytes of the system with data that you can read back out and verify. Modern systems include so many caches that such detection would require you to run such a check directly off the hard disk controller or so (even many of these have enough RAM to boot a small GNU/Linux system) if you wanted to have real assurance. > 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. As an aside: this has always been a little fantasy of mine (and I know I'm not alone). I've written little lisps in all sorts of languages (including C and m68k assembler), ostensibly to experiment with different optimisations or kill time on a train trip, but secretly to prove to myself that if I ever find I am in some twighlight-zone situation where I'm a child in the early 90's again and *this time* I can really convince my parents to buy me a computer, I can bootstrap myself up from machine code if need be (: > 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. Ok, that's a cool idea. You're a pretty decent hacker, you should do it. I'm busy with other things. >From a security point of view, I'm now slowly working toward verified runtimes (including verified JIT), replacing C as the low-level language de jure, and a verified kernel for GNU. My opinion that these were TRT to do *next* formed over many years, and only slowly it became clear to me that they are possible (if a lifetime of train trips in length). There are other opinions, and many problems to be solved. I don't think they are invalid. > 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? Of the many things that we can do to make things better for software developers, you have one idea. Please understand that our lack of enthusiasm for it is not without our own individual commitments to the security and freedoms of users; rather while the extra assurances your project may provide sound nice, they are frankly rather minimal and don't have much additional utility, and so are not priority one. -- William Leslie Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement.