This whole thread of "safe" languages is rather troubling to me.
I spent more years than I care to count building secure operting systems,
often using formal models of security and performing various degrees of
proof of correctness on the software itself. In essence what we were
building were "safe" environments for the execution of unverified software.
The problems are these:
- One person's "safe" is another person's security violation -- in
other words finding an acceptable policy is very hard. (Denial of
service is a particularly hard concern to factor into a policy.)
In many cases, people don't state their security policy, either
formally or informally. This is a real problem, because without
a security policy, one can not judge whether
a) If the enviroment works as advertised, whether it is sufficiently
powerful to use for the desired job. (I.e. if the policy
has a 100% prohibition against inter-user data flow, then
that environment would not be useful to support a multi-user
chat application.)
b) Without a policy it is impossible to evaluate the
implementation of the abstract "safe" machine to see whether
it is, in fact, "safe" according to the policy.
- It takes work to gain sufficient trust that the policy is enforced
by the abstract machine, no matter what sequence of actions are
performed by the unverified software. Some people do this by making
the abstract machine very simple or very restrictive. (An example
of this is a calculator.)
But it takes more work to determine whether to trust the more
sophisticated abstract machines. You can test it, but it's
usually impossible to test all possible sequences of states that
the unverified software may cause. And formal proof of correctness
is something that is very hard to do.
- Sometimes the degree of trust of the "safe" environment can be
reduced by allowing it to run only programs which have been
examined and blessed. This is the argument that many people
make regarding the importion of source versus binary code -- if
you can inspect it you may feel safer about running it.
In a typical OS, such as Un*x, we've spent years trying to build a "safe"
environment in which users can write code which doesn't violate one
another's security. We're not there yet.
So we put people into restricted shells or application, which rather
limits the usefulness of the "safe" environment, often to the point where
the "safe" environment is useless as a vehicle to get the needed job
done.
Safe-TCL occupies this middle area. It tries to find a useful balance
between a restrictive environment and utility. For many people, this
balance is adequate. It is likely that over time, we will find that it
is, however, overly restrictive to support some new, imaginative,
multi-user applications.
I, for one, would like to see a policy defining what we want from a
"safe" environment.
I'll start off by asserting that such a policy should support
interactions between multiple users -- which implies that there can be
data flows between the users. (The reason I'm starting with this is that
WWW browsers like Hot Java or Sesame (?) can easily evolve so that the
users are interacting directly with one another through a matrix of
connections rather than through a shared server.)
--karl--