5 ms·

Sure, just look at the languages that have more stringent type systems.

by lallysingh 7y ago

adrianN 7y ago
They don't really help me make the mountains of C we have in the world less buggy.
- lallysingh 7y ago
  C code doesn't have enough information in it to do a whole lot of mechanical analysis. Runtime analysis of its behavior is what you've got.
  - nickpsecurity 7y ago
    Have you never heard of program analysis for security? Genuine question. RVI, the Mayhem developers, and many others would strongly disagree with you: https://runtimeverification.com/match/1.0-SNAPSHOT/docs/benchmark/ https://runtimeverification.com/match/1.0-SNAPSHOT/docs/benc... https://spectrum.ieee.org/computing/software/mayhem-the-machine-that-finds-software-vulnerabilities-then-patches-them https://spectrum.ieee.org/computing/software/mayhem-the-mach... The field evidence would support their position, too. Your claim about C is true just enough to encourage people to not use it if they want to get more out of program analysis. Yet, current tools make up for it enough to find most or all bugs in benchmarks with Mayhem fixing them, too. The only problem is that almost nobody that cares about FOSS security is working on those tools that automate it. The companies doing it end up black boxing, patenting, etc the tools that they sell for exhorbitent prices. Something like RV-Match well-integrated with repos either FOSS or just price scaled to focus on mass adoption over high profit would be a game changer. Especially if 3rd parties could use it on repos.
    - lallysingh 7y ago
      Aren't those runtime tools like I just suggested? The other ones in the 1st link are theorem provers (at least the one that I recognized, frama-c) that require a lot more than off-the-shelf C code for their inputs. You can't just run CC=my-compiler-frontend make to suddenly get better diagnostics.
      - nickpsecurity 7y ago
        Companies are mixing static and running analysis more than they used to. Most static analyzers look at just the code itself, build models of it, check their properties, and report the presence/absence of errors. First links were more about effectiveness on C. I just dug around in search to find you something that explains it, shows its effectiveness, and threw in a case study you might enjoy: https://www.cs.colorado.edu/~kena/classes/5828/s12/presentation-materials/blackshearsam.pdf https://www.cs.colorado.edu/~kena/classes/5828/s12/presentat... https://cacm.acm.org/magazines/2010/2/69354-a-few-billion-lines-of-code-later/fulltext https://cacm.acm.org/magazines/2010/2/69354-a-few-billion-li... Here's the main competition evaluating them so you can see criteria and current state-of-the-art: https://www.sosy-lab.org/research/pub/2019-TACAS.Automatic_Verification_of_C_and_Java_Programs_SV-COMP_2019.pdf https://www.sosy-lab.org/research/pub/2019-TACAS.Automatic_V... The provers do something similar but with more manual effort and logic-based approach. Frama-C and SPARK Ada are interesting in that they use programmer annotations plus supporting functions (eg ghost code). These are converted into logical representation (eg facts about the program), fed into logic solvers with properties intended to be proved, and success/failure maybe tells you something. Like with static analyzers, you get the results without running the program. A recent, great addition is that, if proof is too hard, the condition you didn't prove can be turned into a runtime check. You could even do that by default only proving the ones that dragged performance down too much. Flexible. The best methods are a mix. I've always advocated mixing static analyzers, dynamic analysis, fuzzing etc since each technique might spot something the other will miss. They also cover for implementation bugs each might have. That adding runtime analysis can improve effectiveness does not negate my original claim that static, non-runtime analysis of C code can tell you a lot about it and/or find a ton of bugs. I also agreed with one point you made about it not conveying enough information: these clever tools pull it off despite C lacking design attributes that would make that easier. SPARK Ada is a great example of a language designed for low-level, efficient coding and easy verification. Although, gotta give credit to Frama-C people for improving things on C side.
        salawat 7y ago
        For some reason this feels like a rediscovery of the virtues of leaving asserts in production code to me. Though I need to give these a read. Thanks!
- KirinDave 7y ago
  It does suggest we should delete it, which is pretty helpful. It's a terribly liability.

