CASE STUDYNVIDIA: Adoption of SPARK Ushers in a New Era
in Security-Critical Software Development

adacore.com

Summary

Customer:

NVIDIA Corporation, the world’s best-known maker ofgraphics processing units (GPU), is also among the mosttrusted names in embedded systems, high-performancecomputing, and artificial intelligence. As a supplier ofcritical hardware, software, and firmware components
across numerous sectors, they are recognized for tacklingsome of the tech industry’s toughest problems.

Challenge:

Security is essential to NVIDIA’s brand. However, withcybersecurity risks rising across the board, includingin the verticals they serve, the company was facing thechallenge of delivering more secure products without
incurring a large increase in development time and cost.

An increasingly hostile cybersecurity
environment
Several converging macro trends are currently putting pressure on
the makers of embedded systems. Customers are demanding they
demonstrate air-tight security in their products.
First, cyberattacks against firmware and hardware are on the rise.
Hackers are targeting the lower levels of the technology stackhoping to exploit vulnerabilities that are difficult and expensive tocorrect. Due to the ubiquity of embedded systems, it is often very
costly to update firmware and hardware in the field.
Second, the development and verification ecosystem hasn’t
kept pace with the scale of these attacks. Many languages
and toolsets are insufficiently robust for critical embedded
applications; they provide no guarantees during development that
security vulnerabilities have been eliminated. For example, the C
programming language is often preferred for embedded systems
because it’s great for writing fast and efficient code. But codedeveloped in C is hard to get perfect and C lacks many verification
capabilities.
Third, an industry-wide lack of secure code designers and software
security practitioners is making project timescales problematic.
These valuable resources have become extremely difficult tofind. The cybersecurity professional organization (ISC)2 recently
calculated the global cybersecurity workforce shortage totalledsome 2.7 million unfilled positions at the end of 2021. 1
The convergence of these trends is causing extreme concern insafety-critical sectors such as medical devices, robotics, andautomotive. OEMs are demanding a high degree of security
assurance from their suppliers. And they have become very
interested in the methods and techniques being used in secureenvironments.
1(ISC)2 Cybersecurity Workforce Study, 2021, (ISC)2, March 2022.

NVIDIA Corporation is among
the world’s most trusted
names in graphics processing
units, embedded systems,
high-performance computing,and artificial intelligence.
To find a more measurable
solution for verifying
embedded system security andsafety in an increasingly hostile
threat environment.

Solution:

SPARK - a programming
language designed to facilitate
the use of formal methods toguarantee the correctness ofsoftware with mathematicsbased assurance.

Result:

NVIDIA is now using SPARK toachieve and demonstrate theabsence of runtime errors in
its most critical components
and to prove conformance tospecifications for its root-oftrust applications.

Company Snapshot
NVIDIA has over

25,000+employees

Operates in50+

locations
Reported$26.9 billion
revenue in FY22

Find out how SPARK and AdaCore can help you with your projects

adacore.com

2

A preference for measurable
outcomes
In response to these concerns, NVIDIA examined all
aspects of their software development methodology,
asking themselves which parts of it needed to evolve.
They began questioning the cost ofusing the traditional languages andtoolsets they had in place for theircritical embedded applications.
For years, they had typically used
C and C++ for these applications.
And they were still sufferingfrom the decades-old challenges
endemic to those languages,
including ambiguities in the C andC++ specifications that limit theeffectiveness of C and C++ analysis
tools. When there is no certainty ofverification, you never know when
you’re done testing a particularcode module. Security assurance
not only isn’t certain, progress
towards it isn’t measurable underthose circumstances.

can we actually use?” They put these questions to theirsoftware security team.
In reply, the security team came back with what
Daniel Rohrer characterized as “a fairly heretical”
proposition: “What if we just stopped using C?”SPARK has a capability
that is not found in mostother programming
languages. That is theability to specify program
requirements within
the code itself and use
the associated set oftools to ensure that theimplementation matches
its requirements.
Essentially you areproving your programs
are correct. That’s a very
powerful capability.

