It doesn't take much experience with C to appreciate something of the magnitude of difficulty of keeping a million lines of C UB-free. I'm not in the security field, but if the code there is anything like the codes I've worked with, I'd be surprised to find even a "security-critical" C program of any appreciable complexity that doesn't invoke undefined behaviour.
>Every time you write '+' in a C program between two signed values, do you do an overflow check beforehand?
Personally? I use signed scalar arithmetic very rarely. The bulk of the arithmetic I do is with unsigned integers (bit vectors, really) and arbitrary-precision integers. In fact, essentially the only time I do use signed scalar arithmetic is when I can determine statically that it won't overflow. Signed integer overflow is a bitch, UB optimizations or no.
>Or do you do a global dataflow analysis of the program to prove that it can't overflow?
That's the basic idea behind seL4, for example.
>Arguing for a technical correctness that is observably almost impossible to achieve in the wild is what's really pointless.
Sure, but only because everyone writes their security-critical programs in a language that couldn't more effectively impede security if it were designed to do so. Could a "friendly" dialect help? Maybe, but the proposed changes are far from sufficient to make formal verification feasible, and frankly, I don't know how seriously I can take "security-critical" without formal verification.
But UB isn't the problem here. You can make two's complement wraparound the defined behavior, and programs which fail to check their arithmetic are very likely to be wrong.
This is already the case with unsigned overflow: it's defined to wrap around. Yet many many programs are vulnerable because they do something like malloc(nitems * size) and carry on thinking they must've gotten the wanted amount of memory.
Most of the time, you really have to do the right checks whether your arithmetic is signed or not. Whether wraparound is defined or not.
In any case, I'm bored of discussing this with people who haven't studied the problem.
Every time you write '+' in a C program between two signed values, do you do an overflow check beforehand? Do you know what it takes to write that overflow check? Or do you do a global dataflow analysis of the program to prove that it can't overflow?
Saying that 95% (at a conservative guess, IMO) of C programs out there are wrong makes for a strong argument for this proposal, not against it. Arguing for a technical correctness that is observably almost impossible to achieve in the wild is what's really pointless.