3 ms·

Have you never heard of program analysis for security? Genuine question. RVI, the Mayhem developers, and many others would strongly disagree with you: https://

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!
    - nickpsecurity 7y ago
      That's a good comparison given asserts are specs. If you like asserts, the easiest, high-ROI method of getting into verification is Design-by-Contract. Here's both a way to sell it to your boss and some articles highlighting it: https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b... https://www.hillelwayne.com/post/contracts/ https://www.hillelwayne.com/post/contracts/ https://www.hillelwayne.com/post/pbt-contracts/ https://www.hillelwayne.com/post/pbt-contracts/ Many of us independently converged on a consensus about how to do it quickly, too. You put the contracts into the code, do property-based testing to test them, and have them turn into runtime or trace checks combined with fuzzers. Eclipser is one that runs on binaries finding problems way faster than others. This combo lets you iterate fast knocking problems out early. If you want more assurance, you can feed those contracts (aka formal specifications) into tools such as Frama-C and SPARK Ada to get proofs they hold for all inputs. Obviously, run lots of analyzers and testing tools on it overnight, too, so you get their benefits without just staring at the screen. https://github.com/SoftSec-KAIST/Eclipser https://github.com/SoftSec-KAIST/Eclipser Another lightweight-ish, formal method you might like was Cleanroom Software Engineering. It was one of first to make writing software more like engineering it. Stavely's introduction is good. His book was, too, with the chapter on semi-formal verification being easier to use and high ROI having excellent arguments. Fortunately, the automated and semi-automated tools doing formal analysis look good enough to replace some or all of the manual analysis Cleanroom developers do. Languages such as Haskell with advanced type systems might let it go even further. I advise coding in a simplified, hierarchical style like in Cleanroom to ease analysis of programs even if you do nothing else from the method. If you're curious, that technique was invented by Dijkstra in 1960's to build his "THE Metaprogramming System." https://web.archive.org/web/20190301154112/http://infohost.nmt.edu/~al/cseet-paper.html https://web.archive.org/web/20190301154112/http://infohost.n... https://en.wikipedia.org/wiki/THE_multiprogramming_system https://en.wikipedia.org/wiki/THE_multiprogramming_system Have fun with all of that. I'm pretty sure straight-forward coding, careful layering, DbC, and PbT will help you on realistic projects, too.

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!
  - nickpsecurity 7y ago
    That's a good comparison given asserts are specs. If you like asserts, the easiest, high-ROI method of getting into verification is Design-by-Contract. Here's both a way to sell it to your boss and some articles highlighting it: https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b... https://www.hillelwayne.com/post/contracts/ https://www.hillelwayne.com/post/contracts/ https://www.hillelwayne.com/post/pbt-contracts/ https://www.hillelwayne.com/post/pbt-contracts/ Many of us independently converged on a consensus about how to do it quickly, too. You put the contracts into the code, do property-based testing to test them, and have them turn into runtime or trace checks combined with fuzzers. Eclipser is one that runs on binaries finding problems way faster than others. This combo lets you iterate fast knocking problems out early. If you want more assurance, you can feed those contracts (aka formal specifications) into tools such as Frama-C and SPARK Ada to get proofs they hold for all inputs. Obviously, run lots of analyzers and testing tools on it overnight, too, so you get their benefits without just staring at the screen. https://github.com/SoftSec-KAIST/Eclipser https://github.com/SoftSec-KAIST/Eclipser Another lightweight-ish, formal method you might like was Cleanroom Software Engineering. It was one of first to make writing software more like engineering it. Stavely's introduction is good. His book was, too, with the chapter on semi-formal verification being easier to use and high ROI having excellent arguments. Fortunately, the automated and semi-automated tools doing formal analysis look good enough to replace some or all of the manual analysis Cleanroom developers do. Languages such as Haskell with advanced type systems might let it go even further. I advise coding in a simplified, hierarchical style like in Cleanroom to ease analysis of programs even if you do nothing else from the method. If you're curious, that technique was invented by Dijkstra in 1960's to build his "THE Metaprogramming System." https://web.archive.org/web/20190301154112/http://infohost.nmt.edu/~al/cseet-paper.html https://web.archive.org/web/20190301154112/http://infohost.n... https://en.wikipedia.org/wiki/THE_multiprogramming_system https://en.wikipedia.org/wiki/THE_multiprogramming_system Have fun with all of that. I'm pretty sure straight-forward coding, careful layering, DbC, and PbT will help you on realistic projects, too.