Re: NSA back doors in encryption products

[David Honig]

At 12:39 AM 5/25/00 -0700, Eugene Leitl wrote:
>less bits to look at than your average Unix box. Can one prove
>behaviour of small VHDL circuits these days, anyone knows?

You can prove that two descriptions (e.g., C & RTL & gates) are
functionally equivalent; harder to prove they don't do anything
else :-)

Formal verification is a holy grail.

There's a few commercial chip strippers that have the reverse-engineering
tool flow understood, who can go from microscopy to netlists.  E.g.,
chipworks.com IIRC