Re: "Perfect" or "Provable" security both crypto and non-crypto?

From: Paul Rubin (//phr.cx_at_NOSPAM.invalid)
Date: 09/17/04 

Date: 16 Sep 2004 15:08:09 -0700

"Douglas A. Gwyn" <DAGwyn@null.net> writes:
> > You check the context; the definition of 'a' wasn't part of your
> > template.
>
> And many other things were missing, too. I thought it would be
> obvious what I was saying, but since you're so fixated on concretes,
> you missed the idea being expressed.

Well, yes, formal verification deals with the concretes. And the idea
being expressed is still wrong. Even if "a" is an array with a fixed
location, if "i" is a local variable, it lives in the current stack frame,
and the "do_something" function can reach upward and change it.