6 ms·

Catching integer overflows with template metaprogramming (2015)

88 points by jgeralnik 10y ago

staticassertion 10y ago
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.
- kentonv 10y ago
  https://twitter.com/BenLaurie/status/575079375307153409 https://twitter.com/BenLaurie/status/575079375307153409 :) The sad part of the story is that Cap'n Proto actually hasn't had a release since then, so (so far) I've effectively gotten out of doing any of those release-oriented things I promised. Many changes have gone into git master, but Sandstorm used git master directly, meaning there wasn't sufficient incentive to do the work of a release. (And as an understaffed startup we could never quite justify spending the time.) The good news is that I joined Cloudflare two weeks ago, who is a big Cap'n Proto user, and it looks like I'll have more time and justification to do releases there. (And yes, I do intend to fulfill all the promises in doing so.)
  - staticassertion 10y ago
    > The good news is that I joined Cloudflare two weeks ago, who is a big Cap'n Proto user, and it looks like I'll have more time and justification to do releases there That's great news, thanks for the disclaimer/ info.
DannyBee 10y ago
"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 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 :)
- jbapple 10y ago
  Does Ada check these type of invariants at compile-time or run-time?
  - DannyBee 10y ago
    It can do both.
- milesrout 10y ago
  Ada is not the right solution.
  - ky738 10y ago
    So what is the right solution? Don't leave us hanging like that, so unpolite.
- geofft 10y ago
  What's the story for interop between Ada and C on modern systems? That is, if I want to write a library that C programmers on Ubuntu or something can use in a straightforward manner, can I write it in Ada without too much difficulty?
  - nickpsecurity 10y ago
    Ada was designed for cross-language development. It was ahead of the curve on that. I'd be surprised if it was hard to integrate C today. The others I recall off top of head that went big in industry were OpenVMS (standard calling conventions, etc) and .NET CLR. I can't find my original article on "mixed, language development" in Ada but the marketing piece below gives you an idea of what developers were doing in 2005. Mixed language development, debugging, and traces. It's probably better now. https://www.rti.com/hubfs/docs/2005Q1_2.pdf https://www.rti.com/hubfs/docs/2005Q1_2.pdf
  - tjalfi 10y ago
    Ada95 added the Interfaces.C package for interop with C. http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-B-3.html http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-B-3.htm... shows the interface for Ada 2012. If you want your library to run anywhere then you probably still need to use C.
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.
danschumann 10y ago
Boo I thought it was a reference to fictional Tom Parris's holodeck program
winstonewert 10y ago
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.
- kentonv 10y ago
  Cap'n Proto by its nature is doing a lot of work with integers that represent sizes, indices, offsets, addresses, etc. These tend to have well-defined ranges -- and unusually bad failure modes. So it works unusually well here.
norswap 10y ago
> 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/ http://whiley.org/) and Dafny (http://rise4fun.com/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.
michaelt 10y ago
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.
- kentonv 10y ago
  For my purposes, I would be happy with a way that I can specify constraints specifically in certain critical code sections, where I'd be happy to work around some false positives. Most other code could go on ignoring overflow as it does today.

88 points by jgeralnik 10y ago

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.

kentonv 10y ago
https://twitter.com/BenLaurie/status/575079375307153409 https://twitter.com/BenLaurie/status/575079375307153409 :) The sad part of the story is that Cap'n Proto actually hasn't had a release since then, so (so far) I've effectively gotten out of doing any of those release-oriented things I promised. Many changes have gone into git master, but Sandstorm used git master directly, meaning there wasn't sufficient incentive to do the work of a release. (And as an understaffed startup we could never quite justify spending the time.) The good news is that I joined Cloudflare two weeks ago, who is a big Cap'n Proto user, and it looks like I'll have more time and justification to do releases there. (And yes, I do intend to fulfill all the promises in doing so.)
- staticassertion 10y ago
  > The good news is that I joined Cloudflare two weeks ago, who is a big Cap'n Proto user, and it looks like I'll have more time and justification to do releases there That's great news, thanks for the disclaimer/ info.

DannyBee 10y ago

"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 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 :)

jbapple 10y ago
Does Ada check these type of invariants at compile-time or run-time?
- DannyBee 10y ago
  It can do both.
milesrout 10y ago
Ada is not the right solution.
- ky738 10y ago
  So what is the right solution? Don't leave us hanging like that, so unpolite.
geofft 10y ago
What's the story for interop between Ada and C on modern systems? That is, if I want to write a library that C programmers on Ubuntu or something can use in a straightforward manner, can I write it in Ada without too much difficulty?
- nickpsecurity 10y ago
  Ada was designed for cross-language development. It was ahead of the curve on that. I'd be surprised if it was hard to integrate C today. The others I recall off top of head that went big in industry were OpenVMS (standard calling conventions, etc) and .NET CLR. I can't find my original article on "mixed, language development" in Ada but the marketing piece below gives you an idea of what developers were doing in 2005. Mixed language development, debugging, and traces. It's probably better now. https://www.rti.com/hubfs/docs/2005Q1_2.pdf https://www.rti.com/hubfs/docs/2005Q1_2.pdf
- tjalfi 10y ago
  Ada95 added the Interfaces.C package for interop with C. http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-B-3.html http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-B-3.htm... shows the interface for Ada 2012. If you want your library to run anywhere then you probably still need to use C.

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.

danschumann 10y ago

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

winstonewert 10y ago

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.

kentonv 10y ago
Cap'n Proto by its nature is doing a lot of work with integers that represent sizes, indices, offsets, addresses, etc. These tend to have well-defined ranges -- and unusually bad failure modes. So it works unusually well here.

norswap 10y ago

> 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/ http://whiley.org/) and Dafny (http://rise4fun.com/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.

michaelt 10y ago

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.

kentonv 10y ago
For my purposes, I would be happy with a way that I can specify constraints specifically in certain critical code sections, where I'd be happy to work around some false positives. Most other code could go on ignoring overflow as it does today.