> You aren't aware just how many security-critical C programs invoke potentially undefined behaviour today.
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.
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.