Security, parallelism

[Tril]

On 1 Jan 1999, Laurent Martelli wrote:

> >>>>> "Tril" == Tril  <dem@tunes.org> writes:
>     Tril> In TUNES you can control the access to any thread at a very
>     Tril> fine grain.  (and using any program to determine the access
>     Tril> restriction) You don't have to lump priviledges together
>     Tril> like in UNIX.
> 
> Well, I think that threads or processes are just an implementation
> trick to give the impression that you have parallel execution. But I
> don't consider them as a good high level abstraction. 

Currently we have the "procedure" as a high level abstraction for serial
execution.  It consists of an ordered collection of instructions.  The
"ordered" property of the collection means there is a relation of
"sequence" between every two consecutive members of the collection.

In the new system, use an unordered collection of instructions. 
"Unordered" means no relation of sequence exists, therefore no dependency
of one instruction on the previous.  Where there is no dependency, the
compiler can assume the instructions can be scheduled in parallel.  It
seems pretty simple to me, but all languages (?) seem to include an
implicit dependency of serialization between every instruction, which is
why it is so hard to program parallel software.

It also would help to have meta-programming utilities which can take an
abstract algorithm, and translate it into any number of threads of
execution.  That would be hard, but possible if the language didn't imply
dependencies.

>     Tril> Communicating with untrusted systems, well, can you give an
>     Tril> example?  Data can be verified once imported into the
>     Tril> system...
> 
> I was referning to the fact that you can execute some code which you
> don't know exactly what it does (cf applets). It is executed with your
> rights, and can therefore mess with private data. In fact, this is
> rather a problem of trust. 

I shall assume that applets are distributed in source form, and before
being installed they are verified that they are not dangerous, by programs
which examine the source code.  This should be made easier with
specification languages and interactive program provers.  The applet can
be distributed with a proof that it is not harmful.  Proofs are structures
which can be verified more quickly than they can be generated, so they are
a contribution to "speed".

> One possible way of handling this without having to look at the code,
> would be to use post conditions. They are supposed to describe what
> the code do, so if we can check that the post condition is verified,
> we know that the code is correct. 

Proofs are a kind of post conditions.  The main program's specification
has pre- and post-conditions for the entire body.  Then each instruction
has individual pre- and post-conditions.  This is called axiomatic
semantics if anyone is interested in researching it.  I have found
descriptions of it in every book I looked at on programming language
concepts.

> But there's however a problem : how
> can you be sure that the code does not do more than what it is
> supposed to do?

That sounds like a hard question.  I think the best answer is to not have
any code at all, only the specification.  My answer seems very confusing.
How about this: Every program is broken down into pieces, right?  Each
piece has a precondition and postcondition.  Well at some point there are
axioms.  These are basic operations that aren't broken down into smaller
pieces.  In fact all they consist of is a precondition and a
postcondition.  (Usually they have a name, too, but see my other posts for
my ideas on getting rid of named functions.)  Because axioms are not
broken down, you don't have their source, and you don't know how they
work.  You just assume they do.

All the axioms are implemented on your computer, and you have already
decided that they do what they say. (By trying it over and over, or
reading the source)

I guess my answer boils down to, "If the source is distributed, can't you
always tell that the program does what it says it does, by looking at the
source?"  And you can still examine the binary even if source isn't
distributed.

David Manifold <dem@tunes.org>
This message is placed in the public domain.