From: Christian Wettergren <cwe@it.kth.se>
Date: Mon, 16 Oct 95 03:27:58 PDT
To: Frank Stuart <fstuart@vetmed.auburn.edu>
Subject: Re: [NOISE] was Re: java security concerns
In-Reply-To: <199510100639.BAA19818@snoopy.vetmed.auburn.edu>
Message-ID: <199510161024.LAA11745@piraya.electrum.kth.se>
MIME-Version: 1.0
Content-Type: text/plain



| This is a bit off-topic, but hopefully interesting.
| 
| Rather than trying to prove a program to be correct (which I agree is doomed
| to failure for the forseeable future for all but trivial programs), perhaps
| it would be useful to have an automated therom-prover to try to deduce
| "interesting things" about certain programs such as "this program always
| bounds-checks its input", "this program allows writes to arbitrary files on
| lines x, y, and z", "this program halts". (:>)

I'm doing a PhD on runtime information flow analysis of programs,
tracking each datum and who has contributed to it. Each datum has an
associated set of subjects that has contributed, and each system call
checks whether all subjects in the set are granted the call or not.
This tracking is done by compiled-in 'shadowing' code, compiled in
into the binary, and the code is inserted based on something similar
to 'data flow' analysis.

Its messy, but I think it might work out in the end. This kind of
access control is much better suited for extensive communication
between different subjects than the current paradigm of having
an owner of the process. 

With the current concept, it is imperative for the process to
filter and controll each datum entering the process, since it might
be 'hostile'. (The current concept of identity is really based on
*partitioning* an expensive computing facility, without communication
between the different partitions.) I believe this task to be to 
burdening in the long run.

With "my approach", you can accept any input without fear, since
it will be stopped when your application does the syscall.

I just started, so I don't have anything concrete yet. I'll have it 
in five years! :-)

| Obviously (as the last example illustrates), this isn't perfect because
| something can be true without being provable.

Why ever prove anything else but a trace of actual execution? This is
usually almost trivial, you don't have the problem of calculating the
proof for all possible branches, etc...

| Further, it's likely that assumptions must be made about system calls, 
| libraries, and the  ways in which they interact.  

It might be fruitful to do it for an actual system, although I think
that this "paradigm"-shift will influence a lot of the design of the
system.

| However, I think such a tool would be useful because 
| it may quickly point out things not obvious to (most) humans
| and getting some idea of what can't be deduced and why would be instructive.

Tell me if your planning to do something along these lines, it would
be most interesting.

Regards,
	Christian