[cap-talk] Memory Safety (was: Midori in The Register)
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
> 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
> cap-talk mailing list
> cap-talk at mail.eros-os.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the cap-talk