Re: Thoughts on provably secure systems

Well...I've gone away and done some reading and thinking and come back
with this:

Type systems/proof systems attack the problem at a high level, true.

You can't simply abstract the entire machine. This violates Godel's theorem.

If your language is a full Turing machine, you cannot bound resource usage.
Necula mentions it in his thesis about type-safe programs, and you restate it
as proofs=types. My idea of compiling code into blocks and passing blocks
to the OS allows a scheduler (actually, a security checker in this case) to be
inserted at necessary points in the program flow. Basically, I've sugar-coated
a run-time security check around the idea of providing a necessary service
(scheduling).

There's no reason that scheduling couldn't be provided in user-level code
except that we'd probably violate data encapsulation if programs were
open about their resource (CPU time) needs. We could black-box this (hide
the program details). Then you can still derive derivative information (by
watching for patterns in the black boxes), which gets us into the same kind of
encryption games that people have already been working on for such
purposes (such as randomizing the patterns of e-mail transmissions from
anonymous email forwarding sites).

You lose the ability to have a full Turing machine BUT you can come pretty
close to it if you restrict resource usage in some way such as restricting
resource usage to consumption only (no releasing such as revoking a
capability). This makes resource usage a type of monotonic increasing
problem, which has been solved. It goes in 2 steps:
1. Prove that resource usage is only increasing.
2. Prove that it is bounded.

I haven't read the references yet but I assume this is the "linear typing" idea.

The question becomes...the resulting system is resource bounded, and
that it will be strictly decidable. It will be possible to avoid the stopping
problem (condition #2) since this must be proven. It's not a full-fledged
Turing machine. I think at worst, we can code programs in such a way that
we'd have something like the following (in pseudo-C):

i=0
while (i < 10000) {
    Do some operation where the execution time is not statically determined;
    i++
};
if (i=10000) return(ERROR---did not finish);
...

i is a bogus variable present only to bound loop execution in a case
where execution is indeterminate.

My three cases (terminates, bounds known; terminates, bounds not easily
determined; does not terminate) fall apart into whether programs fail one
or both conditions on resource bounds.

By way of example, I think we can show that although the allowable
programs are strictly not fully general (not representative of a Turing
machine), that this limitation in the model is not sufficiently restrictive
that it will be a major problem. And since we've specified the fundamental
flaws in the computational model up front, we won't run afoul of Godel's
annoying theorem...which gets back to your linear/multi-linear typing.

Reference for LXres that I mentioned:

The problem with LXres is simple...we've pushed the representation of
resource bounds to the meta-level. In itself, this is not a fundamental
problem. The problem is that we have not also similarly created resource
bounds at the meta-level by making the meta-language fully general.
So I could probably construct a meta-program that violates resource
bounds, although the underlying program itself may not have to do so.
LXres is thus not safe.

I also thought of nesting. This means that you have a restricted language
to describe the resource needs of your meta-language. Then the meta-
language executes (such as LXres) to describe the resource needs of
the underlying program, which finally gets executed if the security checker
lets it through. However, once again this goes back to Godel's theorem
and I see no real need for more than 1 or 2 levels of this kind of stuff
except as a convenience with respect to abstraction.

The way I see it, there will always be an OS somewhere in the machine
because you can't fully provide the machine in abstraction without also
living with fundamentally weak security. Thus, there must ALWAYS be a
trusted kernel if the OS enforces the most basic security requirement
which can be reduced down to simply obeying resource bounds. The
question is just how small can we make that kernel in terms of resource
usage. I think we can safely answer the question:

1. Kernel resource usage is always unbounded by definition (it runs in
a fully generalized computational model...on a Turing machine).
2. To enforce ALL resource bounds, all programs must run in a
restricted computational model. The model can be enforced at run time
(using system calls or a variety of other techniques) or it can be
enforced statically at load-time (whatever form this takes).

It remains to be determined whether static or dynamic (run-time)
enforcement has a lower computational cost. However, at a first pass,
it seems obvious that static checking would always be preferable
because the resource cost of static checking can be amortized
over each execution of the program. The final question (which is
what the TUNES and EROS projects have as sub-projects) is the
determination of HOW to do this.

I know this is long and rambling...but it seems that these
fundamental questions need to be made more clear and given
strong consideration by OS/language designers. If that were not
the case, I wouldn't run 99% of the time with Java turned off in my
browser because I don't trust the sandboxing in the browser and
I've run into a lot of sites that violate resource usage in terms of
CPU, causing all kinds of havoc in my web browser.