[cap-talk] Memory Safety (was: Midori in The Register)
benl at google.com
Wed Aug 6 11:28:42 CDT 2008
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>
>> 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
More information about the cap-talk