[trealira]

> Moreover, it is untenable to maintain a small island of "secure software" for "important things" in a vast ocean of careless and vulnerable code. Inevitably, the island gets infected, and not even air-gaps can save it, as stuxnet showed.

Why is it inevitable? As long as it doesn't connect to other software (via internet or other means), isn't it possible to formally verify one critical software component, e.g. in pacemakers?

I'm not saying that C would necessarily be the best choice for formally verifying it, though.

[PH95VuimJjqBqy]

more than that, you only have so much time and money, concentrating on more important pieces allows you to be more thorough where the highest impacts are.

perfect is the enemy of good, "security" people act as if all breaches are equally relevant.

When your surface area is everything you're more likely to have holes, that's just a law of nature. Limit your surface area and suddenly you can be more thorough.

[SenAnder]

Formally verifying does no good if the compiler is infected. In the stuxnet example, formal verification wouldn't even help - how do you formally verify centrifuge timings?

Unlike what your sibling comment claims, I'm not saying all software is equally important, or must have equal effort invested in securing it. But insecurity absolutely is infectious, and the more insecure the general environment is, the harder it is to secure a small part of it.

For example, you'll want a compiler. How secure is the web stack of the page that delivers your gcc/clang? How secure is its host's infrastructure, and of the DNS provider? The browser you're downloading it with? Did you ever visit any other page that might have compromised it? What about your text editor, your OS, the SDK you're using to flash code onto the pacemaker.. And all of them have vast supply-chain networks.

[trealira]

Hopefully, for the pacemaker, the authors of the code would be using a verified compiler like CompCert (although it's only verified for the compilation, not the parsing or the preprocessor), but you don't have control at every level, like for the hardware. You can't verify centrifuge timings, but you can specify software and verify that it fits the specification to the point that it won't be the point of failure (assuming you have everything under control, like the pacemaker SDK, everything). I do see what you're saying about it being infectious, though.