Tony Morris

The thing is, brains do that. Nature does that. Physics does that. As Dan Geer says, security is the absence of unmitigatable surprise.

All abstractions are leaky because they encode implicit assumptions. Attempting to make all assumptions explicit creates awkward pedantry that *still* leaks, because thought transfer is a lossy process. Conversational vs. legal verbiage. I'm thinking clearly about the unclear.

Reminds me of testing's finding, "All oracles are heuristic". There are no perfect tests that can always separate the working from the not-working.

Yes there are. They are called proofs.

With no side channels?

What is a "side channel"? Proofs show correctness, to the point that there is nothing left to show. It is correct.

After reading the rest of the thread, are you talking about a Lambda Calc proof of an implementation? I'm interested to see an example or two. Side channels from the hardware your implementation runs on make the proof heuristic. On paper it's perfect. On silicon, less so.

They emit information through EMF. They constrain where none exists in the proof. Formally verified algorithms get owned all the time by unseen constraints. That's why all abstractions are leaky and all oracles are heuristic. Gödel's Incompleteness is related.