Licensing restrictions of formal methods (code proof) tools and contractors

Question

This is NOT Intended to be a product/service recommendation question - I am trying really hard to word this so it isn't one.

Does anyone here perform static analysis on your code using abstract interpretation or formal methods? If so, did you have to license a tool to do it? Is this something that can be contracted out?

Here is my dillemma: My company makes embedded systems products. Our programming language is C99 and the target we're running on a 16bit little-endian processor. We are looking into some code analysis tools that use formal methods / abstract interpretation to evaluate all execution paths of code and guarantee that they will be free from run time exceptions. This does not replace function testing like unit testing or system integration testing, but it would give us extra coverage on scenarios that are hard to test in system and it would reduce the amount of time an effort that we need to put into code reviews.

We've looked at several tools and they are all great! They are also pretty expensive (~30kUSD is the price floor). I could run some numbers and prove that we will get ROI in a few years vs. doing nothing, but I am wondering if there are any other options. We also do not necessarily need to run the tool daily or nightly - our release frequency isn't that fast. Sure that would be nice, but we would also benefit greatly just being able to run the tool periodically before major milestones and releases - so a couple of times a month.

So naturally I started looking into contractors who may have the tool and could run this service for us. But I can't seem to find any. It appears the vendors who make these tools might all have clauses in their EULAs that prohibit them from using the tool on code they do not own or are not shipping in their product.

There are some open source options out there that I am aware of - but taking the time to configure that tool without support also has some implicit cost to it.

If there are contractors that are able to do this sort of thing, then perhaps I am just not searching for them the right way. Is there some other term I should be searching for?

Answer 1

I haven't gone looking for such services, but I doubt that they would work out.

Current static analysis tools can deliver very useful information, but they need to be tuned for best results. This tuning is an upfront cost that you have to pay (either by doing it or by paying the vendor to do it for you) once per code base, regardless of how often you run the tool. That comes in addition to the time it took to develop the tool, which of course is independent of how many times you run the tool. The only part of static analysis tools that costs more when you use it more is the processor time on a beefy machine — and if you want you can rent that bit out easily, but it's only a small part of the total cost.

The time it took to develop the tool itself is to a first approximation constant, and as a second approximation a function of the number of different customers (extra features, support). Once again how often you run the tool doesn't matter. The upshot is that economically speaking, there is no reason to charge you less because you use the tool less often.

Moving on from the economics to the technical side, I take strong objection to your statement that

We also do not necessarily need to run the tool daily or nightly - our release frequency isn't that fast.

You should run static analysis tools nightly! Ideally, if they're fast enough, run them for each commit. Static analysis is not something you do just before the release: at that point, it's lost a lot of its value. If a bug can be found both by static analysis and by runtime testing, let static analysis tell you, because you'll fix it quicker that way.

Static analysis tells you where your code looks suspicious. These are the places that you need to focus more on, maybe get a second pair of eyes on, and test more thoroughly, perhaps with some additional asserts. The feedback from static analysis is more useful before you do any debugging, because static analysis gives you a lot more direct feedback. The output of a (good) static analysis tool is something like “if x > y and p == NULL then there is an array access out of bounds at line 1234”. Being told that when the code is still fresh in your mind is a lot more helpful than waiting a week, then finding that one of the stress tests is crashing at line 2345, and spending three days with a debugger to find just where the heap had gotten corrupted.

The proper order of things is static analysis first, then runtime testing, then manual review. Each steps benefit from having the previous step weed out the problems it could detect.

Answer 2

I think there are (at least) two levels of static analysis. There are the lint-like analysers that can be run quickly and, as said in @Gilles' answer, can perhaps should be run on every build. (I read that lint was separate from the early C compilers for performance reasons. The computers and compilers were slow and lint checks have added significant extra time to the compilation.)

There are other analysers that require a significant expenditure of time to run them and to analyse the outputs. I worked in a team that used Malpas (see here) to formally analyse a large software system. The analysis took somewhere between 20 and 50 man-years.

Your question desires:

code analysis tools that use formal methods / abstract interpretation to evaluate all execution paths of code and guarantee that they will be free from run time exceptions

To achieve this, you should expect to spend a significant amount of time on the analysis. You have to ask yourself - is it really worth it? Will people die or be hurt if the system does not work properly? If not then ask your accountants to balance the cost of failures against the cost of ensuring that the system does not fail.