5 ms·

Two other ways of checking integer bound invariants: 1. Undefined behavior sanitizer, which checks integer overflows at run-time, like INT_MAX + 1. Can optiona

by jbapple 10y ago

Two other ways of checking integer bound invariants: 1. Undefined behavior sanitizer, which checks integer overflows at run-time, like INT_MAX + 1. Can optionally check other invariants; see https://gcc.gnu.org/onlinedocs/gcc/Instrumentation-Options.html https://gcc.gnu.org/onlinedocs/gcc/Instrumentation-Options.h... and https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html. 2. Abstract interpretation - using a lot of constraint solver cycles and enough math to choke a dinosaur, you can check some integer bounds at compile time "relationally", like knowing that x < y. See, for example, "Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses": https://www.microsoft.com/en-us/research/publication/pentagons-a-weakly-relational-abstract-domain-for-the-efficient-validation-of-array-accesses/ https://www.microsoft.com/en-us/research/publication/pentago.... I'm not sure, but that code might be available in https://github.com/Microsoft/CodeContracts https://github.com/Microsoft/CodeContracts.

kentonv 10y ago
#1 doesn't get you very far since it can only catch cases that are locally detectable -- where the compiler can prove that some lines of code will always result in an overflow. Consider the code: int f(int x) { return x + 1; } This code could overflow, but surely the compiler won't complain about it -- it would instead assume that you don't intend to pass a value for x that is too large. In order for the compiler to have enough information to complain, it would need you to specify explicitly what the range of x is -- so that it can detect violations both within the function definition and at call sites. There is no built-in way to specify this. But, this is exactly what my template hacking adds -- a way to specify the actual range of each variable. I haven't looked closely at your #2. Presumably it also requires some constraint annotations to be added to your code. But if they've provided tools that can process those annotations and detect violations, that's pretty cool.
- jbapple 10y ago
  While I agree with your essential point about #1, I think we agree for different reasons. UBSan is a set of run-time checks and has low compile-time cost. The example function you give, f, would be complained about if you passed it INT_MAX, but that complaint would come at run-time and it would never be triggered if you never passed it INT_MAX. I also agree that it is not possible to enforce non-INT_MAX limits, like x < 10.
  - kentonv 10y ago
    Oh, for some reason I thought Clang's sanitizers were strictly compile-time, but looking closer I see that's not correct. Hmm, will have to look closer at that.
- nickpsecurity 10y ago
  The best ones you can straight-up buy are SPARK and Astree that I'm aware of. I've already linked to SPARK. Astree is limited in application but pretty amazing in what it does: https://www.di.ens.fr/~cousot/publications.www/CousotEtAl-ESOP05.pdf https://www.di.ens.fr/~cousot/publications.www/CousotEtAl-ES... My idea was to subset as many components as possible to static-ish components it could handle then focus more on integration testing. Then one could reap the benefits in a larger project. Similar idea for SPARK, which is probably cheaper.
  - touisteur 10y ago
    SPARK is indeed very adapted to some kinds of code (protocols, serialization, deserialization, index manipulation, masks...). Proving the absence of runtime errors in such code is easy (not much help needed for the provers, just type your data structures well) and makes you think of every case. Fun. Even better : once AoRTE is proved, remove all runtime checks and get C-like performance. You can also prove some isolated functional properties ('the answer to message X can only be message Y or Z'... just sprinkle some asserts, post-conditions or check the nice Contract_Case syntax). Or you can go to 'platinum'-level and prove your complete protocol/algorithm. The tech is great and it keeps improving, it gets easier every year...
    - nickpsecurity 10y ago
      Oh yeah, Rod Chapman and others at Praxis did amazing work. It's probably the single, most-practical tools in engineered software since abstract, state machines for specification or Cleanroom for building. Their error rate was so low. The traditional problem, though, was that some tools were good for specifying full correctness of high-level models while others were good for verifying properties of code itself. They rarely did both well. Still true with SPARK. Before DeepSpec, I was already pushing for mixing them up a lot with different tools on different components with some sort of unified logic. You might find it interesting that one of those was with SPARK and the successful Event-B method. I'll give you a paper show how hard it is to use Event-B by itself down to low-level code followed by how a combo improves things. http://eb2all.loria.fr/html_files/files/landingsystem.pdf http://eb2all.loria.fr/html_files/files/landingsystem.pdf http://journal.ub.tu-berlin.de/eceasst/article/view/785/782 http://journal.ub.tu-berlin.de/eceasst/article/view/785/782 One last thing before I head out is that the landing system paper is great for illustrating difficulty of correctness. It shows a small number of straight-forward requirements and design specs. Then, verification conditions are derived down to the low level code that must all be maintained true for total correctness. As in, it makes explicit all the stuff a developer must get right in their head to correctly solve this simple problem. I find it's a nice reality check for people even if they don't know the notation on intrinsic complexity of software & how that affects verification. Especially why you want to use simpler, automated methods than hope to test your way out of that level of complexity w/ corner cases. ;)

