Re:Prossimo – Memory safety for the Internet's most critical...
by tialaramex on Saturday June 19, 2021 @08:11AM
(#27559816)
> MISRA C, model checkers and theorem provers all exist to provide some of these guarantees that are, to my knowledge, widely recognized in applications where “safety” actually entails life safety.
So, where do I get the version of curl or similar that in fact provides "some of these guarantees" ? Because ISRG isn't spending money on developing software for the Ford Bronco or US aircraft carriers, it is spending money on curl.
MISRA C like a long list of other projects for C or C++ including Bjarne's "Core Guidelines", goes like this:
1. Classify things people will end up needing to do as sinful.
2. Offer them a mechanism to obtain an indulgence, knowing this mechanism will quickly be exhausted.
3. When inevitably this results in tragedy point back at item (1) which absolves you of responsibility.
Example #1, MISRA says you mustn't have any unreachable code. Of course deciding whether code is actually reachable requires solving the Halting Problem, so your automated tooling doesn't do that and will either just flag code that might or might not really be unreachable (useless noise that reduces development velocity) or ignore MIRSA here and just leave your programmers to try not to do this, the status quo ante.
MISRA often needs to dish out "permits" to violate their guidelines because, in practice, the guidelines are too strict to be usable and somebody's workplace requires the guidelines so... the alternative is incredibly creaky and likely unsafe code that's "compliant" - or a "permit" to just ignore a guideline. This is most common when the language doesn't provide a sane way to do something.
Example #2, MISRA forbids hiding variables. If the inner scope has a variable named 'counter' and so does the outer scope, programmers are likely to get confused and mean one when the other is actually in scope, the language compiler won't stop this. But MISRA has to issue a permit because C macros routinely do this and so if your static analysis tool looks at the code it sees lots of such re-use that was (hopefully) harmless.
But if you have hygienic macros (Rust declarative macros) then this isn't a problem, the hygienic macro can't accidentally shadow variables. So you don't need these acrobatics in Rust, if you want to ban shadowing, you can do that and not have weird knock-on effects in macros.
Example #3 MISRA forbids invariants from appearing as conditionals. MISRA reasons that you couldn't possibly have meant to check that buffer != NULL because you know you set buffer in the constructor, and so this is a coding error. But of course you wrote that because you're worried that a bug elsewhere might null out the buffer and blow up the whole system... So now your static analysis tool is screaming that your defensive coding violate MISRA. Do you go ask the Boss for authority to ignore this rule? Or do you rip out the defensive checks?
Tools like F* and WUFFS are different because they've intentionally set their sights low. If you say you want to write the software for your Jet Fighter in WUFFS its authors will carefully explain that this can't be done, and they don't want to help you try. They solve small, well-specified problems in a constrained problem space. They do it very well, you should use them when they're appropriate. They can't be used to replace curl.
So, where do I get the version of curl or similar that in fact provides "some of these guarantees" ? Because ISRG isn't spending money on developing software for the Ford Bronco or US aircraft carriers, it is spending money on curl.
MISRA C like a long list of other projects for C or C++ including Bjarne's "Core Guidelines", goes like this:
1. Classify things people will end up needing to do as sinful.
2. Offer them a mechanism to obtain an indulgence, knowing this mechanism will quickly be exhausted.
3. When inevitably this results in tragedy point back at item (1) which absolves you of responsibility.
Example #1, MISRA says you mustn't have any unreachable code. Of course deciding whether code is actually reachable requires solving the Halting Problem, so your automated tooling doesn't do that and will either just flag code that might or might not really be unreachable (useless noise that reduces development velocity) or ignore MIRSA here and just leave your programmers to try not to do this, the status quo ante.
MISRA often needs to dish out "permits" to violate their guidelines because, in practice, the guidelines are too strict to be usable and somebody's workplace requires the guidelines so... the alternative is incredibly creaky and likely unsafe code that's "compliant" - or a "permit" to just ignore a guideline. This is most common when the language doesn't provide a sane way to do something.
Example #2, MISRA forbids hiding variables. If the inner scope has a variable named 'counter' and so does the outer scope, programmers are likely to get confused and mean one when the other is actually in scope, the language compiler won't stop this. But MISRA has to issue a permit because C macros routinely do this and so if your static analysis tool looks at the code it sees lots of such re-use that was (hopefully) harmless.
But if you have hygienic macros (Rust declarative macros) then this isn't a problem, the hygienic macro can't accidentally shadow variables. So you don't need these acrobatics in Rust, if you want to ban shadowing, you can do that and not have weird knock-on effects in macros.
Example #3 MISRA forbids invariants from appearing as conditionals. MISRA reasons that you couldn't possibly have meant to check that buffer != NULL because you know you set buffer in the constructor, and so this is a coding error. But of course you wrote that because you're worried that a bug elsewhere might null out the buffer and blow up the whole system... So now your static analysis tool is screaming that your defensive coding violate MISRA. Do you go ask the Boss for authority to ignore this rule? Or do you rip out the defensive checks?
Tools like F* and WUFFS are different because they've intentionally set their sights low. If you say you want to write the software for your Jet Fighter in WUFFS its authors will carefully explain that this can't be done, and they don't want to help you try. They solve small, well-specified problems in a constrained problem space. They do it very well, you should use them when they're appropriate. They can't be used to replace curl.