Sure, just look at the languages that have more stringent type systems.

adrianN 7y ago

They don't really help me make the mountains of C we have in the world less buggy.

lallysingh 7y ago
C code doesn't have enough information in it to do a whole lot of mechanical analysis. Runtime analysis of its behavior is what you've got.
- nickpsecurity 7y ago
  Have you never heard of program analysis for security? Genuine question. RVI, the Mayhem developers, and many others would strongly disagree with you: https://runtimeverification.com/match/1.0-SNAPSHOT/docs/benchmark/ https://runtimeverification.com/match/1.0-SNAPSHOT/docs/benc... https://spectrum.ieee.org/computing/software/mayhem-the-machine-that-finds-software-vulnerabilities-then-patches-them https://spectrum.ieee.org/computing/software/mayhem-the-mach... The field evidence would support their position, too. Your claim about C is true just enough to encourage people to not use it if they want to get more out of program analysis. Yet, current tools make up for it enough to find most or all bugs in benchmarks with Mayhem fixing them, too. The only problem is that almost nobody that cares about FOSS security is working on those tools that automate it. The companies doing it end up black boxing, patenting, etc the tools that they sell for exhorbitent prices. Something like RV-Match well-integrated with repos either FOSS or just price scaled to focus on mass adoption over high profit would be a game changer. Especially if 3rd parties could use it on repos.
  - lallysingh 7y ago
    Aren't those runtime tools like I just suggested? The other ones in the 1st link are theorem provers (at least the one that I recognized, frama-c) that require a lot more than off-the-shelf C code for their inputs. You can't just run CC=my-compiler-frontend make to suddenly get better diagnostics.
    - nickpsecurity 7y ago
      Companies are mixing static and running analysis more than they used to. Most static analyzers look at just the code itself, build models of it, check their properties, and report the presence/absence of errors. First links were more about effectiveness on C. I just dug around in search to find you something that explains it, shows its effectiveness, and threw in a case study you might enjoy: https://www.cs.colorado.edu/~kena/classes/5828/s12/presentation-materials/blackshearsam.pdf https://www.cs.colorado.edu/~kena/classes/5828/s12/presentat... https://cacm.acm.org/magazines/2010/2/69354-a-few-billion-lines-of-code-later/fulltext https://cacm.acm.org/magazines/2010/2/69354-a-few-billion-li... Here's the main competition evaluating them so you can see criteria and current state-of-the-art: https://www.sosy-lab.org/research/pub/2019-TACAS.Automatic_Verification_of_C_and_Java_Programs_SV-COMP_2019.pdf https://www.sosy-lab.org/research/pub/2019-TACAS.Automatic_V... The provers do something similar but with more manual effort and logic-based approach. Frama-C and SPARK Ada are interesting in that they use programmer annotations plus supporting functions (eg ghost code). These are converted into logical representation (eg facts about the program), fed into logic solvers with properties intended to be proved, and success/failure maybe tells you something. Like with static analyzers, you get the results without running the program. A recent, great addition is that, if proof is too hard, the condition you didn't prove can be turned into a runtime check. You could even do that by default only proving the ones that dragged performance down too much. Flexible. The best methods are a mix. I've always advocated mixing static analyzers, dynamic analysis, fuzzing etc since each technique might spot something the other will miss. They also cover for implementation bugs each might have. That adding runtime analysis can improve effectiveness does not negate my original claim that static, non-runtime analysis of C code can tell you a lot about it and/or find a ton of bugs. I also agreed with one point you made about it not conveying enough information: these clever tools pull it off despite C lacking design attributes that would make that easier. SPARK Ada is a great example of a language designed for low-level, efficient coding and easy verification. Although, gotta give credit to Frama-C people for improving things on C side.
      - salawat 7y ago
        For some reason this feels like a rediscovery of the virtues of leaving asserts in production code to me. Though I need to give these a read. Thanks!
KirinDave 7y ago
It does suggest we should delete it, which is pretty helpful. It's a terribly liability.