[cap-talk] Memory Safety (was: Midori in The Register)

[Mark Miller]

On Wed, Aug 6, 2008 at 6:52 AM, Jonathan S. Shapiro <shap at eros-os.com>wrote:

>
>  A C program that is successfully checked by some checker imposing
>  stronger guarantees than C ensures can be type safe, even though C as
>  a language does not structurally ensure safety.


If there is an automated predicate V (for verify) such that for all source
S, if V(S) implies "C(S) is memory safe", then C as guarded by V effectively
forms a memory-safe language. I took Ben's "circumvents" comment as an
admission that there is no such automated predicate V.


>
>  A statically compiled ML program is generally considered safe, even
>  though a user could link arbitrary ASM code into the binary and
>  execute that. Also the ML runtime is written in an unsafe language.


Neither of these render ML itself memory unsafe. However, OCaml at least is
memory unsafe anyway, by virtue of publicly callable entry points in the
library such as Array.unsafe_set. OCaml as guarded by the Emily verifier is
memory safe. (It is also ocap-safe, but that's an additional matter.)


> My point is only that the term "safe" should not be interpreted to apply
> only to programs that are safe by virtue of structural language
> constraints.
>

If an attacker can pass all automated tests and still violate memory safety,
then we should consider that platform to be memory unsafe.

If we have automated tests that guarantee memory safety, then the language
as guarded by those tests becomes a new language that's memory "safe by
virtue of structural language constraints".

I say "memory unsafe" rather than "type unsafe" above because the latter
phrase should include any violation of the type system even if it doesn't
allow violation of memory safety. For example, AFAIK, Haskell is memory
safe. But Haskell is type-unsafe by virtue of the unconditional availability
of unsafePerformIO.

-- 
Text by me above is hereby placed in the public domain

Cheers,
--MarkM
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.eros-os.org/pipermail/cap-talk/attachments/20080806/5af7e481/attachment.html