Today I want to share a great story about why many NVIDIA products are now running formally verified SPARK code. This blog post is in part a teaser for the case study that NVIDIA and AdaCore published today.

Our journey begins with the NVIDIA Security Team. Like many other security-oriented teams in our industry today, they were looking for a measurable answer to the increasingly hostile cybersecurity environment and started questioning their software development and verification strategies.

“Testing security is pretty much impossible. It’s hard to know if you’re ever done,” said Daniel Rohrer, VP of Software Security at NVIDIA.

In my opinion, this is the most important point of the case study - that test-oriented software verification simply doesn’t work for security. Once you come out of the costly process of thoroughly testing your software, you can have a metric on the quality of the features that you provide to the users, but there’s not much you can say about security.

Rohrer continues, “We wanted to emphasize provability over testing as a preferred verification method.” Fortunately, it is possible to prove mathematically that your code behaves in precise accordance with its specification. This process is known as formal verification, and it is the fundamental paradigm shift that made NVIDIA investigate SPARK, the industry-ready solution for software formal verification.

Back in 2018, a Proof-of-Concept (POC) exercise was conducted. Two low-level security-sensitive applications were converted from C to SPARK in only three months. After an evaluation of the return on investment, the team concluded that even with the new technology ramp-up (training, experimentation, discovery of new tools, etc.), gains in application security and verification efficiency offered an attractive trade-off. They realized major improvements in the security robustness of both applications (See NVIDIA's Offensive Security Research D3FC0N talk for more information on the results of the evaluation).

As the results of the POC validated the initial strategy, the use of SPARK spread rapidly within NVIDIA. There are now over fifty developers trained and numerous components implemented in SPARK, and many NVIDIA products are now shipping with SPARK components.

I encourage everyone to read the full case study, which covers some important topics that should be very interesting for others questioning their own cybersecurity strategies, such as:

• Performance compared to C: “I did not see any performance difference at all.”

• Overcoming skepticism: “others who ... were initially detractors but have subsequently become champions”

• Impact on audits: “Hey, look, we’ve got this tool. We were able to prove these properties, let’s focus on other areas of security.”

• Customer relationships: “we didn’t just run some bug-checking hunting tool, we formally verified it—that’s huge”