[7204] in cryptography@c2.net mail archive
Re: NSA back doors in encryption products
daemon@ATHENA.MIT.EDU (David Honig)
Fri May 26 22:07:05 2000
Message-Id: <3.0.6.32.20000526074502.0080d140@pop.sprynet.com>
Date: Fri, 26 May 2000 07:45:02 -0700
To: Eugene Leitl <eugene.leitl@lrz.uni-muenchen.de>,
"Enzo Michelangeli" <enzom@bigfoot.com>
From: David Honig <honig@sprynet.com>
Cc: "Eugene Leitl" <Eugene.Leitl@lrz.uni-muenchen.de>,
"Rick Smith" <rick_smith@securecomputing.com>,
"Arnold G. Reinhold" <reinhold@world.std.com>,
"John Gilmore" <gnu@toad.com>, <cryptography@c2.net>, <gnu@cygnus.com>
In-Reply-To: <14636.55488.285821.179589@lrz.uni-muenchen.de>
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
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
