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: Verifying Toolchain Semantics Date: Sun, 5 Oct 2014 20:30:57 -0400 Message-ID: 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 1412555477 17440 80.91.229.3 (6 Oct 2014 00:31:17 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 6 Oct 2014 00:31:17 +0000 (UTC) To: William Leslie , =?UTF-8?B?VGF5bGFuIEJhecSxcmzEsQ==?= , guile-devel , lightning Original-X-From: lightning-bounces+gcglg-lightning=m.gmane.org-mXXj517/zsQ@public.gmane.org Mon Oct 06 02:31:12 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 1XawCg-0006Mv-Pi for gcglg-lightning@m.gmane.org; Mon, 06 Oct 2014 02:31:07 +0200 Original-Received: from localhost ([::1]:49521 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XawCg-0007CZ-6k for gcglg-lightning@m.gmane.org; Sun, 05 Oct 2014 20:31:06 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:33515) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XawCb-0007CJ-Vf for lightning-mXXj517/zsQ@public.gmane.org; Sun, 05 Oct 2014 20:31:03 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1XawCa-0006O6-3v for lightning-mXXj517/zsQ@public.gmane.org; Sun, 05 Oct 2014 20:31:01 -0400 Original-Received: from mail-wi0-x22a.google.com ([2a00:1450:400c:c05::22a]:56455) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XawCZ-0006Nz-OA; Sun, 05 Oct 2014 20:31:00 -0400 Original-Received: by mail-wi0-f170.google.com with SMTP id hi2so5407812wib.5 for ; Sun, 05 Oct 2014 17:30:57 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20120113; h=mime-version:date:message-id:subject:from:to:content-type; bh=UeD2GPojVpQuiYNVal+Oje9hckwNB0lChNPF1BkBbog=; b=a0GsUPHEhBbbPhom0Jq+OrjJdbdQsYzzRz60DpBsGUYefDDDertTyakttfZKjo4VK2 ElPQOg3J0Vmvxq4aquhifqP0HqORS7zKcs/CiioPsJPf7BbAAwbMP+r196rHP8MY2ns2 Tl/CnzcbYWMKynVXzhEZrnFGTI3rEmZmSoN7cmHL/0BuCaara0PtttCo5QpMsX9Dk+k7 GJw/GK7LLoAwu1X+e0mg1k/n9/mGDrwe+lu4WK62PRAtOhnBrxnzzcfh+QkU0W4CIr7l WvAO9wJv0a4gBD+S7dRe88GN+wUw/dFZ0JBnRvBGO9lNyiacure8JkjyhreBBfWel+od JTcw== X-Received: by 10.180.94.163 with SMTP id dd3mr15630990wib.31.1412555457840; Sun, 05 Oct 2014 17:30:57 -0700 (PDT) Original-Received: by 10.194.77.49 with HTTP; Sun, 5 Oct 2014 17:30:57 -0700 (PDT) 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:601 gmane.lisp.guile.devel:17554 Archived-At: http://lists.gnu.org/archive/html/guile-devel/2014-10/msg00016.html From: William ML Leslie Date: Mon, 6 Oct 2014 00:57:49 +1100 On 3 October 2014 22:56, Taylan Ulrich Bayirli/Kammer wrote: > Say, for example, that I can guess you will end up viewing the > document with one of five output programs - maybe, evince, chrome, > tk, gecko translating xsl-fo to xul or firefox viewing html 4 > directly, and say that I only have exploits for the first three. > Now I have a bit of a problem: I need to find a way to get your tool > to emit the specific structure that will invoke the exploit. Since > it will show a document that looks correct, although underneath may > have a different structure, I will have to account for variation in > what it emits but there will be a limited class of algebraic > manipulations that it can make without changing the semantics of the > document. It's not about this. These are all the programs that have problems. We're not going to use these sorts of programs anymore. We're going to use auto-generated, nearly perfect code. And after a few years it won't be just near perfect, it'll be perfect. > Maybe I would not find a way to /reliably/ produce a document that > will infect your machine. Or maybe I would. It's hypothetical. > But you know as well as I do that fuzzing a document generator to > see what instructions produce exploitable output is easier than > either writing a verifiable PDF viewer or writing a tool that > bisimulates a PDF document with a class of layout languages. The > cherry on top is that all that extra code you introduce is surely > ripe with additional vulnerabilities - so maybe I don't need to > bother with producing those back-end exploits at all. This is wrong. If you look at the automatically-generated assembler code from a formal spec, in the form of a functional program generating that code: https://github.com/IanANGrant/red-october/blob/master/src/dynlibs/ffi/AbstractMachineWord.sml you will see that the extra code has no extra attack vectors. It's all machine-generated. If this were a piece of code for reading a binary file, then it would have been generated from a grammar describing exactly what are the valid words in that language. (Using words and language in the technical sense as "valid strings" and "set of all valid strings".) So buffer overruns won't happen. And if all the semantics are formalised, then off-by-one errors won't happen either. If they do, they'll happen all over the place and you will find out very quickly. > Though I think your analogy is wrong. PDF is already an abstract > semantics, like any formal language spec. The question is whether > an implementation realizes precisely those semantics, or adds "oh > and insert a backdoor" to some pieces of code in that language, "as > an addition to the language semantics." This augmentation to the > semantics needn't be apparent in the source code of the > implementation, since the language it's written in might again be > compiled by a compiler that "augments" the semantics of the language > it compiles, and that in turn needn't be apparent in the compiler's > source ... until you arrive at the since long vanished initial > source code that planted the virus. > I hope by now you understand why I think this to be nonsense. It's > still a C compiler. You know that, I know that. Why wouldn't the > machine be able to tell? Because it's formally undecidable. That's Rice's Theorem. And it's not "in practice" probably detectable by semantantic methods, because we are going to extra lengths to obscure the effective operational semantics by multiple re-encodings. How are you going to recognise a compiled Fortran90 program translating a C program into an abstract assembler like lightning, as a C compiler? You don't even know what the opcode numbers are: we can permute them. > The problem that I have with this discussion is that rather than > address many* of the points in my email, he instead resorted to > insisting I was a shill. It's very difficult to have a conversation > with someone who uses silencing tactics. Or better - it's > pointless. What are you talking about? Here is what you wrote to me: http://lists.gnu.org/archive/html/guile-devel/2014-09/msg00036.html > 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. Now if you wanted me to continue answering your questions, then well, I'm sorry, I just got the wrong end of stick completely. I thought you wanted me to fuck off! So I replied as below. To you, privately. And that was it. Silencing tactics? You then copied it to the world, and a guy who I _told_ you, was deputy director of the NSA's National Computer Security Centre! And I didn't mind. (I did wonder what the hell does he think he's doing?! But it's your privilege to say what you want, to whom you want, and none of my business.) Date: Sun, 7 Sep 2014 11:39:44 +1000 Message-ID: Subject: Re: GNU Thunder From: William ML Leslie To: Ian Grant , guile-devel , lightning , schellr-EkmVulN54Sk@public.gmane.org X-List-Received-Date: Sun, 07 Sep 2014 01:39:50 -0000 --e89a8ff1ca20e0b37105026fc673 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On 7 September 2014 01:49, Ian Grant 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. > =E2=80=8BUnfortunately, this is a reality we have to deal with when discuss= ing 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 =E2=80=8Badding 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. --=20 William Leslie [...] Here's my e-mail: MIME-Version: 1.0 Received: by 10.194.219.234 with HTTP; Sat, 6 Sep 2014 08:49:15 -0700 (PDT) In-Reply-To: References: Date: Sat, 6 Sep 2014 11:49:15 -0400 Delivered-To: ian.a.n.grant-gM/Ye1E23mwN+BqQ9rBEUg@public.gmane.org Message-ID: Subject: Re: GNU Thunder From: Ian Grant To: William ML Leslie Content-Type: multipart/alternative; boundary=001a1136144a26f19e05026787e6 --001a1136144a26f19e05026787e6 Content-Type: text/plain; charset=UTF-8 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. Ian --001a1136144a26f19e05026787e6 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
You are just not at all convincing, I'm afraid. Tell y= our boss they didn't train you properly, and can you get assigned somew= here else.

Ian

--001a1136144a26f19e05026787e6-- ============================================================================= You see, I thought you were a Microsoft plant. I just couldn't figure out any other reason why someone who clearly didn't know anything about computers, would say they were going to write a secure operating system! :-) Ian