I agree that C code can be made correct with somewhere around 10x the effort folks normally put into writing C code, and that one of the ways that you could profitably spend that extra effort is formal verification (though very good testing or auditing discipline could work too).
Conversation
My claim is that it actually takes less effort. Rather it takes abandoning your ideas that doing clever tricks is going to make your code more efficient.
1
Eliminating 90% of memory corruption bugs with clean, well-written C code and proper usage of tooling like UBSan and ASan isn't good enough or comparable to providing memory safety. Full memory safety can be provided for C without proving all the code formally correct.
1
Either write it in a subset with annotations specifically to take advantage of memory safety verification (which would not be far from what you want to write naturally in clean code most of the time, but with some adjustments and annotations) or have the compiler do it.
1
Even a project like SQLite with a huge amount of testing / dynamic analysis tooling applied to it still has serious vulnerabilities caused by memory corruption bugs.
sqlite.org/testing.html
It's important to make a small TCB for these kinds of issues.
2
That claim sounds implausible - the memory usage patterns should not be a function of untrusted input.
1
SQLite still has memory corruption bugs. A subset of those are vulnerabilities. I can link to some of the recent ones, but I don't feel that's necessary. I don't see how it's implausible that C code is still going to have edge cases not totally handled leading to mem corruption.
1
I think it sounds more plausible that someone thought "you feed a corrupt sqlite db file to it" is a CVE, when accepting untrusted db files is not the intended usage.
1
That is the intended usage of SQLite. That's part of the threat model for it in the real world and it certainly aims to be safe in that case. It's also supposed to remain memory safe with a lot of attacker control over the database queries.
1
1
This Tweet was deleted by the Tweet author. Learn more
I didn't say running untrusted SQL. I said "a lot of attacker control over the database queries". If I meant executing arbitrary SQL, that's what I would have said, and I clearly didn't mean that. Please don't misrepresent my statements any more.
sqlite.org/whentouse.html
> SQLite does not compete with client/server databases. SQLite competes with fopen().
#2 on list of recommend uses
> Application file format
Also listed:
> Data transfer format
And yes, it is widely used this way in the real world, as intended.
1
1
I believe you. This is a highly irresponsible recommendation, both from a security perspective and a design one, and ppl should ignore it.