GNU Thunder

GNU Thunder

[Ian Grant]

[-- Attachment #1.1: Type: text/plain, Size: 427 bytes --]

Dear Lightning/Guile types,

I wrote this to try to motivate people to steer projects in mutually
beneficial directions. The two projects I had forremost in mind where GNU
Lightning and Guile. Can we discuss possible future development of these
two projects _together?_ If we can, then I think that something very good
will start to happen.

This is a link to the PDF which is a Google drive doc:

   http://goo.gl/ioTpR7

Ian

[-- Attachment #1.2: Type: text/html, Size: 527 bytes --]

[-- Attachment #2: Type: text/plain, Size: 159 bytes --]

_______________________________________________
Lightning mailing list
Lightning-mXXj517/zsQ@public.gmane.org
https://lists.gnu.org/mailman/listinfo/lightning

Re: GNU Thunder

[Richard Stallman]

[[[ To any NSA and FBI agents reading my email: please consider    ]]]
[[[ whether defending the US Constitution against all enemies,     ]]]
[[[ foreign or domestic, requires you to follow Snowden's example. ]]]

    This is a link to the PDF which is a Google drive doc:

       http://goo.gl/ioTpR7

To use Google Drive to store a document requires running some nonfree
software (written in Javascript).  Try using it with JS disabled
and you'll see.  I tried to fetch that URL and got nothing but
some Javascript code, and was unable to figure out how to access
the PDF.

I hope that nobody here would enable that Javascript code in order
to see the text.  Would you please post the PDF file in a place
where people can download it without running nonfree software?

See http://gnu.org/philosophy/javascript-trap.html for explanation of
the general issue.

However, for the purpose of discussion, it would be more effective
to format it readably as ASCII and mail us the text.

-- 
Dr Richard Stallman
President, Free Software Foundation
51 Franklin St
Boston MA 02110
USA
www.fsf.org  www.gnu.org
Skype: No way! That's nonfree (freedom-denying) software.
  Use Ekiga or an ordinary phone call.

Re: GNU Thunder

[Mike Gerwitz]

[-- Attachment #1: Type: text/plain, Size: 756 bytes --]

> To use Google Drive to store a document requires running some nonfree
> software (written in Javascript).  Try using it with JS disabled
> and you'll see.  I tried to fetch that URL and got nothing but
> some Javascript code, and was unable to figure out how to access
> the PDF.

After some trial-and-error, I was able to determine from the served JS that
this is the URL to download the PDF:

  https://docs.google.com/uc?id=0B9MgWvi9mywhblFxZTA4R1VDdlBSSW5aWENjZEZ0OXA5RTZJ

(It will perform a redirect.)

Not that this solves the problem, but will at least allow others to view the
document in the meantime.

-- 
Mike Gerwitz
Free Software Hacker | GNU Maintainer
http://mikegerwitz.com
FSF Member #5804 | GPG Key ID: 0x8EE30EAB

[-- Attachment #2: Digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: GNU Thunder

[Ian Grant]

[-- Attachment #1: Type: text/plain, Size: 1136 bytes --]

Sorry about that. I have limited resources and am restricted to using free
services. Here is a link to GitHub, I don't know if that is any better ...
probably. GitHub seems far better organised than Google.

    https://github.com/IanANGrant/red-october/raw/master/thunder.pdf

Ian



On Sun, Aug 24, 2014 at 1:13 AM, Mike Gerwitz <mikegerwitz@gnu.org> wrote:

> > To use Google Drive to store a document requires running some nonfree
> > software (written in Javascript).  Try using it with JS disabled
> > and you'll see.  I tried to fetch that URL and got nothing but
> > some Javascript code, and was unable to figure out how to access
> > the PDF.
>
> After some trial-and-error, I was able to determine from the served JS that
> this is the URL to download the PDF:
>
>
> https://docs.google.com/uc?id=0B9MgWvi9mywhblFxZTA4R1VDdlBSSW5aWENjZEZ0OXA5RTZJ
>
> (It will perform a redirect.)
>
> Not that this solves the problem, but will at least allow others to view
> the
> document in the meantime.
>
> --
> Mike Gerwitz
> Free Software Hacker | GNU Maintainer
> http://mikegerwitz.com
> FSF Member #5804 | GPG Key ID: 0x8EE30EAB
>

[-- Attachment #2: Type: text/html, Size: 1881 bytes --]

Re: GNU Thunder

[Ian Grant]

[-- Attachment #1.1: Type: text/plain, Size: 2236 bytes --]

On Sun, Aug 24, 2014 at 12:07 AM, Richard Stallman <rms-mXXj517/zsQ@public.gmane.org> wrote:


>     The research is all done. We just need to implement it.
>
> I would describe this as a domain for research, because it is
> far from clear whether it could possibly work in practice;
> if it could, it is not obvious how to make it work.
>
> It's not like writing an assembler, where we know it can work.


We don't actually know the assembler _does_ work. That's what I tried to
say. I didn't want to over-emphasise it, because I thought people might
already be bored of me banging on about it But apparently not! The problem
is the semantics of the whole GNU toolchain are inaccessible because they
depend 100% on the proprietary non-free tools that were used to build them.

This is important, so let me make a statement:

     There is not one single line of GNU source code, the meaning
      of which does not depend entirely on non-free proprietary
      software.

The source code will not tell you what the software actually does. See
Thompson's 1984 Turing Award Speech
http://www.ece.cmu.edu/~ganger/712.fall02/papers/p761-thompson.pdf for the
details. I quote:

     "The moral is obvious. You can't trust code that you did not
       totally create yourself. (Especially code from companies
       that employ people like me.) "

He works for Google now, doesn't he :-)

The trick Thompson demonstrates is what I call a _syntactic fixed-point_.
He basically makes a Y combinator of the C compiler, so that it takes in
its own source and outputs it again, but that does not mean that the source
it outputs is the source you read when you look at the source-distribution.

The solution is to establish a _semantic_ fixedpoint. But to do that we
need to be able to generate arbitrarily many essentially different working
implementations of the compiler, and make sure that the code it generates
when it compiles itself is the same, whatever the particular
implementation. So if we see that the version that we compiled into MS Word
BASIC produces the same binary executable as the JavaScript and COBOL
versions then we can have some more confidence that the semantics of the
GNU toolchain haven't been hijacked, ... yet.

Ian

[-- Attachment #1.2: Type: text/html, Size: 3060 bytes --]

[-- Attachment #2: Type: text/plain, Size: 159 bytes --]

_______________________________________________
Lightning mailing list
Lightning-mXXj517/zsQ@public.gmane.org
https://lists.gnu.org/mailman/listinfo/lightning

Trusting trust

[Ludovic Courtès]

Ian Grant <ian.a.n.grant@googlemail.com>
skribis:

> The trick Thompson demonstrates is what I call a _syntactic fixed-point_.
> He basically makes a Y combinator of the C compiler, so that it takes in
> its own source and outputs it again, but that does not mean that the source
> it outputs is the source you read when you look at the source-distribution.
>
> The solution is to establish a _semantic_ fixedpoint.

On that topic, you might like:

  https://lists.gnu.org/archive/html/guix-devel/2013-09/msg00159.html

You’re even welcome to contribute to that effort.  :-)

(I think it doesn’t have much to do with the initial lightning + Guile
discussion, though.)

Ludo’.


_______________________________________________
Lightning mailing list
Lightning@gnu.org
https://lists.gnu.org/mailman/listinfo/lightning

Re: GNU Thunder

[Stefan Monnier]

> This is a link to the PDF which is a Google drive doc:
>    http://goo.gl/ioTpR7

No, it's not a link to a PDF document.  It's a link to an
HTML+Javascript page that tries to render in your browser some PDF
document (to which I don't seem to have direct access).


        Stefan

Re: GNU Thunder

[Richard Stallman]

[[[ To any NSA and FBI agents reading my email: please consider    ]]]
[[[ whether defending the US Constitution against all enemies,     ]]]
[[[ foreign or domestic, requires you to follow Snowden's example. ]]]

	 There is not one single line of GNU source code, the meaning
	  of which does not depend entirely on non-free proprietary
	  software.

Are you saying that someone could have put a Ritchie hack
into the proprietary compilers that would detect the code
that GCC was going to have -- even though GCC kept changing?

We can't prove it did  not happen, but it would have been hard
for them to keep up with us.

-- 
Dr Richard Stallman
President, Free Software Foundation
51 Franklin St
Boston MA 02110
USA
www.fsf.org  www.gnu.org
Skype: No way! That's nonfree (freedom-denying) software.
  Use Ekiga or an ordinary phone call.

Re: GNU Thunder

[Ian Grant]

On 8/30/14, Richard Stallman <rms-mXXj517/zsQ@public.gmane.org> wrote:
> Are you saying that someone could have put a Ritchie hack
> into the proprietary compilers [...]

Perhaps you know more about the origins of the hack than I do, I was
going to call it a Schell script.

> [...] that would detect the code
> that GCC was going to have -- even though GCC kept changing?

It's surprisingly hard to fundamentally change a program that big.
Most changes are fairly minor and leave the basic structure unchanged.
So a trap door could look at the large-scale structure using
unification to do pattern matching, Then it would be able to adapt
automatically to many localised changes.

> We can't prove it did  not happen, but it would have been hard
> for them to keep up with us.

But "they" have all the source so they know exactly what they're attacking..

Ian

Re: GNU Thunder

[Richard Stallman]

[[[ To any NSA and FBI agents reading my email: please consider    ]]]
[[[ whether defending the US Constitution against all enemies,     ]]]
[[[ foreign or domestic, requires you to follow Snowden's example. ]]]

    It's surprisingly hard to fundamentally change a program that big.
    Most changes are fairly minor and leave the basic structure unchanged.

That hack recognized specific syntax.  Any change in the wrong place
would break it.

    So a trap door could look at the large-scale structure using
    unification to do pattern matching, Then it would be able to adapt
    automatically to many localised changes.

Who knows.  It is an imponderable.

The reason I am not interested in focusing on this problem, which is
conceivable, is that (1) it seems unlikely and (2) we face other
problems that are just as bad and that are real for certain.

-- 
Dr Richard Stallman
President, Free Software Foundation
51 Franklin St
Boston MA 02110
USA
www.fsf.org  www.gnu.org
Skype: No way! That's nonfree (freedom-denying) software.
  Use Ekiga or an ordinary phone call.

Re: GNU Thunder

[Ian Grant]

[-- Attachment #1.1: Type: text/plain, Size: 5361 bytes --]

> That hack recognized specific syntax.  Any change in the wrong
> place would break it.

Which hack was that? The one Thompson is reported to have actually
implemented in Unix? You are assuming what you are trying to
prove: you are assuming there has only ever been one instance of this
class of attack, and you are trying to prove that this class of attack
is unlikely. That used to be called "Begging the Question" but
nowadays the general level of understanding of logic is so poor that
most uses of that phrase are not in this sense.

It may *seem* unlikely, but to anyone who has given serious thought to
the possibilities of such an attack it seems more than wildly probable.

I suppose everyone knows that Roger Schell spent several years in the office
of deputy director of the NSA's National Computer Security Centre?  If
he did not alert the NSA to the possibility of this sort of attack
then he was not doing his job properly. Having read some of the
Computer Security History Project interview with him, I do not think
Roger Schell is the sort of person who doesn't do his job properly.

Thompson wrote that paper in 1984, and I don't think that was a
coincidence. What he shows is that if you control the semantics of a
language, that is if you control the meaning of what people say, then
you control what they *see,* and so you also control what they
think. And that was a theme in Orwell's book "1984." By controlling
the meaning of what people say, Big Brother controlled their thought.

In programming terms, if you control the semantics of the compiler,
then you can control what people see. For example, you can insert code
into libc.so and ld.so that looks for certain signatures and then
changes the data that system calls like read and stat return to
certain programs, such as sha256sum and objdump for example,
according to some predicate. You can also monitor the behaviour of
other programs. If you see that there is a program that reads mainly C
source and writes mainly a.out executables, then you know those
executables should contain a certain signature, and if they don't then
you know you have a C compiler on the system which is not bugged, at
least, one which has not got *your* bug (it may have any number of
other such bugs however, because this semantics generalises.) So you
can call for help, or you can even insert code to call for help into
the binaries that program creates. Basically, your power over the
system appears to be total. Of course it's not, because there are any
number of other such bugs in there with you. In the end the only
person who is guaranteed not to have control over what the system does
is the program source code.

Now it may seem unlikely to some that this has been done. But it is
surely obvious to *everyone* that this is *possible,* and since the
advantage an attacker accrues if he can pull this off effectively is
incalculable, it should also be obvious to *everyone* that if this has
not yet been done, then it will soon be done. Perhaps as a direct
result of people reading what I am writing right now.

So I hope people will focus on this problem, in spite of what Richard
says. He will change his mind in due course, quite shortly I think :-)

Focussing on free source code is pointless, we need to focus on free
semantics. Of course this negates certain fairly fundamental
principles of the Free Software Foundation. One of these is the idea
of "Copyleft." By taking concrete representation of algorithms as the
stock-in-trade of computer programmers, it is able to use the
copyright laws to effect a kind of viral copyright status which
automatically infects any program which uses that particular source
code representation. The problem is that once one concentrates on free
semantics rather than free source code, there is no longer any
recourse to the copyright laws: the copyright laws protect only one
particular concrete representation of an idea. The only legal
protection sematics have is through patent law. So the Free Software
Foundation, if it's to 'own' anything at all anymore, will have to
register and defend its assets as patents.

Ian


On Wed, Sep 3, 2014 at 8:50 AM, Richard Stallman <rms-mXXj517/zsQ@public.gmane.org> wrote:

> [[[ To any NSA and FBI agents reading my email: please consider    ]]]
> [[[ whether defending the US Constitution against all enemies,     ]]]
> [[[ foreign or domestic, requires you to follow Snowden's example. ]]]
>
>     It's surprisingly hard to fundamentally change a program that big.
>     Most changes are fairly minor and leave the basic structure unchanged.
>
> That hack recognized specific syntax.  Any change in the wrong place
> would break it.
>
>     So a trap door could look at the large-scale structure using
>     unification to do pattern matching, Then it would be able to adapt
>     automatically to many localised changes.
>
> Who knows.  It is an imponderable.
>
> The reason I am not interested in focusing on this problem, which is
> conceivable, is that (1) it seems unlikely and (2) we face other
> problems that are just as bad and that are real for certain.
>
> --
> Dr Richard Stallman
> President, Free Software Foundation
> 51 Franklin St
> Boston MA 02110
> USA
> www.fsf.org  www.gnu.org
> Skype: No way! That's nonfree (freedom-denying) software.
>   Use Ekiga or an ordinary phone call.
>
>

[-- Attachment #1.2: Type: text/html, Size: 6342 bytes --]

[-- Attachment #2: Type: text/plain, Size: 159 bytes --]

_______________________________________________
Lightning mailing list
Lightning-mXXj517/zsQ@public.gmane.org
https://lists.gnu.org/mailman/listinfo/lightning

Re: GNU Thunder

[Richard Stallman]

[[[ To any NSA and FBI agents reading my email: please consider    ]]]
[[[ whether defending the US Constitution against all enemies,     ]]]
[[[ foreign or domestic, requires you to follow Snowden's example. ]]]

    Which hack was that? The one Thompson is reported to have actually
    implemented in Unix? You are assuming what you are trying to
    prove: you are assuming there has only ever been one instance of this
    class of attack, and you are trying to prove that this class of attack
    is unlikely.

We can imagine all sorts of possible ways we might have been sabotaged.
It is an imponderable.

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.

-- 
Dr Richard Stallman
President, Free Software Foundation
51 Franklin St
Boston MA 02110
USA
www.fsf.org  www.gnu.org
Skype: No way! That's nonfree (freedom-denying) software.
  Use Ekiga or an ordinary phone call.

Re: GNU Thunder

[Ian Grant]

[-- Attachment #1.1: Type: text/plain, Size: 4865 bytes --]

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.  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

[-- Attachment #1.2: Type: text/html, Size: 5541 bytes --]

[-- Attachment #2: Type: text/plain, Size: 159 bytes --]

_______________________________________________
Lightning mailing list
Lightning-mXXj517/zsQ@public.gmane.org
https://lists.gnu.org/mailman/listinfo/lightning

Re: GNU Thunder

[William ML Leslie]

On 6 September 2014 11:40, Ian Grant <ian.a.n.grant-gM/Ye1E23mwN+BqQ9rBEUg@public.gmane.org> 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.

RE: GNU Thunder [Comments on Subversins from Ian Grant and Richard Stallman of GNU]

[Dr. Roger R. Schell]

[-- Attachment #1: Type: text/plain, Size: 5434 bytes --]

Although I agree with several of the comment by both Richard and Ian, most of what I would have to say is in my comments on subversion found at http://cisr.nps.edu/downloads/papers/04paper_subversion.pdf Although written a decade ago, it is still current today.

 

Roger Schell

 

From: Ian Grant [mailto:ian.a.n.grant@googlemail.com] 
Sent: Friday, September 05, 2014 6:40 PM
To: Richard Stallman; guile-devel@gnu.org; lightning; Markus Kuhn; Theo deRaadt; Linus Torvalds; schellr@ieee.org
Subject: Re: GNU Thunder

 

On Thu, Sep 4, 2014 at 9:50 PM, Richard Stallman <rms@gnu.org> 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


[-- Attachment #2: Type: text/html, Size: 8991 bytes --]

Re: GNU Thunder

[Ian Grant]

[-- Attachment #1.1: Type: text/plain, Size: 356 bytes --]

On Sun, Aug 24, 2014 at 12:07 AM, Richard Stallman <rms-mXXj517/zsQ@public.gmane.org> wrote:

> [[[ To any NSA and FBI agents reading my email: please consider    ]]]
> [[[ whether defending the US Constitution against all enemies,     ]]]
> [[[ foreign or domestic, requires you to follow Snowden's example. ]]]
>

The answer seems to be "No it doesn't."

[-- Attachment #1.2: Type: text/html, Size: 740 bytes --]

[-- Attachment #2: Type: text/plain, Size: 159 bytes --]

_______________________________________________
Lightning mailing list
Lightning-mXXj517/zsQ@public.gmane.org
https://lists.gnu.org/mailman/listinfo/lightning

Re: GNU Thunder

[William ML Leslie]

[-- Attachment #1.1: Type: text/plain, Size: 1468 bytes --]

On 7 September 2014 01:49, Ian Grant <ian.a.n.grant-gM/Ye1E23mwN+BqQ9rBEUg@public.gmane.org> wrote:

> You are just not at all convincing, I'm afraid. Tell your boss they didn't
> train you properly, and can you get assigned somewhere else.
>

​Unfortunately, this is a reality we have to deal with when discussing
security on the internet: we've got to assume the enemy is listening.  It
could be me, I could even be intercepting your emails and making them sound
incoherrent, and upping the tinfoil-hat quotient by ​adding people like
Theo and Linus to the To: list.  I could be suggesting that effort be spent
in a project that will provide very little value, wasting your time.

Remember:  I'm not suggesting what the outcome of your project will be,
just that if the result is negative, we still know nothing.  When testing a
system for subterfuge, we need to examine *all* of the moving parts, even
those that appear to be unused.  If the system you're building your
assembler on is compromised, it can still give you a negative answer.
That's what was so scary about this particular type of attack.

-- 
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.

[-- Attachment #1.2: Type: text/html, Size: 2037 bytes --]

[-- Attachment #2: Type: text/plain, Size: 159 bytes --]

_______________________________________________
Lightning mailing list
Lightning-mXXj517/zsQ@public.gmane.org
https://lists.gnu.org/mailman/listinfo/lightning

Re: GNU Thunder

[Taylan Ulrich Bayirli/Kammer]

William ML Leslie <william.leslie.ttg@gmail.com> writes:

> Remember: I'm not suggesting what the outcome of your project will be,
> just that if the result is negative, we still know nothing. When
> testing a system for subterfuge, we need to examine *all* of the
> moving parts, even those that appear to be unused. If the system you're
> building your assembler on is compromised, it can still give you a
> negative answer. That's what was so scary about this particular type
> of attack.

If I understood Mr. Grant right, the thing is that while a number of GCC
builds might have been infected a decade ago and spreading it everywhere
since we all use GCC built with GCC, if we use a new language right now
to verify GCC, a language which since it's new couldn't have its
evaluator infected at any layer (C compiler, assembler, hardware) since
it's unknown to everyone, then we can be sure.  In other words, since
this language with new semantics is being created right here and now,
it's *very* implausible (much more so than GCC being infected) that our
communications would be intercepted right away and this language's
evaluator also immediately infected to make the GCC verification fail.

Also, since we define a simple semantics for which a new evaluator could
be implemented at any time in any language, it becomes ever more and
more implausible that *all* tools everywhere have been previously
"patched" to infect all the evaluators being implemented or
automatically generated in all kinds of different environments.

I might not have fully grokked the topic so I hope I'm not just babbling.

Taylan

Re: GNU Thunder

[Ian Grant]

[-- Attachment #1.1: Type: text/plain, Size: 2331 bytes --]

On Sun, Sep 7, 2014 at 9:18 AM, Taylan Ulrich Bayirli/Kammer <
taylanbayirli-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org> wrote:

> Also, since we define a simple semantics for which a new evaluator could
> be implemented at any time in any language, it becomes ever more and
> more implausible that *all* tools everywhere have been previously
> "patched" to infect all the evaluators being implemented or
> automatically generated in all kinds of different environments.
>

Dear Taylan,

Thank you. Yours is a concise and accurate statement of what I am
proposing. If I had been able to write something that clear then I doubt
there would have been any misunderstanding between Richard and I.

What I mean by a semantic fixed point is a fixed point of the _actual_
semantics, not the syntactic forms of the textual representations such as
appear on a terminal window or in a text file dump. So we are going to do
this under the assumption that the systems we are using _are in fact
compromised._

One obvious consequence of this is that the assurance we obtain is always
in the form of actual knowledge. So if, say, the debian build team get
together and go through such a validation exercise, then they can state
they have done this, and document and explain the results on a web page,
but this will not give anyone apart from them the knowledge of the security
of the debian build process, because the build team may have been
infiltrated. But if another team of system administrators at a university,
say, were to repeat the debian exercise, using a different implementation
of the reference compiler, one they created themselves, on systems that
were isolated as far as they could determine, and perhaps whilst wearing
tin-foil hats as William recommends, then they would know they shared that
knowledge with the debian team. But no-one else would have good reason to
believe that what _they_ downloaded from the debian mirrors was actually
the real deal. So what we will be publishing is not a certificate of
security, it is a method of _actually knowing_ that the system is _very
probably_ secure. So it is extremely important that we explain very, very
clearly what this form of a trusted computing platform really is.

Thank you for your clarification. And please post any further thoughts you
might have to this thread.

Ian

[-- Attachment #1.2: Type: text/html, Size: 2792 bytes --]

[-- Attachment #2: Type: text/plain, Size: 159 bytes --]

_______________________________________________
Lightning mailing list
Lightning-mXXj517/zsQ@public.gmane.org
https://lists.gnu.org/mailman/listinfo/lightning