Modern systems, from data centers to embedded systems, are built from an ever-growing assortment of embedded controllers, accelerators, and firmware components. At scale, traditional “test more” approaches struggle to keep pace: tests can show the presence of bugs but cannot guarantee the absence of whole classes of failures that attackers routinely exploit. That is why the conversation is shifting from securing software after it is written to engineering security into the software from the start.

In a presentation by Adam Zabrocki and Marko Mitic of NVIDIA at DEF CON, they discuss the challenge of securing a proprietary, billion-core architecture.

Since 2016, NVIDIA has migrated its Falcon control processors to RISC-V, shipping 10 - 40 cores per chipset and surpassing a billion cores by 2024. This brought challenges that existing models couldn’t address. The response was a ground-up security design: a purpose-built separation kernel, custom RISC-V extensions (e.g., pointer masking, IOPMP), and bespoke secure boot and attestation. The talk shares lessons learned and what’s next for NVIDIA.

This article will delve into a particular section of the talk, from ~27 minutes onwards, that sets out NVIDIA’s stance on language-based security.

Rather than relying solely on operating system guards or run-time checks, the idea is to enforce properties through the programming language and toolchain. By using strong types, contracts, and automated proofs, they rule out undefined behavior and memory hazards by construction. In practice, that means specifying what critical modules must do, encoding those expectations as pre-/postconditions and invariants, and then discharging proof obligations so that verified components become hardened building blocks in a layered defense.

What is meant by “language-based security“?

Language-based security is defined as enforcing security properties through the programming language (types, contracts, semantics) and compiler-assisted analysis, rather than relying only on OS/hardware guards. The idea is to shrink the trusted computing base and rule out whole classes of defects by construction.

Why does this matter for NVIDIA?

Conventional testing can’t give sufficient assurance at the scale NVIDIA describes (many GPUs, each with tens of embedded RISC-V control cores). Tests show bugs exist; proofs can show certain bugs cannot occur.

“Traditionally, we relied on tests to show programs correctness or to point out that there is a security vulnerability somewhere in the code, and this is good but there are no guarantees that you won’t have a let’s say single overflow in a large C codebase, for example, but with SPARK we can prove that whole classes of vulnerabilities will not ever happen and we do that through contract-based programming, and due to the fact that SPARK is a very strict subset of Ada language with formally defined specification.” Marko Mitic, NVIDIA

Using SPARK enables NVIDIA to prove the absence of run-time errors such as overflows and memory safety, including out-of-range memory accesses in selected modules.

Marko goes on to make the point that you don’t have to write 100% of the software in SPARK. You can make calls into Ada, C, or assembly as needed. This allows engineers to pursue a practical, incremental adoption of SPARK, focusing their efforts on the most critical parts of the software.

“In this case, you would test for what you cannot prove. SPARK proves that the preconditions hold when a foreign call is made; it’s the postconditions that have to be tested, because the foreign code provides no guarantees”.

“If you have most of your code in SPARK, or let’s say some subcomponents 100% written in SPARK, having this guarantee that there will be no runtime exceptions at any given time for any given input is extremely valuable for both security and reliability perspectives.”

Key takeaways

• At scale, assurance must be engineered in, not inspected in: Use a language and toolchain that allows you to prove the absence of critical classes of defects.
• SPARK is used here to verify selected GPU-adjacent RISC-V firmware components, narrowing “language states” to provably correct behavior and reducing attack surface.
• Language-based security complements hardware features and testing; it’s part of a layered defense strategy for a proprietary, high-volume embedded ecosystem.

Watch the full talk from DEF CON 33 here: DEF CON 33 - How to secure unique ecosystem shipping 1 billion+ cores? - Adam Zabrocki, Marko Mitic