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

Mike Samuel mikesamuel at gmail.com
Wed Aug 6 16:16:19 CDT 2008


2008/8/6 Mark Miller <erights at gmail.com>

> 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.
>

It seems odd for a definition of type safety to depend on the definition of
attacker.  Specifically, if Apache contributors are assumed not to be
attackers, does that change whether or not apache is type-safe.




> 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
>
>
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.eros-os.org/pipermail/cap-talk/attachments/20080806/2b29808a/attachment.html 


More information about the cap-talk mailing list