Security is only as strong as its weakest link. That's important to keep in mind for software security, with its long chain of links, from design to development to deployment. Last year, members of NVIDIA's Offensive Security Research team (aka "red team") presented at DEF CON 29 their results on the evaluation of the security of a firmware written in SPARK and running on RISC-V. They ended up not finding vulnerabilities in the code but in the RISC-V ISA instead. This year, the same team presented at DEF CON 30 a retrospective on the security evaluation of 17 high-impact projects since 2020. TL;DR: using SPARK makes a big difference for security, compared to using C/C++.

The security researchers start by stating a well-known fact (that they support with the reports on 12 years of security bugs at Microsoft, and 5 years of security bugs at Google Chrome team): 70% of all security bugs are related to memory safety. That's the kind of bugs you won't see in SPARK code, as they are either prevented by the design of SPARK or detected by formal verification.

Then, at 15:39 in the recording, Zabrocki asks the most interesting question: do they see benefits in using SPARK, compared to similar developments in C/C++? He then goes on to compare the results on 3 projects in SPARK and 6 projects in C/C++, and the results are clear. As he says: there is a "huge difference". Not only do they detect fewer security bugs in SPARK projects, but they detect "deeper" bugs related to software design and hardware-software interfaces, as they do not need to spend time looking for "simple" bugs like memory safety ones.

If you want to peek at what are the "deeper" bugs that they detected in SPARK projects, jump to 22:38 of the recording. I personally enjoyed it! And I'm both amazed and grateful that NVIDIA shows such openness in disclosing the kind of bugs that escaped all their regular development and verification activities.

If you have only 2 minutes, just jump to the conclusion at 39:00. There should be some inspiration for you if you're facing similar security issues in your software products.