[Cryptech Tech] Fwd: verification of design

[Randy Bush]

From: Sandra Murphy <sandy at tislabs.com>
Subject: verification of design
Date: Thu, 6 Nov 2014 09:29:09 -0500
Message-Id: <0639F902-E735-4A47-90DC-37F110182447 at tislabs.com>
Cc: Sandra Murphy <sandy at tislabs.com>
To: Randy Bush <randy at psg.com>

Speaking as someone who was decades ago involved in code level
verification.

Hardware verification was (at the time) one of the more successful part
of automated verification.  A very bounded problem.

But an outstanding problem in verification was proving the absence of 
anything except the modeled algorithm

So really hard to prove that a non-deterministic step was not being 
implemented deterministically, for an inference path.

If there's some feature that is not part of your model of the computing 
environment, your formal verification will not spot changes in that 
feature.

So timing used for information leak can't be disproved in a model that 
doesn't include that.

I don't know that the verification research has gotten beyond that while 
I have not been looking.

--Sandy