3 ms·
Formal correctness proofs are both unattainable and insufficient. We don't know how to do it at the required scale, and it doesn't save us from flawed formal sp
by fulafel 5y ago
Formal correctness proofs are both unattainable and insufficient. We don't know how to do it at the required scale, and it doesn't save us from flawed formal specifications, we'll have the bugs in the formal requirements instead of in the code.
There are more cost efficient and proven ways to effectively address these kinds of vulnerabilities, like limiting complexity, using programming language features to eliminate classes of bugs, using other verifiable engineering disciplines, and compartmentalisation. Proofs also have their place locally in verifying small components. But making this commercially viable would large numbers of customers and users who are willing to make big compromises in functionality, features, third party apps etc.
- nine_k 5y agoLimiting complexity is often not an option, because the complexity is of the subject area. Things like image format decoders are easiest to produce formal analysis and proofs for. It's sadly still too expensive and slow to produce. Fuzzing as a mandatory testing step could be useful in some cases. I agree about bugs in specifications though :(
- fulafel 5y agoIn this case limiting complexity would have worked: don't support frivolous amounts of image codecs (like the fax format here), just support 1-2, and make sure there is high assurance of the safety using known methods (security oriented code design, memory safe language, fuzzing, and sandboxing).