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
Return-Path: <debatem1@gmail.com>
X-Original-To: python-list@python.org
Delivered-To: python-list@mail.python.org
X-Spam-Status: OK 0.043
X-Spam-Evidence: '*H*': 0.91; '*S*': 0.00; 'one?': 0.05; 'correctness': 0.09; 'am,': 0.14; 'wrote:': 0.14; 'subject:python': 0.14; 'correct)': 0.16; 'properties.': 0.16; 'subject:distribution': 0.16; 'input': 0.17; 'cc:addr:python- list': 0.17; 'header:In-Reply-To:1': 0.21; "aren't": 0.22; 'thu,': 0.22; 'cc:2**0': 0.22; 'cc:no real name:2**0': 0.23; 'correct,': 0.23; 'received:209.85.213.46': 0.23; 'received:mail- yw0-f46.google.com': 0.23; 'subject:code': 0.23; 'fri,': 0.23; "doesn't": 0.25; 'tests': 0.26; '(in': 0.26; 'testing': 0.27; 'correct': 0.28; 'message-id:@mail.gmail.com': 0.28; '(the': 0.28; 'typically': 0.28; 'process,': 0.29; 'opposed': 0.29; 'cc:addr:python.org': 0.30; 'confident': 0.30; 'throwing': 0.30; 'it.': 0.31; 'equivalent': 0.31; 'cases': 0.32; 'steven': 0.32; "isn't": 0.33; 'source': 0.34; 'there': 0.35; '-0700,': 0.35; "d'aprano": 0.35; 'received:google.com': 0.37; 'received:209.85': 0.37; '20,': 0.37; 'bigger': 0.37; 'mathematical': 0.37; 'received:209.85.213': 0.37; 'model': 0.37; 'pretty': 0.37; 'but': 0.38; 'question,': 0.38; 'subject:: ': 0.38; 'some': 0.38; 'should': 0.39; 'received:209': 0.39; 'system.': 0.39; 'version:': 0.39; 'software': 0.40; 'really': 0.40; 'easily': 0.60; 'generate': 0.60; 'piece': 0.63; 'free': 0.63; 'feeding': 0.67; 'verified': 0.73; 'risk': 0.75; 'verification': 0.76; '12:10': 0.84; 'about,': 0.91; 'certificates': 0.95
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:in-reply-to:references:date :message-id:subject:from:to:cc:content-type; bh=4BJaakzqi8N3Qkn24gKHPuHgECLGCUR0lvCu2yOmVg8=; b=ZQ+qGcqEsp53T+KANsKmcDdf9eDfN01qIhYP4fTyr0dQngrx9Fp74p7eOF1tCYtQMl ZE6+9F/LBY6UccYeCrwOJiwtsk0MHogpNP0VIEWzrwQfNmGBExQ9Ae7OUdVZMVYkysnh 0NKvHhtmyuwUL8W0UXT0q6r35keSIcQjmMn1s=
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; b=Fi36KL26tdAbfg/DA/FTAj7/hLQUW+ZML8udrlZ5YOJd5+XwE2u86YGH8vXGN0tAmi pdT7lLFfyDqjwagj3vLMWZTnKw+nx1/in2gXdTvl+7YpIH1gsZ8WZMoHCvXsm3cwczc8 4zuB0p5SSx2vwuk4HOnKIuFH2YHHBfE9J3F6g=
MIME-Version: 1.0
In-Reply-To: <4dd613f5$0$29996$c3e8da3$5496439d@news.astraweb.com>
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> <mailman.1808.1305852976.9059.python-list@python.org> <4dd613f5$0$29996$c3e8da3$5496439d@news.astraweb.com>
Date: Fri, 20 May 2011 09:26:28 -0700
Subject: Re: obviscating python code for distribution
From: geremy condra <debatem1@gmail.com>
To: "Steven D'Aprano" <steve+comp.lang.python@pearwood.info>
Content-Type: text/plain; charset=ISO-8859-1
Cc: python-list@python.org
X-BeenThere: python-list@python.org
X-Mailman-Version: 2.1.12
Precedence: list
List-Id: General discussion list for the Python programming language <python-list.python.org>
List-Unsubscribe: <http://mail.python.org/mailman/options/python-list>, <mailto:python-list-request@python.org?subject=unsubscribe>
List-Archive: <http://mail.python.org/pipermail/python-list>
List-Post: <mailto:python-list@python.org>
List-Help: <mailto:python-list-request@python.org?subject=help>
List-Subscribe: <http://mail.python.org/mailman/listinfo/python-list>, <mailto:python-list-request@python.org?subject=subscribe>
Newsgroups: comp.lang.python
Message-ID: <mailman.1842.1305908800.9059.python-list@python.org>
Lines: 33
NNTP-Posting-Host: 82.94.164.166
X-Trace: 1305908800 news.xs4all.nl 49176 [::ffff:82.94.164.166]:35203
X-Complaints-To: abuse@xs4all.nl
Xref: x330-a1.tempe.blueboxinc.net comp.lang.python:5858

On Fri, May 20, 2011 at 12:10 AM, Steven D'Aprano
<steve+comp.lang.python@pearwood.info> wrote:
> On Thu, 19 May 2011 17:56:12 -0700, geremy condra wrote:
>
>> TL;DR version: large systems have indeed been verified for their
>> security properties.
>
> How confident are we that the verification software is sufficiently bug-
> free that we should trust their results?

Pretty confident. Most formal verification systems are developed in
terms of a provably correct kernel bootstrapping the larger system.
The important thing is that since that kernel doesn't need to be
complete (only correct) it can typically be easily verified, and in
some cases exhaustively tested. There are also techniques which
generate certificates of correctness for verifiers that aren't
provably correct, but that isn't an area I know much about, and I
don't know if that gets used in practice. The bigger risk is really
that the model you're feeding it is wrong.

> How confident are we that the verification software tests every possible
> vulnerability, as opposed to merely every imaginable one?

Formal provers typically don't work by just throwing a bunch of input
at a piece of software and then certifying it. They take a set of
specifications (the model), a set of assumptions, and the program in
question, and provide a proof (in the mathematical sense) that the
program is exactly equivalent to the model given the assumptions.
Testing the assumptions and model are typically part of the
development process, though, and that's definitely a possible source
of errors.

Geremy Condra