from Hacker News

Catching integer overflows with template metaprogramming (2015)

by jgeralnik on 3/26/17, 9:45 PM with 32 comments

• by DannyBee on 3/27/17, 1:12 AM

  "Some day, I would like to design a language that gets this right. But for the moment, I remain focused on Sandstorm.io. Hopefully someone will beat me to it. Hint hint. "

  Some language already did beat him to it: Ada

  http://www.ada-auth.org/standards/12rat/html/Rat12-2-4.html

  Ada's rules for type invariants check them in all the places you would expect, and are straightforward to use.

  It's about as correct as you can get without it being impossible to compute :)

• by michaelt on 3/27/17, 11:56 AM

    Why don’t programming languages do this?
  

  I worked on a contribution to clang-analyser a few months ago - one of the things I learned was (1) No-one likes code analysers that raise false alarms and (2) it's really difficult not to raise false alarms. For example, consider checking this program for divide-by-zero bugs:

    for (int i=-99999 ; i<99999 ; i+=2) {
      printf("%d\n", 100/i);
    }
    for (int i=-100000 ; i<100000 ; i+=2) {
      printf("%d\n", 100/i);
    }
  

  A programmer can clearly see that in the first loop there is no divide-by-zero as i will jump directly from -1 to +1 - whereas in the second loop the counter will hit 0 and trigger a divide-by-zero.

  But for a static analyser, your options are:

  1. Model i as a single value, and simulate all ~400,000 passes through the loops. Slow - you basically have to run the program at compile time.

  2. Same but truncate the simulation after, say, 20 loops on the assumption that most bugs would have been found on the first few passes. This misses the bug in the second loop.

  3. Model i as "Integer in the range -99,999 to +99,999" and generate a false alarm on the first loop.

  4. Support arbitrarily complex symbolic values. Difficult - as the value of a variable might depend on complicated business logic.

  I guess the benefit of starting a new programming language is you can choose option 3 and say "Working code is illegal, deal with it" from the start.

• by staticassertion on 3/27/17, 1:03 AM

  That's a pretty impressive response - committing to fuzzing with AFL, improving current fuzzing test coverage, adding new coding guidelines, and a paid security audit.

  In regards to 4 (valgrind) perhaps utilizing other sanitizers would be a good idea.

  Awesome that they tested whether those methods would actually have caught this bug - and multiple did. That's a smart metric.

  And a writeup about TMP and compile time safety to boot.

  I'm struggling to come up with anything more that I'd want in a disclosure.

• by jbapple on 3/27/17, 1:55 AM

  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.h... and 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/pentago.... I'm not sure, but that code might be available in https://github.com/Microsoft/CodeContracts.

• by norswap on 3/27/17, 10:03 AM

  > Some day, I would like to design a language that gets this right. But for the moment, I remain focused on Sandstorm.io. Hopefully someone will beat me to it.

  Two language that do it: Whiley (http://whiley.org/) and Dafny (http://rise4fun.com/dafny).

  I expect (but not sure) that the proving power is about the same as what can be achieved by template meta-programming.

• by winstonewert on 3/27/17, 4:56 AM

  I'm unclear on how this would work out practically. Cases where my integers belong to a fixed range seems rare. I'd like to have seen more discussion of how it caught the bugs it did.

• by danschumann on 3/27/17, 2:38 AM

  Boo I thought it was a reference to fictional Tom Parris's holodeck program