[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Provably Correct Crypto?
On Tue, 1 Aug 1995, Dr. Frederick B. Cohen was alleged to have blathered:
> Tim May mused:
> > Anything that "reaches out" to external libraries or utilities would then
> > have the vulnerabilities of _those_ libraries and utilities, which may or
> > may not be provably correct themselves. (And the issue of any PRNG being
> > probably correct or not is of course an interesting, and deep, question.)
> > I do think the issues of modular design and provable correctness--or
> > approximations to it--are interesting ones.
> I think that this issue can generally be addressed by a divide and
> conquer strategy. Prove that the called routines are correct and
> confined under all possible parameters, do the same for the calling
> routines, do the same for the interaction between them, and I think you
> have it. This is pretty easy for one or two routines, but when you take
> the OS into account, the C compiler into account, the program itself
> into account, and the external environment into account, you run into
> some serious limitations. For example, you may (in some cases) have to
> show that under all possible sequences of interrupt timings and stack
> conditions, the system operates correctly (which almost none currently
> do). Unless you design with this sort of thing in mind, it's very hard
> to demonstrate these properties even for limited subproblems.
After all your griping over PGP, you spout this? Have you ever heard of
Godel's theorem? I have a phrase for people who peddle their mark of
approval that a given large program will work: "Snake oil salesman". In
the messages which you have scrawled between this and the last on my
system when I caught up this evening, you have demonstrated the
fraudulent nature of your business by first claiming that certain
propositions were "demonstrated", then stating that a graduate student
was working on "proving" them.
I repeat: Snake Oil Salesman