Originally posted by liam
View Post
That also requires that the specification is correct. One university project to produce programs proved via formal logic succeeded. But they had to revise their specification over 400 times. Showing that formal proof just moves the problem higher up. People don't always understand how to ask for what they actually want.
And that does not include hardware errors which may be inherent in the design or happen via electromagnetic interference.
One hacker took down a formally proved smart-card security chip by applying heat until it began to malfunction. And several fancy electronic biometric key locks have been defeated by inducing a signal into the unlock wiring through induction, bypassing the whole authentication system. And of course several attacks against passwords and hashes based on getting data via hyperthreading, cache misses, page faults, context switches and just timing information generally.
Comment