Re: Verifying Toolchain Semantics

2014-10-08 Thread Mark H Weaver
Ian Grant writes: > On Tue, Oct 7, 2014 at 1:28 PM, Mark H Weaver wrote: >> Ian, please stop posting to guile-devel. You've made your points, and >> I've even called attention to what I think is the best exposition of >> your ideas. At this point you're just repeating yourself and hurling >> g

Re: Verifying Toolchain Semantics

2014-10-07 Thread Mike Gerwitz
To limit your attack area for a response (out of respect for the recipients---feel free to continue this conversation with me in private) I'm going to keep this relatively brief. On Tue, Oct 07, 2014 at 01:18:31PM -0400, Ian Grant wrote: > The problem is not understood by _you._ otherwise you woul

Re: Verifying Toolchain Semantics

2014-10-07 Thread Ian Grant
On Tue, Oct 7, 2014 at 1:28 PM, Mark H Weaver wrote: > Ian, please stop posting to guile-devel. You've made your points, and > I've even called attention to what I think is the best exposition of > your ideas. At this point you're just repeating yourself and hurling > gratuitous insults. Enough

Re: Verifying Toolchain Semantics

2014-10-07 Thread Mark H Weaver
Ian, please stop posting to guile-devel. You've made your points, and I've even called attention to what I think is the best exposition of your ideas. At this point you're just repeating yourself and hurling gratuitous insults. Enough! Mark

Re: Verifying Toolchain Semantics

2014-10-07 Thread Ian Grant
On Mon, Oct 6, 2014 at 12:23 AM, Mike Gerwitz wrote: > On Sun, Oct 05, 2014 at 12:11:00PM -0400, Ian Grant wrote: >> > As has been stated---your concerns are substantiated and understood, >> >> I wasn't aware that my concerns _have_ been substantiated. How? I am >> not sure they have been understo

Re: Verifying Toolchain Semantics

2014-10-06 Thread William ML Leslie
On 6 October 2014 11:30, Ian Grant wrote: > 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 w

Re: Verifying Toolchain Semantics

2014-10-06 Thread Nala Ginrut
On Mon, Oct 6, 2014 at 12:24 AM, Ian Grant wrote: > On Sun, Oct 5, 2014 at 11:15 AM, Nala Ginrut wrote: > > > > Alright, I changed a system and try it again with evince successfully. > > Anyway, I did't find any maths or special symbols in it, so it could be > > published on your blog as plain t

Re: Verifying Toolchain Semantics

2014-10-05 Thread Mike Gerwitz
On Sun, Oct 05, 2014 at 12:11:00PM -0400, Ian Grant wrote: > > As has been stated---your concerns are substantiated and understood, > > I wasn't aware that my concerns _have_ been substantiated. How? I am > not sure they have been understood, either. They were substantiated long ago by the very r

Re: Verifying Toolchain Semantics

2014-10-05 Thread Ian Grant
On Sun, Oct 5, 2014 at 1:42 PM, Ian Grant wrote: > [we] will be able to implement a C compiler in Microsoft Word BASIC, or in > COBOL, and that will be capable of compiling GCC, if we had a year or > so to wait while it does it ... This is not true. Word BASIC or COBOL could easily write out an e

Re: Verifying Toolchain Semantics

2014-10-05 Thread Ian Grant
Taylan wrote: > In your PDF analogy, the solution is to write a spurious > amount of PDF implementations. Or for C, to implement > a spurious amount of C compilers. That is impractical > because C is complex. It's not as complex as you might think. In the space of a couple of months, I wrote wha

Re: Verifying Toolchain Semantics

2014-10-05 Thread Ian Grant
On Sun, Oct 5, 2014 at 11:15 AM, Nala Ginrut wrote: > > Alright, I changed a system and try it again with evince successfully. > Anyway, I did't find any maths or special symbols in it, so it could be > published on your blog as plain text. But you may insist on the opinion of > PDF. There is ano

Re: Verifying Toolchain Semantics

2014-10-05 Thread Ian Grant
On Sun, Oct 5, 2014 at 2:58 AM, Mike Gerwitz wrote: > On Sat, Oct 04, 2014 at 09:35:09PM -0400, Ian Grant wrote: >> Well, if I do succeed in distributing malware, it will be a good >> demonstration of what I have been arguing for months now, which is >> that your "core infrastructure" is _very,_ _

