On 11/11/23 4:16 PM, Keith F. Lynch wrote:
> Tim Merrigan <
tp...@ca.rr.com> wrote:
>> "Keith F. Lynch" <k...@KeithLynch.net> wrote:
>>> I'd much rather rely on code that's written to be free of security
>>> bugs in the first place.
>
>> They will never find and fix all the bugs, because they're not
>> omniscient, and can only fix the bugs they find, often by end users
>> reporting them, (possibly introducing new bugs in the process, being
>> fellable humans, and all).
>
> Code is made of basically the same stuff as mathematical theorems.
> Do you also believe that there are undetected bugs in all theorems,
> i.e. that there's nothing we know for certain about math? Flaws are
> sometimes found in theorems, but it's very rare (not counting theorems
> "proven" by crackpots).
>
> The "millennium problems" each offer a million-dollar reward for
> proofs or disproofs of various conjectures (e.g. the Riemann
> Hypothesis). To avoid risk, they require that the work be published
> in a reputable peer-reviewed journal, and that nobody finds a flaw in
> the first two years after publication.
An application to perform a real-world task has little similarity to a
mathematical theorem. "Proving the correctness of a browser" is a
meaningless phrase. A complex application with a user interface deals
with an open-ended set of user inputs, third-party code, and system
services.
Any key-based encryption system is, from a theoretical standpoint,
already defective. Given infinite computing resources and time, you can
break it. Whether something is a bug or not is often a question of
whether it's good enough. This changes over time. Encryption that was
effectively unbreakable in 1995 may be hopelessly weak now.
The number of combinations of inputs, data, and environmental factors is
too large for any mathematical demonstration the they're all bug-free.
This isn't to deny that a lot of code is much sloppier than it has any
right to be. The main reason is feature bloat. Browsers would be much
more secure than they are if they just didn't support JavaScript. Giving
anyone in the world the power to run code on your computer created a
minefield that can never be fully cleaned up. But people want all those
features.