4 ms·

Bounded model checking is not a silver bullet. If you want to prove it is, verify a Web browser and blog about it.

• nanolith 2y ago
  There are no silver bullets. But, that doesn't mean that we should dismiss tooling that is not well understood in order to chase unrealistic goals, like rewriting extant code bases in a different language to achieve security goals. Or, worse, as this article suggests, using mechanical translation to somehow capture the features of error-prone software without carrying over the errors. Better process and better tooling allows us to write better software. Bounded model checking is an incredibly useful bit of tooling that allows us, within context of the software, to demonstrate that certain conditions do not arise. This includes memory errors, resource errors, and other classes of errors. The limitation is the faithfulness of the translation to SMT and the complexity of the code being modeled. The former has gotten quite good with CBMC 6, and the latter can be managed through careful refactoring and shadow function substitution. Is it magic? There is no such thing. But, it is a practical tool that is available for use today. One need not wait until an entire web browser is verified using it. It can scale to this, but given the unreasonable size and scope of web browsers with respect to this challenge, which are basically operating systems and suites of software in one these days, that's like saying, "verify all software then blog about it."