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

[Ben Laurie]

On Wed, Aug 6, 2008 at 3:53 PM, Mark Miller <erights at gmail.com> wrote:
> 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.

One of the motivations for what I was doing was to make it possible to
use Deputy on OpenSSL. Possibly the combination would provide that (if
one avoided certain Deputy constructs, which could be statically
verified).