by jbapple 10y ago

kentonv 10y ago

#1 doesn't get you very far since it can only catch cases that are locally detectable -- where the compiler can prove that some lines of code will always result in an overflow. Consider the code: int f(int x) { return x + 1; } This code could overflow, but surely the compiler won't complain about it -- it would instead assume that you don't intend to pass a value for x that is too large. In order for the compiler to have enough information to complain, it would need you to specify explicitly what the range of x is -- so that it can detect violations both within the function definition and at call sites. There is no built-in way to specify this. But, this is exactly what my template hacking adds -- a way to specify the actual range of each variable. I haven't looked closely at your #2. Presumably it also requires some constraint annotations to be added to your code. But if they've provided tools that can process those annotations and detect violations, that's pretty cool.

jbapple 10y ago
While I agree with your essential point about #1, I think we agree for different reasons. UBSan is a set of run-time checks and has low compile-time cost. The example function you give, f, would be complained about if you passed it INT_MAX, but that complaint would come at run-time and it would never be triggered if you never passed it INT_MAX. I also agree that it is not possible to enforce non-INT_MAX limits, like x < 10.
- kentonv 10y ago
  Oh, for some reason I thought Clang's sanitizers were strictly compile-time, but looking closer I see that's not correct. Hmm, will have to look closer at that.
nickpsecurity 10y ago
The best ones you can straight-up buy are SPARK and Astree that I'm aware of. I've already linked to SPARK. Astree is limited in application but pretty amazing in what it does: https://www.di.ens.fr/~cousot/publications.www/CousotEtAl-ESOP05.pdf https://www.di.ens.fr/~cousot/publications.www/CousotEtAl-ES... My idea was to subset as many components as possible to static-ish components it could handle then focus more on integration testing. Then one could reap the benefits in a larger project. Similar idea for SPARK, which is probably cheaper.
- touisteur 10y ago
  SPARK is indeed very adapted to some kinds of code (protocols, serialization, deserialization, index manipulation, masks...). Proving the absence of runtime errors in such code is easy (not much help needed for the provers, just type your data structures well) and makes you think of every case. Fun. Even better : once AoRTE is proved, remove all runtime checks and get C-like performance. You can also prove some isolated functional properties ('the answer to message X can only be message Y or Z'... just sprinkle some asserts, post-conditions or check the nice Contract_Case syntax). Or you can go to 'platinum'-level and prove your complete protocol/algorithm. The tech is great and it keeps improving, it gets easier every year...
  - nickpsecurity 10y ago
    Oh yeah, Rod Chapman and others at Praxis did amazing work. It's probably the single, most-practical tools in engineered software since abstract, state machines for specification or Cleanroom for building. Their error rate was so low. The traditional problem, though, was that some tools were good for specifying full correctness of high-level models while others were good for verifying properties of code itself. They rarely did both well. Still true with SPARK. Before DeepSpec, I was already pushing for mixing them up a lot with different tools on different components with some sort of unified logic. You might find it interesting that one of those was with SPARK and the successful Event-B method. I'll give you a paper show how hard it is to use Event-B by itself down to low-level code followed by how a combo improves things. http://eb2all.loria.fr/html_files/files/landingsystem.pdf http://eb2all.loria.fr/html_files/files/landingsystem.pdf http://journal.ub.tu-berlin.de/eceasst/article/view/785/782 http://journal.ub.tu-berlin.de/eceasst/article/view/785/782 One last thing before I head out is that the landing system paper is great for illustrating difficulty of correctness. It shows a small number of straight-forward requirements and design specs. Then, verification conditions are derived down to the low level code that must all be maintained true for total correctness. As in, it makes explicit all the stuff a developer must get right in their head to correctly solve this simple problem. I find it's a nice reality check for people even if they don't know the notation on intrinsic complexity of software & how that affects verification. Especially why you want to use simpler, automated methods than hope to test your way out of that level of complexity w/ corner cases. ;)