Re: obviscating python code for distribution

References	(9 earlier) <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	2011-05-20 09:26 -0700
Subject	Re: obviscating python code for distribution
From	geremy condra <debatem1@gmail.com>
Newsgroups	comp.lang.python
Message-ID	<mailman.1842.1305908800.9059.python-list@python.org> (permalink)

Show all headers | View raw

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

Thread

Re: obviscating python code for distribution Daniel Kluev <dan.kluev@gmail.com> - 2011-05-16 13:21 +1100
  Re: obviscating python code for distribution "Rhodri James" <rhodri@wildebst.demon.co.uk> - 2011-05-16 23:42 +0100
    Re: obviscating python code for distribution Hans Georg Schaathun <hg@schaathun.net> - 2011-05-18 08:36 +0100
      Re: obviscating python code for distribution Dotan Cohen <dotancohen@gmail.com> - 2011-05-18 17:42 +0300
      Re: obviscating python code for distribution geremy condra <debatem1@gmail.com> - 2011-05-18 09:54 -0700
        Re: obviscating python code for distribution Hans Georg Schaathun <hg@schaathun.net> - 2011-05-18 18:33 +0100
          Re: obviscating python code for distribution geremy condra <debatem1@gmail.com> - 2011-05-18 12:07 -0700
            Re: obviscating python code for distribution Hans Georg Schaathun <hg@schaathun.net> - 2011-05-18 20:56 +0100
              Re: obviscating python code for distribution geremy condra <debatem1@gmail.com> - 2011-05-18 14:34 -0700
                Re: obviscating python code for distribution Hans Georg Schaathun <hg@schaathun.net> - 2011-05-19 06:21 +0100
                Re: obviscating python code for distribution Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2011-05-19 08:47 +0000
                Re: obviscating python code for distribution Hans Georg Schaathun <hg@schaathun.net> - 2011-05-19 10:16 +0100
                Re: obviscating python code for distribution geremy condra <debatem1@gmail.com> - 2011-05-19 10:23 -0700
                Re: obviscating python code for distribution Hans Georg Schaathun <hg@schaathun.net> - 2011-05-19 19:23 +0100
                Re: obviscating python code for distribution geremy condra <debatem1@gmail.com> - 2011-05-19 17:56 -0700
                Re: obviscating python code for distribution Hans Georg Schaathun <hg@schaathun.net> - 2011-05-20 05:48 +0100
                Re: obviscating python code for distribution Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2011-05-20 07:04 +0000
                Re: obviscating python code for distribution Hans Georg Schaathun <hg@schaathun.net> - 2011-05-20 09:54 +0100
                Re: obviscating python code for distribution harrismh777 <harrismh777@charter.net> - 2011-05-20 15:24 -0500
                Re: obviscating python code for distribution geremy condra <debatem1@gmail.com> - 2011-05-20 15:45 -0700
                Re: obviscating python code for distribution Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2011-05-21 00:54 +0000
                Re: obviscating python code for distribution harrismh777 <harrismh777@charter.net> - 2011-05-20 23:26 -0500
                Re: obviscating python code for distribution Steven D'Aprano <steve+comp.lang.python@pearwood.info> - 2011-05-20 07:10 +0000
                Re: obviscating python code for distribution geremy condra <debatem1@gmail.com> - 2011-05-20 09:26 -0700
                Re: obviscating python code for distribution Nobody <nobody@nowhere.com> - 2011-05-20 18:48 +0100
                Re: obviscating python code for distribution Chris Angelico <rosuav@gmail.com> - 2011-05-20 11:33 +1000
                Re: obviscating python code for distribution geremy condra <debatem1@gmail.com> - 2011-05-19 19:30 -0700
                Re: obviscating python code for distribution Chris Angelico <rosuav@gmail.com> - 2011-05-20 12:35 +1000
      Re: obviscating python code for distribution Chris Angelico <rosuav@gmail.com> - 2011-05-19 03:24 +1000
        Re: obviscating python code for distribution John Bokma <john@castleamber.com> - 2011-05-18 12:31 -0500
          Re: obviscating python code for distribution Chris Angelico <rosuav@gmail.com> - 2011-05-19 03:52 +1000
      Re: obviscating python code for distribution geremy condra <debatem1@gmail.com> - 2011-05-18 10:40 -0700
      Re: obviscating python code for distribution Chris Angelico <rosuav@gmail.com> - 2011-05-19 04:07 +1000
      Re: obviscating python code for distribution "Littlefield, Tyler" <tyler@tysdomain.com> - 2011-05-18 12:26 -0600
        Re: obviscating python code for distribution harrismh777 <harrismh777@charter.net> - 2011-05-18 21:54 -0500
          Re: obviscating python code for distribution geremy condra <debatem1@gmail.com> - 2011-05-19 10:50 -0700
            Re: obviscating python code for distribution harrismh777 <harrismh777@charter.net> - 2011-05-20 01:17 -0500
      Re: obviscating python code for distribution Dotan Cohen <dotancohen@gmail.com> - 2011-05-18 21:30 +0300
      Re: obviscating python code for distribution Dotan Cohen <dotancohen@gmail.com> - 2011-05-18 21:31 +0300
      Re: obviscating python code for distribution Chris Angelico <rosuav@gmail.com> - 2011-05-19 04:37 +1000
      Re: obviscating python code for distribution Chris Angelico <rosuav@gmail.com> - 2011-05-19 04:49 +1000
      Re: obviscating python code for distribution geremy condra <debatem1@gmail.com> - 2011-05-18 14:47 -0700

csiph-web