Path: csiph.com!x330-a1.tempe.blueboxinc.net!usenet.pasdenom.info!aioe.org!feeder.news-service.com!newsfeed.xs4all.nl!newsfeed6.news.xs4all.nl!xs4all!post.news.xs4all.nl!not-for-mail
DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=Nng831N/qxp+I58x0m3L3P0JeD+2Uf/hkJ6MTfXv53nG1ewrtxNsb8SDzDmqjzftUV 9iIYrcn7j7HM5PvgC4M+RGBOQGqZwZh7RCtYn/96qRkhlPgjahDLM6fBHZNKszRepdET 3tPkDeKQpxhsCOtE+3U11CClMPuATxOTQZ2Mk=
MIME-Version: 1.0
In-Reply-To: <0q3ga8-s2v.ln1@svn.schaathun.net>
References: <4DD08620.4030507@tysdomain.com> <mailman.1611.1305512463.9059.python-list@python.org> <op.vvlipenoa8ncjz@gnudebst> <5h9ca8-ekq.ln1@svn.schaathun.net> <mailman.1757.1305737674.9059.python-list@python.org> <rgcda8-tor.ln1@svn.schaathun.net> <mailman.1769.1305745672.9059.python-list@python.org> <1skda8-3as.ln1@svn.schaathun.net> <mailman.1773.1305754489.9059.python-list@python.org> <4vlea8-55t.ln1@svn.schaathun.net> <mailman.1795.1305825830.9059.python-list@python.org> <0q3ga8-s2v.ln1@svn.schaathun.net>
Date: Thu, 19 May 2011 17:56:12 -0700
Subject: Re: obviscating python code for distribution
From: geremy condra <debatem1@gmail.com>
To: Hans Georg Schaathun <hg@schaathun.net>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Cc: python-list@python.org
Precedence: list
Newsgroups: comp.lang.python
Message-ID: <mailman.1808.1305852976.9059.python-list@python.org>
Lines: 67
NNTP-Posting-Host: 82.94.164.166
Xref: x330-a1.tempe.blueboxinc.net comp.lang.python:5801

On Thu, May 19, 2011 at 11:23 AM, Hans Georg Schaathun <hg@schaathun.net> w=
rote:
> On Thu, 19 May 2011 10:23:47 -0700, geremy condra
> =A0<debatem1@gmail.com> wrote:
> : =A0Let me get this straight: your argument is that operating *systems*
> : =A0aren't systems?
>
> You referred to the kernel and not the system. =A0The complexities of
> the two are hardly comparable.

I don't know about that. Among the many verified microkernels, at
least two projects have formally verified both their kernel and their
toolchain, and one of them claims they've verified everything in their
TCB and are headed towards verified POSIX compliance in 2012. That
would seem to be a fairly large system (and definitely a complete OS)
to me. Another (seL4) says they've formally verified security  of a
complete system that includes a userspace and the ability to run other
OSes in fully isolated containers, which also seems to be quite
complete. Finally, there's one from Microsoft research that claims
similar properties but which apparently isn't interested in
compatibility, which I'm not sure how to interpret in terms of
usefulness and size. In any event, higher level systems- like
electronic voting mechanisms and automotive sensor networks- have also
been verified, which seems to run counter to your original point.

Also, not sure if it's open to the general public but if you're
interested in this kind of thing and live near seattle, I think
there's actually going to be a talk on verifying a POSIX userspace
implementation here tomorrow.

TL;DR version: large systems have indeed been verified for their
security properties.

> There probably are different uses of system; in computer security
> literature=B9 it often refers, not only to a product (hardware/software)
> an actual installation and configuration of that product in a specific
> context. =A0/I/ did not redefine it.

You chose a word with a many meanings, used it to make a very broad
statement which is only a little bit true, and then pretended that you
had the One True Definition in your pocket. I don't think that's
legitimate, but whatever; let's just say that we meant different
things by the word and drop it.

> Speaking of reasonable assumptions, one necessary assumption which is
> particularly dodgy is that whoever deploys and configures it
> understands all the assumptions and do not break them through ignorance.

Yup. Nothing is safe from idiots.

> Is your concern with security purely from a developer's viewpoint,
> so that you don't have to worry about the context in which it will
> be deployed?

My viewpoint is that of an attacker, since that's more or less my job.

> I read your initial comment to imply that if you cannot get satisfactory
> assurance using the lower levels, you won't get any at the higher
> levels. =A0That does not make any sense.

Well, this is kind of like my point. My point was that you really
don't get anything at the lower levels, and that they should fix that
(which is far more useful to a normal consumer) rather than trying to
talk about formal verification and similar tools, which are only going
to be used on a tiny fraction of products.

Geremy Condra