Has cbmc found security bug in a widely used software?

20 views
Skip to first unread message

Georgi Guninski

unread,
Nov 8, 2020, 5:10:44 AM11/8/20
to cprover...@googlegroups.com
There is a lot money in the security "theatre".

Has cbmc found security bug in a widely used software?

Andrew Jones

unread,
Nov 8, 2020, 6:29:51 AM11/8/20
to cprover...@googlegroups.com
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

unread,
Nov 9, 2020, 6:58:10 AM11/9/20
to cprover...@googlegroups.com
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


Reply all
Reply to author
Forward
0 new messages