[cap-talk] C vs. Safety

[Jonathan S. Shapiro]

On Wed, 2008-08-06 at 00:54 +0000, Baldur Johannsson wrote:
> Þann 5 ágúst 2008 ritaði Jonathan S. Shapiro <shap at eros-os.com>:
> > On Tue, 2008-08-05 at 10:48 -0400, Jonathan S. Shapiro wrote:
> >> On Tue, 2008-08-05 at 14:10 +1000, James A. Donald wrote:
> -snip-
> >
> > The goal, of course, is *static* safety, and that is considerably harder
> > to achieve. Still, it isn't unimaginable.
> >
> Hmm... isnt static safety as unsolvable as the famous halting problem?
> That is the question: does program p ever do anything unsafe?

It is certainly NOT as unsolvable as the halting problem.

> and what exactly is safety in this context, please?

Thanks. By safety, here, I mean "type safety", and therefore "memory
reference safety".

> as far as I understand it, safety is about limiting programs access
> both to resources and other components of the computer system.

Not so. First, "safety" in the absence of other qualification generally
refers to type safety. More generally, safety is with respect to some
property, and a program is safe w.r.t. that property if the property is
satisfied under all terminating executions of the program. A program is
*statically* safe w.r.t. a property if the determination that it is safe
can be made at compile time.

There are many safety properties that cannot be statically checked. Type
safety *can* be statically checked for a suitably designed language.

Safety is different from security, but safety is generally a
precondition to security in any language-based security scheme, because
language-based security tends to rest on the type system, which in turn
guards the integrity of the virtual machine. A program that can violate
the type system can compromise the virtual machine, and can therefore
violate any other safety property we might care to name.



shap