[trustable-software] Model Checkers

[Ben Brewer]

On 21/09/18 15:45, Maciej Wolny wrote:
> On 21/09/2018 14:10, Ben Brewer wrote:
>> The website for MOPS states that it's not a checker itself, but a framework for adding your own checks, so I highly suspect that the reason it could be run over an entire distro is that they ran a very minimal set of checks; the paper also suggests this as they only found 138 bugs in the distribution, while I believe it's reasonable to assume that there are a lot more than that.
> If you're coming from a perspective of finding all bugs, you're going to be disappointed forever. Not only that, this perspective is dangerous, because any procedure/tool that you believe to be satisfying this requirement will give you a false sense of security. 138 bugs is in and of itself neither a big or small. That being said, personally, I would be proud of this result, and would consider it an important contribution to the bug-finding effort.
I agree, it'd be silly to expect an exhaustive list of bugs, but I don't 
think anyone suggested that.

I was more meaning that 138 is a very small number for an entire linux 
distro given I'm pretty sure gcc -Wextra, cppcheck or scanbuild would 
find orders of magnitude more bugs/issues.

Either way, I don't think using an abandoned 14 year old framework is a 
particularly practical approach.