Re: Verifying Toolchain Semantics

2014-10-05 Thread Nala Ginrut
On Sun, Oct 5, 2014 at 10:14 PM, Ian Grant wrote: > On Sun, Oct 5, 2014 at 1:39 AM, Nala Ginrut wrote: > > > > The real problem here, is the provided PDF can't be opened normally. > That's > > bad, for your idea. It's your mistake, not others. > > Then tell me the name, the sha512sum of the file

Re: Verifying Toolchain Semantics

2014-10-05 Thread Ian Grant
On Sun, Oct 5, 2014 at 1:39 AM, Nala Ginrut wrote: > > The real problem here, is the provided PDF can't be opened normally. That's > bad, for your idea. It's your mistake, not others. Then tell me the name, the sha512sum of the file, the URL from which you downloaded it and the size of the file a

Re: Verifying Toolchain Semantics

2014-10-05 Thread William ML Leslie
On 3 October 2014 22:56, Taylan Ulrich Bayirli/Kammer < taylanbayi...@gmail.com> wrote: > William ML Leslie writes: > > > ​Oh, interesting point. Maybe we should define PDF as an abstract > > semantics that we can convert into a wide range of equivalent document > > layout languages? If the attac

Re: Verifying Toolchain Semantics

2014-10-04 Thread Mike Gerwitz
On Sat, Oct 04, 2014 at 09:35:09PM -0400, Ian Grant wrote: > Well, if I do succeed in distributing malware, it will be a good > demonstration of what I have been arguing for months now, which is > that your "core infrastructure" is _very,_ _very_ flaky, and that far > from being "the most important

Re: Verifying Toolchain Semantics

2014-10-04 Thread Nala Ginrut
2014年10月5日 上午9:35于 "Ian Grant" 写道: > > Well, if I do succeed in distributing malware, it will be a good > demonstration of what I have been arguing for months now, which is > that your "core infrastructure" is _very,_ _very_ flaky, and that far > from being "the most important developers," you are

Re: Verifying Toolchain Semantics

2014-10-04 Thread Ian Grant
On Fri, Oct 3, 2014 at 2:23 AM, Mark H Weaver wrote: >> http://livelogic.blogspot.com/2014/10/the-foundation-part-i.html > I downloaded the PDF linked in that blog entry and attempted to view it > using Emacs's docview mode, which reported that the pdf->png process > died with a segfault. Thi

Re: Verifying Toolchain Semantics

2014-10-03 Thread Mark H Weaver
Taylan Ulrich Bayirli/Kammer writes: > In your PDF analogy, the solution is to write a spurious > amount of PDF implementations. Or for C, to implement a spurious amount > of C compilers. That is impractical because C is complex. What might > be practical might be to write one new C compiler (

Re: Verifying Toolchain Semantics

2014-10-03 Thread Taylan Ulrich Bayirli/Kammer
William ML Leslie writes: > ​Oh, interesting point. Maybe we should define PDF as an abstract > semantics that we can convert into a wide range of equivalent document > layout languages? If the attacker can't tell exactly what xsl-fo or > dsssl the tool will output, or what software you're using

Re: Verifying Toolchain Semantics

2014-10-03 Thread Nala Ginrut
On Fri, 2014-10-03 at 02:23 -0400, Mark H Weaver wrote: > Ian Grant writes: > > > Dear programming language types, > > > > I wrote this to try once again to explain what is the nature of the > > problem that one would have in verifying the integrity of _any_ > > software toolchain, whether it is

Re: Verifying Toolchain Semantics

2014-10-03 Thread William ML Leslie
On 3 October 2014 16:23, Mark H Weaver wrote: > Instead, he insists to distribute them in an opaque > format that can only be interpreted by a small handful of very complex > programs with a large attack surface. > ​Oh, interesting point. Maybe we should define PDF as an abstract semantics that

Re: Verifying Toolchain Semantics

2014-10-02 Thread Mark H Weaver
Ian Grant writes: > Dear programming language types, > > I wrote this to try once again to explain what is the nature of the > problem that one would have in verifying the integrity of _any_ > software toolchain, whether it is aimed ultimately at the production > of other software, or of hardware