This led to other questions, like,“What alternative languages andtools are available to support theuse of formal methods?”
In trying to answer thosequestions, NVIDIA discovered
SPARK.

SPARK and its benefits
SPARK is a high-level computer
programming language consistingof a well-defined subset of Ada.
Like Ada before it, SPARK wasdesigned for the developmentof high-integrity software usedin systems where predictable
and highly reliable operation isessential. SPARK uses a language
feature known as “contracts” tospecify components in a form thatis suitable for static verification
using formal methods.

“We like measurable outcomes,”- Dhawal Kumar,
said Daniel Rohrer, VP of Software
Principal Software Engineer, NVIDIA
Security at NVIDIA. “We’d like tobe able to ship products into thefield and know what the customer
experience is going to be before they see it. One of the “From the perspective of programming language
key challenges we placed in front of the team is how capabilities, the paradigms are very similar to C andto turn this from a non-measurable, where we can’t C++,” said Dhawal Kumar, a principal software engineer
even answer ‘Are we done yet,’ to a more measurable at NVIDIA and one of their first SPARK users. “SPARK
answer.”is an imperative programming language. You can write
procedure-oriented or object-oriented code, and there
NVIDIA’s software security team examined various are other facilities for programming in the large.”
methods and strategies that offered measurability.
They soon recognized that the bases of many of these Thanks to its design, there can be no undefined
methods were mathematical formal methods and the behaviors in code developed with SPARK. The language
use of formal provers. They also discovered that these comes with a set of built-in checks that make sure alltools had undergone a major evolution over the past its rules are obeyed, so run-time errors (such as buffer
decade or so.
overrun) cannot occur.
“We wanted to emphasize provability over testing asa preferred verification method,” said Rohrer. “Testing
security is pretty much impossible. It’s hard to know
if you’re ever done.” Formal proof, on the other hand,offered guarantees that were very attractive to NVIDIA.
These include the absence of runtime errors andcommon security vulnerabilities, and also proof that a
program’s functionality conforms to its specification.

A “heretical” proposition
NVIDIA began to ask themselves, “Can we change ourfundamental approach? And if so, which of these tools

Another key feature of SPARK is that it supports formal
verification. In other words, through the use of SPARK
and formal methods solvers, it is possible to prove
mathematically that your SPARK code behaves inprecise accordance with its specification. This process
is known as formal verification.
“SPARK has a capability that is not found in most otherprogramming languages,” said Dhawal Kumar. “That is
the ability to specify program requirements within thecode itself and use the associated set of tools to ensurethat the implementation matches its requirements.
Essentially you are proving your programs are correct.
That’s a very powerful capability.”

Find out how SPARK and AdaCore can help you with your projects

adacore.com

3

AdaCore appears very
focused on solving customer’s
problems first. We know we
can count on AdaCore toanswer our questions withvery low latency.
- Dhawal Kumar,
Principal Software Engineer, NVIDIA

Advantages of SPARK
Daniel Rohrer listed several SPARK advantages thatwere important to NVIDIA.
First, SPARK is deterministic. This enables formal
proofs to guarantee the absence of runtime errors andspecification compliance.
Next, SPARK code is linkable with C. This meant
NVIDIA would not have to recode everything at once orrecode non-critical components. SPARK components
are easily integrated within C/C++ environments.
This allowed NVIDIA to wisely choose targets thatwarranted the investment in formal verification.
Finally, SPARK has a credible ecosystem. Ada,
SPARK’s basis, is a very mature language. It has been
upgraded several times since the 1980s. World-classtool support is readily available through AdaCore—theworld’s foremost authority in Ada and SPARK—and
other organizations as well. Plus, Ada and SPARK havean upstream Open Source Software (OSS) presence.
So, while NVIDIA was glad to have AdaCore as a willing
and responsive partner, they knew that even without
AdaCore they could carry their SPARK initiative into
the future.

