Inferbo: Infer-based buffer overrun analyzer
research.fb.com
Inferbo: Infer-based buffer overrun analyzer
1–7 of 7 posts
Re: Inferbo: Infer-based buffer overrun analyzer
#2They mention that they "manually injected into open source C source (spell, unhtml, spell++, bc, gzip). I also ran Inferbo on some internal Facebook code and Inferbo generated alarms in the third-party C source(e.g. open-ssl)."
They then go onto demonstrate how it did in those injected bug cases (really well), but they don't really get into what they found for those "out in the wild" alarms in the third-party C source. The latter seem to be more interesting than the injected bugs.
Re: Inferbo: Infer-based buffer overrun analyzer
#3This sounds cool!
The first example has a pretty nasty typo. This:
int *arr = malloc(9);
It should of course be:
int *arr = malloc(9 * sizeof *arr);
Re: Inferbo: Infer-based buffer overrun analyzer
#4This sounds cool! The first example has a pretty nasty typo. This: int *arr = malloc(9); does of course not allocate enough space to make it safe to index arr up to 8. It only allocates 9 bytes , which on a typical 32-bit int machine only gives you room for 2.25 ints. It should of course be: int *arr = malloc(9 * sizeof *arr); It's fixed in the second example, where they introduce the malloc_wrapper().
Thanks for pointing this out! Fixed in an update to the post.
Re: Inferbo: Infer-based buffer overrun analyzer
#5They mention that they "manually injected into open source C source (spell, unhtml, spell++, bc, gzip). I also ran Inferbo on some internal Facebook code and Inferbo generated alarms in the third-party C source(e.g. open-ssl)." They then go onto demonstrate how it did in those injected bug cases (really well), but they don't really get into what they found for those "out in the wild" alarms in the third-party C sourc…
Right. But our purpose was to assure that Inferbo performs well to find the bo errors of FB-style against "noises" from the coding idioms in realistic sw.
Re: Inferbo: Infer-based buffer overrun analyzer
#6Can you clarify - does this ship with 0.9.4.1, or is there any procedure for using it beyond the standard Infer invocation?
Re: Inferbo: Infer-based buffer overrun analyzer
#7Can you clarify - does this ship with 0.9.4.1, or is there any procedure for using it beyond the standard Infer invocation?
I added some documentation on using Inferbo and other experimental checkers we are working on: http://fbinfer.com/docs/experimental-checkers.html.
All you need to do to use Inferbo is add `-a bufferoverrun` to your normal Infer command. Inferbo isn't included in 0.9.4.1, but we'll be creating a new release soon.