4 ms·

A sound static analyzer in theory can check the safety of that by examining all code paths and complain whenever any exist where it is possible to go out of bou

by ryao 4y ago

A sound static analyzer in theory can check the safety of that by examining all code paths and complain whenever any exist where it is possible to go out of bounds. It is called sound because the absence of a complaint means it has proven the absence of the issues it is meant to catch. If it has a limitation that prevents it from finding a proof, it will complain about the lines that could not be proven safe.

WalterBright 4y ago
Nearly all my use of arrays is arrays whose length cannot be known until runtime.
- ryao 4y ago
  Then it will complain if there are no checks on the inputs used at runtime to restrict the array usages to safe ones. At least, that is the theory. I have yet to use one. I plan to try the ones I mentioned next year. That said, NIST gave astree a good review in 2020: https://nvlpubs.nist.gov/nistpubs/ir/2020/NIST.IR.8304.pdf https://nvlpubs.nist.gov/nistpubs/ir/2020/NIST.IR.8304.pdf
  - simplotek 4y ago
    > Then it will complain if there are no checks on the inputs used at runtime to restrict the array usages to safe ones. You're only commenting on your personal belief of how your ideal static analyzer would magically work to meet your expectations. This doesn't correspond to how static analyzers work in reality. Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility. C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible?
    - still_grokking 4y ago
      > Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility. Here's a list: https://en.wikipedia.org/wiki/Symbolic_execution#Tools https://en.wikipedia.org/wiki/Symbolic_execution#Tools Also related: https://en.wikipedia.org/wiki/Abstract_interpretation https://en.wikipedia.org/wiki/Abstract_interpretation > C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible? Depends on how you define "feasible". Abstract interpretation and symbolic execution are crazy complex¹. Academia decided that this isn't realistically "feasible" and moved on to some much simpler approaches like pure functional programming and prove systems bases on depended types. Trying to make static guaranties about imperative code is indeed a dead end by now. The problem is that proving any properties of imperative code needs much more effort (and therefore code) than what is expressed by the code that needs proves, so it's actually likely that you haven than bugs in the code that proves things. So this approach is not really "feasible" in the end. --- ¹ Just have a look at the documentation around the KeY tool used to prove things about Java programs. https://www.key-project.org/thebook2/ https://www.key-project.org/thebook2/ That's the most complex stuff I've ever seen! Depended type systems are "trivially simple" in contrast, no joke. But this is just about a "simple language" like Java… The complexity of C is much much higher.
      - zozbot234 4y ago
        Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking.
        still_grokking 4y ago
        > Type checking is actually a special case of abstract interpretation. I'm not sure about that. Maybe in regard to type level functions? But else? I'm skeptical. Could you explain what you exactly mean? Preferably with some examples as I'm having a hard time to imagine something in that direction. > For all we know, it may even be that dependent types can already express many complex uses of it; That for sure! Otherwise, corresponding type systems wouldn't be considered being an alternative. Depended types can express anything computable. (Which also makes them undecidable in general). In theory, you can prove any property of a program using depended types. That's why they're the preferred method by now. But you can't bold on such thing after the fact usually. Your language needs to be pure to benefit form the proving powers of depended types. So no hope for C and such like.
    - ryao 4y ago
      > You're only commenting on your personal belief of how your ideal static analyzer would magically work to meet your expectations. This is how sound static analyzers are advertised. > This doesn't correspond to how static analyzers work in reality. Of course it does not, since a normal static analyzer is not sound. However, a sound static analyzer is sound. > Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility. I already did (and explained that while I have yet to use it, NIST did a positive review). Until you learn better reading comprehension, you will never see it. Here is a hint. Look 6 comments up. > C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible? The theory was made 5 decades ago: https://en.wikipedia.org/wiki/Abstract_interpretation https://en.wikipedia.org/wiki/Abstract_interpretation It has already been rolled out in aviation, nuclear power, etcetera. Even NASA is using an implementation of it: https://www.nasa.gov/content/tech/rse/research/ikos https://www.nasa.gov/content/tech/rse/research/ikos You, like myself a few months ago, had never heard of it. However, when was the last time you seriously looked for something like this? I have been making a major push to resolve all static analysis reports from Coverity, Clang and others in OpenZFS. I found it when looking into additional static analyzers. If it were not for that, I would still be entirely unaware. That being said, you have a clear reading comprehension issue, since I already provided links showing that NASA has deployed software implementing that theory and NIST did a positive review of software implementing it. It is absurd to read that and think “this is not feasible”.
  - ck45 4y ago
    That sounds a bit like what WUFFS is doing WUFFS: https://github.com/google/wuffs https://github.com/google/wuffs

