Has cbmc found security bug in a widely used software?

[Georgi Guninski]

There is a lot money in the security "theatre".

Has cbmc found security bug in a widely used software?

[Andrew Jones]

A quick Google suggests that https://nvd.nist.gov/vuln/detail/CVE-2017-5462 was found with the help of CBMC: https://formal.iti.kit.edu/klebanov/pubs/nss-cve-2017-5462.pdf

HTH

On Sunday, November 8, 2020, Georgi Guninski <ggun...@gmail.com> wrote:

There is a lot money in the security "theatre".

Has cbmc found security bug in a widely used software?

--

---
You received this message because you are subscribed to the Google Groups "CProver Support" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cprover-support+unsubscribe@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/cprover-support/CAGUWgD8MuJDjNkikCu9RJH5%2BE_dBJk9R9urkU-0%2BH%2Bce%2BRqSug%40mail.gmail.com.

[Martin Nyx Brain]

On Sun, 2020-11-08 at 11:03 +0200, Georgi Guninski wrote:
> There is a lot money in the security "theatre".
>
> Has cbmc found security bug in a widely used software?

Some of the users of CBMC do security analysis but many of those are
focused on development-time and pre-deployment security. So perhaps
another question worth thinking about is "how many bugs were found
before things became widely used software". For that you might want to
look at:

Model Checking Boot Code from AWS Data Centers
https://d1.awsstatic.com/Security/pdfs/Model_Checking_Boot_Code_From_AWS_Data_Centers.pdf

Code-level model checking in the software development workflow
https://www.amazon.science/publications/model-checking-as-a-human-endeavor

Cheers,
- Martin