Re:Checked C
by pron on Friday February 19, 2021 @07:08AM
(#26192241)
> so the lowest effort path will necessarily involve refactoring it until it does. And that means that rewriting it altogether into a new language has very few drawbacks, and some additional benefits.
No, because while some refactoring is necessary, it is virtually always local. E.g. if the sound checker can't prove that an access is within an arrays bounds, adding a dynamic test just before it (assuming you don't want to add annotations to help the checker) will make it provable.
Rewriting in a new language is certainly one way to reduce or eliminate memory errors, but if your goal is to reduce or eliminate memory errors in existing codebases, there are other ways that are cheaper, more proven, less risky and are applicable to more environments. These tools are already much more heavily used in safety- and security-critical codebases than any new language, so people are slowly getting good experience with them.
Re:Checked C
by mlindner on Friday February 19, 2021 @10:56AM
(#26194430)
I’m not sure what C code bases you’ve worked with but refactoring in a large C code base is almost never local. Especially if it’s a code base that made extensive use of the gcc flags that disable making sure code does not alias.
Re:Checked C
by pron on Friday February 19, 2021 @05:19PM
(#26198764)
Providing enough information for the prover does not require a big refactoring, and is significantly cheaper and less risky than a rewrite for an established codebase.
No, because while some refactoring is necessary, it is virtually always local. E.g. if the sound checker can't prove that an access is within an arrays bounds, adding a dynamic test just before it (assuming you don't want to add annotations to help the checker) will make it provable.
Rewriting in a new language is certainly one way to reduce or eliminate memory errors, but if your goal is to reduce or eliminate memory errors in existing codebases, there are other ways that are cheaper, more proven, less risky and are applicable to more environments. These tools are already much more heavily used in safety- and security-critical codebases than any new language, so people are slowly getting good experience with them.