by ryao 4y ago

WalterBright 4y ago

Nearly all my use of arrays is arrays whose length cannot be known until runtime.

ryao 4y ago
Then it will complain if there are no checks on the inputs used at runtime to restrict the array usages to safe ones. At least, that is the theory. I have yet to use one. I plan to try the ones I mentioned next year. That said, NIST gave astree a good review in 2020: https://nvlpubs.nist.gov/nistpubs/ir/2020/NIST.IR.8304.pdf https://nvlpubs.nist.gov/nistpubs/ir/2020/NIST.IR.8304.pdf
- simplotek 4y ago
  > Then it will complain if there are no checks on the inputs used at runtime to restrict the array usages to safe ones. You're only commenting on your personal belief of how your ideal static analyzer would magically work to meet your expectations. This doesn't correspond to how static analyzers work in reality. Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility. C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible?
  - still_grokking 4y ago
    > Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility. Here's a list: https://en.wikipedia.org/wiki/Symbolic_execution#Tools https://en.wikipedia.org/wiki/Symbolic_execution#Tools Also related: https://en.wikipedia.org/wiki/Abstract_interpretation https://en.wikipedia.org/wiki/Abstract_interpretation > C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible? Depends on how you define "feasible". Abstract interpretation and symbolic execution are crazy complex¹. Academia decided that this isn't realistically "feasible" and moved on to some much simpler approaches like pure functional programming and prove systems bases on depended types. Trying to make static guaranties about imperative code is indeed a dead end by now. The problem is that proving any properties of imperative code needs much more effort (and therefore code) than what is expressed by the code that needs proves, so it's actually likely that you haven than bugs in the code that proves things. So this approach is not really "feasible" in the end. --- ¹ Just have a look at the documentation around the KeY tool used to prove things about Java programs. https://www.key-project.org/thebook2/ https://www.key-project.org/thebook2/ That's the most complex stuff I've ever seen! Depended type systems are "trivially simple" in contrast, no joke. But this is just about a "simple language" like Java… The complexity of C is much much higher.
    - zozbot234 4y ago
      Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking.
      - still_grokking 4y ago
        > Type checking is actually a special case of abstract interpretation. I'm not sure about that. Maybe in regard to type level functions? But else? I'm skeptical. Could you explain what you exactly mean? Preferably with some examples as I'm having a hard time to imagine something in that direction. > For all we know, it may even be that dependent types can already express many complex uses of it; That for sure! Otherwise, corresponding type systems wouldn't be considered being an alternative. Depended types can express anything computable. (Which also makes them undecidable in general). In theory, you can prove any property of a program using depended types. That's why they're the preferred method by now. But you can't bold on such thing after the fact usually. Your language needs to be pure to benefit form the proving powers of depended types. So no hope for C and such like.
  - ryao 4y ago
    > You're only commenting on your personal belief of how your ideal static analyzer would magically work to meet your expectations. This is how sound static analyzers are advertised. > This doesn't correspond to how static analyzers work in reality. Of course it does not, since a normal static analyzer is not sound. However, a sound static analyzer is sound. > Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility. I already did (and explained that while I have yet to use it, NIST did a positive review). Until you learn better reading comprehension, you will never see it. Here is a hint. Look 6 comments up. > C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible? The theory was made 5 decades ago: https://en.wikipedia.org/wiki/Abstract_interpretation https://en.wikipedia.org/wiki/Abstract_interpretation It has already been rolled out in aviation, nuclear power, etcetera. Even NASA is using an implementation of it: https://www.nasa.gov/content/tech/rse/research/ikos https://www.nasa.gov/content/tech/rse/research/ikos You, like myself a few months ago, had never heard of it. However, when was the last time you seriously looked for something like this? I have been making a major push to resolve all static analysis reports from Coverity, Clang and others in OpenZFS. I found it when looking into additional static analyzers. If it were not for that, I would still be entirely unaware. That being said, you have a clear reading comprehension issue, since I already provided links showing that NASA has deployed software implementing that theory and NIST did a positive review of software implementing it. It is absurd to read that and think “this is not feasible”.
- ck45 4y ago
  That sounds a bit like what WUFFS is doing WUFFS: https://github.com/google/wuffs https://github.com/google/wuffs