On Fri, 17 Nov 2000, Felix von Leitner wrote:
> Software security _is_ easy.
> The correct paradigms have been published for decades.
And ignored by most people for decades. :)
> Had you actually read the Schneier, you would know that no testing in
> the world can prove the security of a system. Testing can only prove
> that a system is not secure.
Unless a finite set of tests can exhaust all the desired behaviour of the
system. Most systems are not finite in this sense but a few are. (Anyway,
I guess that he meant testing in a wider sense.)
> And source code is a formal representation of an algorithm, not a proof.
There is a thing called Howard-Someone correspondence (I can't recall the
second name now, sorry) translating logical formulas to lambda terms and
vice versa. This can be used to show that proofs of theorems of a certain
form correspond to programs (i.e. lambda terms) and programs correspond to
proofs.
--Pavel Kankovsky aka Peak [ Boycott Microsoft--http://www.vcnet.com/bms ]
"Resistance is futile. Open your source code and prepare for assimilation."
