Limits of Enforcement

Something we in the security community seem to ignore is that it’s not enough to have an enforcement mechanism. Of course, you also need policies and you even need a semantics for those policies. But even with all of that, you still don’t have enough. Because security does not happen by accident; it requires careful design. And the real problem is that developers don’t get any help in designing software to be secure.

The fate of proof-carrying code seems like a case in point. Extremely cool and solid technology, with rock-solid enforcement and deep semantic underpinnings. But relatively little attention to how developers might produce software that was accompanied by proofs of properties that go beyond type safety (a property for which PCC is probably overkill).