Successful proof of concept
In the final quarter of 2018, NVIDIA conducted a
proof-of-concept (POC) exercise to delve deeper
into the SPARK language, the associated tools, andthe available technical support; the purpose was toconfirm their general fitness for NVIDIA’s purposes.
For this initial POC, the NVIDIA software security
team applied SPARK to two applications. The firstwas a bare metal application that acts as a rootof trust for code running on several other security
processors. The second was a Real-Time Operating
System (RTOS) application that handles the resizingof protection regions.
In only three months, the small POC team was able
to convert nearly all the code in both codebases
from C to SPARK. In doing so, they realized major

improvements in the security robustness of both
applications. Thanks to the soundness of SPARK
and the ability to express program properties ascontracts, NVIDIA found that reliance on scarce
security practitioners could be significantly reduced.
They also found that the developer teams adapted
readily to the new language and tools.
Reviewing the results with their safety assessor,
NVIDIA also found that SPARK can be safely mixed
with C in a safety context. What’s more, the safetyassessor deemed SPARK not only acceptable but
preferable over C/C++ for safety-critical applications,provided developers have sufficient training.
Evaluating return on Investment (ROI) based on theirresults, the POC team concluded that the engineeringcosts associated with SPARK ramp-up (training,
experimentation, discovery of new tools, etc.) wereoffset by gains in application security and verification
efficiency and thus offered an attractive trade-off.
Finally, NVIDIA concluded that SPARK’s support
infrastructure was excellent.
Dhawal Kumar, who led the POC, called AdaCore’s
support system world-class. “AdaCore appears very
focused on solving customer’s problems first,” hesaid. “We know we can count on AdaCore to answer
our questions with very low latency.”
Daniel Rohrer acknowledged their POC put AdaCore
in a tough corner, but AdaCore’s tools and support
team responded admirably. “We were doing low-levelfirmware in a custom ASIC with registers and side
effects that had to be modeled. Our problems were
not uniform and generally not in AdaCore’s sweet
spot,” said Rohrer. “Throughout the course of thePOC, however, both the tooling and the support really
lived up to the challenge. Surprisingly so.”Coming out of the POC, NVIDIA felt quite confident
that the savings and benefits from using SPARK
would continue, while the added ramp-up costs would
gradually disappear as SPARK expertise grew within
the company.

Find out how SPARK and AdaCore can help you with your projects

adacore.com

4The main reason why we use SPARK is for theguarantees it provides. One of the key values
we wanted to get out of this language was theabsence of runtime errors. It’s very attractive
to know your code avoids most of the common
pitfalls. You tend to have more confidence
when coding in SPARK because the language
itself guards against the common, easily mademistakes people make when writing in C.
- James Xu,
Senior Manager for GPU Software Security, NVIDIA

Adopting SPARK for NVIDIA’s mostsecurity-critical development projects
NVIDIA began implementing SPARK in its security
strategy in 2019 on select pieces of firmware. They
began training additional personnel in SPARK andeventually developed an in-house training program.
Several NVIDIA teams are now using SPARK fora wide range of applications that include image
authentication and integrity checks for the overall
GPU firmware image, BootROM and secure monitor
firmware, and formally verified components of an
isolation kernel for an embedded operating system,
to name just a few.
In general, their targets tend to be smaller code basesthat would benefit the most from SPARK’s strong
typing, absence of runtime errors, and in some cases,
rigorous formal verification of functional properties

Proof of absence of runtime errors
When asked to quantify the benefits they’ve gained
from adopting SPARK, NVIDIA engineering managers
spoke of the guarantees SPARK provides and ofincreased confidence in the quality of their products.
James Xu is the Senior Manager for GPU Software
Security at NVIDIA. His group is charged with making
sure software and firmware in NVIDIA’s GPUs areshipping with industry-leading security postures.
They also drive innovative security and privacy
technologies that help make NVIDIA’s products
unique.
“The main reason why we use SPARK is for theguarantees it provides,” said Xu. “One of the key
values we wanted to get out of this language wasthe absence of runtime errors. It’s very attractive toknow your code avoids most of the common pitfalls.
You tend to have more confidence when coding in

