Re: [Lightning] GNU Thunder

[Ian Grant]

On Sun, Sep 7, 2014 at 9:18 AM, Taylan Ulrich Bayirli/Kammer <address@hidden> 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