[erlang-questions] where did my code come from?

[Jesper Louis Andersen]

On Wed, Sep 14, 2011 at 01:29, David Goehrig <dave@REDACTED> wrote:

> My suspicion is in the long term systems will continue to be so complex no
> one will be able to verify trust, and we'll adapt by living with a certain
> level of insecurity and abuse.

Well, there is one way out, but it is not particularly implemented,
nor easy to pull off. George Necula has written a paper on
proof-carrying-code. Here is the trick.

We start by setting up a security policy. The SP has to be formally
specified since we want a machine to check it. Necula does this for
out-of-bounds memory checks, but you can in principle do it for any
security predicate you want, as long as you are able to make a
formulation of it formally. When we all agree on an SP, the next step
can begin.

The author of the code is obliged to pass two things. The code C, and
a proof P which states that the code obeys the SP. From C a set of
verification conditions are extracted which must be true for SP to
hold. The proof P is a list of how to show these conditions to be
true. How the author comes up with P is interesting. Basically you can
have the compiler infer everything about P you need. In a case the
compiler can't prove something, for a memory access it won't be able
to prove it is not out-of-bounds, the compiler inserts enough checking
so it is able to carry out the proof. This is mostly mechanical. The
proof is output as an Oracle stream which allows us to compress the
size of the proof down. The idea is that the oracle stream provides a
set of hints about what to do if an automated proof checker gets
stuck.

The user of the code gets C and P. He then proceed by using a
verification condition generator on C which tells him what conditions
need to be true - the same generator which the author uses. And he
uses P on the conditions to check that the proof actually is the right
one. If the proof goes through, he may use the code.

The beauty of the approach is that the user of the code does not have
to trust the author. They only have to agree on SP. If the Code is
altered, the Proof may or may not work. If it works, it is still safe.
If not, we can reject the program. If the proof is altered, it may or
may not work. if it works, it is still safe. If not, we can reject the
proof (and thus the program).

Now, it is a 10 year old idea. So why hasn't it seen more use? For
one, it requires some compiler tech support. Then there is the whole
part about SP, which can be pretty nasty to build up. My bet is that
it has to incubate for more years, until our knowledge about
mechanical theorem proving is better.

But a dreamy vision it is! It would allow us to distribute code over
the internet, and execute code from untrusted sources, just by
checking that the proof they provide is correct.


-- 
J.