SPARK because the language itself guards against
the common, easily made mistakes people makewhen writing in C”.
“It’s very nice to know that once you’re done writing
an app in SPARK—even without doing a lot of testingor line-by-line review—things like memory errors,
off-by-one errors, type mismatches, overflows,
underflows and stuff like that simply aren’t there,” Xusaid. “It’s also very nice to see that when we list ourtables of common errors, like those in MITRE’s CWElist, large swaths of them are just crossed out. They’re
not possible to make using this language.”
Varun Kumar manages the GPU Firmware Security
team at NVIDIA. His group is responsible forcomponents that initialize and boot up the GPUs,
functions like secure boot, firmware update, anddevice recovery attestation. He now has 20 engineersbuilding components in SPARK to NIST SP800-193
platform firmware resiliency guidelines. He says thequalities Xu mentioned are also attractive to theircustomers’ security personnel.
“The fact that we can confidently say that we don’t
have any off-by-one errors, overflows, underflows,etc., and are backed by a formally verifiable method(tool), provides good guarantees about the security
and robustness of the program.” said Varun Kumar.

Formal verification—without code
bloat or performance degradation
Cameron Buschardt, a Principal Software Engineer
at NVIDIA, is responsible for the architecture of anembedded operating system. For his application, heneeds a deeper level of proof. Beyond the absenceof runtime errors, he needs formal verification:
demonstrable mathematical proof that the critical
portions of his code are functionally identical to thecorresponding portions of his model.

Find out how SPARK and AdaCore can help you with your projects

adacore.com

5

“We have customers who review our security
parameters very closely. Just being able to say, weformally verified our code—we didn’t just run somebug checking hunting tool, we formally verified
it—that’s huge. The high level of trust this evokes
drastically reduces review burden and maintenanceefforts. It’s huge for me and also for our customers.”

Schedule impact turned out to be far less significant
than imagined. For example, James Xu had guesseddevelopment in SPARK would take twice as long as
in C. That turned out not to be the case when careis taken to apply SPARK to well isolated and smaller(but more valuable) areas. He characterized theactual impact as “a minor annoyance.”

Unlike James Xu and Varun Kumar, whose groups “Some of us were concerned, initially, about how
are using SPARK on new components, Cameron much schedule overrun there might be, or how weBuschardt was able to compare his newly-written were going to fund these projects,” said Xu. “But thatSPARK modules with equivalent modules in C. He turned out not to be a problem.”found no code bloat, nor
Varun Kumar also said that
did he see any degradation
finding help has not been aof performance. “Looking
concern, thanks to AdaCore’s
at the assembly generated
We have customers who
support system.
from SPARK, it was almost
review
our
security
parameters
identical to that from the C
Finally, SPARK has delivered
very closely. Just being able
code,” he said. “I did not see
on its “absence of run-time
to say, we formally verified
any performance difference
errors” promise.
our code—we didn’t just run
at all. We proved all of ourproperties, so we didn’t needsome bug checking hunting“It’s nice to have confidence
to enable runtime checks.”that your code base won’t be
tool, we formally verified it—
plagued with common errors,”
that’s huge. The high level ofsaid Xu. “About 70% of thetrust this evokes drastically
Mitigated concerns
common CVEs simply can’t
reduces review burden andand rising confidence
occur in SPARK. So, when
maintenance efforts. It’s
you talk to an external auditor
As one might expect whenhuge for me and also for our
who looks at your code, for
an organization tries a newcustomers.
example, you can deflect(and possibly a bit heretical)
some basic concerns they
way of doing things, many
- Cameron Buschardt
often have. When they ask
of NVIDIA’s developers andPrincipal Software Engineer, NVIDIA
if they have to read the code
engineering managers wereline by line to see if you’ve got
initially skeptical of SPARK.
misused pointers, overflowsinyourindexes,andstufflike that, you can just“The skepticism was due to a variety of concerns
categoricallysay,‘Don’tbother.
Those things can’t
depending upon whom you talked to, whether they
exist.
You
don’t
need
to
look
at
the
codebase.’”were in engineering or management,” said James Xu.
“Ada and SPARK are less well-known languages insome industries, which led to many questions: Whatis our ability to scale up engineering resources? How
will it impact our development schedules? How do
we find help? The absence of runtime errors sounds
nice, but do we really get that in practice? When it
comes to logic bugs, how does SPARK help us then?
Plus, given the unfamiliarity and the restrictions of
the language, there was a perception of a significantly
longer development time compared to writing in C.”
The answers NVIDIA has gotten to those questions
have overcome much of that skepticism.
For training, NVIDIA initially took advantage of
AdaCore’s courses, but it didn’t take them long todevelop their own in-house training program. They
found their developers ramp up quickly.

Improving customer relationships
Cameron Buschardt says the guarantees SPARK
provides make discussions with customers oversecurity far easier.
“It’s far easier to focus discussions in a massive
component if you’re simply able to say, ‘Hey, look,
we’ve got this tool. We were able to prove theseproperties, let’s focus on other areas of security.’That, for me, is a big motivating factor, because
that’s not going away: customers look at our security
story. With SPARK, it’s much easier to sell.”Find out how SPARK and AdaCore can help you with your projects

adacore.com

6Former skeptics havebecome advocates
Seeing firsthand the positive effects SPARK andformal methods have had on their work and theircustomer rapport, many NVIDIA engineers who
were initially skeptical have become enthusiastic
proponents.
“I’ll be honest; at the beginning,
I was very, very skeptical,” said
Cameron Buschardt. “My firstattempts to prove non-trivial
algorithms in SPARK weredisastrous. But after we got past
the initial learning curve, I wasshocked at what we could prove.
“SPARK promises to let us
implement a component, prove it,
and be done with it,” he continued.
“This is transformative and it
evokes a level of trust no otherlanguage provides.”Daniel Rohrer indicated thatBuschardt is just one of many who
have shed their skepticism andembraced SPARK.

At the conclusion of their initial POC at the end of
2018, NVIDIA had five developers trained in SPARK.
By the second quarter of 2022, that number had
grown to over fifty. During that same period, NVIDIA
implemented numerous components in SPARK. These
include many components of their GPU firmware
image, portions of their hardware boot ROMs, andseveral libraries to simplify the discharge of proofs
for the kernel of an embedded
operating system.

I’ll be honest; at the
beginning, I was very,
very skeptical. My firstattempts to prove nontrivial algorithms in
SPARK were disastrous.
But after we got past theinitial learning curve, I
was shocked at what we
could prove.
SPARK promises to let us
implement a component,
prove it, and be done with
it. This is transformativeand it evokes a level oftrust no other language
provides.

Many NVIDIA products arenow shipping with SPARK
components, and awareness andinterest in SPARK continue togrow within the company.
“We initially created a small
proof-of-concept to convince
ourselves and subsequently
implemented a larger piece of theboot firmware in SPARK. That
proved to other teams within
NVIDIA that SPARK is a viableoption for firmware or similaruse-cases.”“It’s coming up more often inarchitectural discussions,” says
Buschardt. “We’re seeing security
meetings where we’ll talk abouta critical security property thata customer is interested in, andwe’ll come back to that theme:
we can show our customers proof
that this does exactly what the
spec says it does.”“There have been others who,
as we’ve engaged through thisprocess, were initially detractors
but have subsequently becomechampions,” Rohrer said. “For those- Cameron Buschardt
who’ve looked at the challenges
Principal Software Engineer, NVIDIA
that are facing us and were willingto face them head-on, once they
Overall, NVIDIA has demonstrated
got past the initial inertia of ‘Hey,groundbreaking
leadershipand innovation in thethis is the way we’ve been doing it the last 20 years,’ it’s
softwaresecurity
domain.
They
had a very challenging
been transformative.”goal and took an ambitious path to accomplish
something that had never been done before in thesemiconductor industry. For four years, they have
Rapid growth
successfully demonstrated time and time again that
The use of SPARK and the formal methods tools built their choice to adopt SPARK was the right one - andfor the language has grown and spread rapidly within have paved the way for anyone interested in following
NVIDIA since their initial deployment.
NVIDIA’s lead.

Find out how SPARK and AdaCore can help you with your projects

adacore.com

7adacore.com

8