Nvidia Security Team: “What if we just stopped using C?” (2022)

People who don't want to read the first line of the article, rejoice!

It sounds like a good decision though. Formal verification tends to make more sense in highly concurrent situations where there is a high-value stable API to be supported. That describes graphics cards and surrounding environments really well so it makes sense that Nvidia would find use cases.

Something more from the article is also that they made the decision with a pilot project that went well. It'd be nice to have more details about it; that sort of thing is important to do well and always interesting. Lo and behold, we do have more details about it! https://blog.adacore.com/when-formal-verification-with-spark... - there is a video in there that looks to be worth a watch.

I really wish there was more active development on SPARK.

It's largely untouched over the last 10-years.

https://github.com/AdaCore/spark2014

For those not aware, SPARK gives even more safeguards/guarantees than Rust (see below) ... and also does it at compile time (when not all of Rust safeguards are at compile time).

https://blog.adacore.com/should-i-choose-ada-spark-or-rust-o...

They actually had to use the non-cutdown version of SPARK that this company sells, called SPARK Pro.

SPARK has some adherents in spacecraft programming for its formal verifiability and safety features.

[flagged]

Not related to Ada, but Dafny is a "Verification aware programming Language" where both Formal Specification and Verification are combined together in the same source language - https://dafny.org It uses curly braces and can generate code for a number of different languages at the backend (eg. Java, C#, Go, Python, Javascript, C++).

I haven't played with it yet but just from reading the documentation i really like this approach since you need learn only one language/toolchain for both formal specification/verification and implementation. But by giving one the flexibility to generate code to various mainstream languages you can slowly add verified code module by module to existing codebases.

You are right but the vhdl-like syntax is quite nice. It does some surprisingly modern things.

Nothing prevents anyone from creating a preprocessor that maps { to BEGIN and } to END.

I'm also desperate to stop Rust by any means, but I don't think you're correct; I think the sticking point for language adoption is the presence or absence of a big npm clone.

That would be a good start as the current syntax is absurd.

I'd also add that AI code generation in non-formally-verifiable languages, at places with concurrency requirements like Nvidia, might end up in the short-term creating more hard-to-spot concurrency bugs than before, as developers become incentivized to tab-complete code without fully thinking through the implications as they type.

But AI code generation for formally verifiable programs? And to assist in writing custom domain-specific verifiers? Now that's the sweet spot. The programming languages of the future, and the metaprogramming libraries on top of them, will look really, really cool.

I’m not entirely sure they are writing any portion of their driver using SPARC the presentation they gave 5 years ago seems to indicate they are limiting the usage to firmware for their embedded RISC-V co-processor, they may have expanded the usage of it but I still think it’s predominantly firmware related with possibly some expansion to their automotive and robotics solutions.

https://www.slideshare.net/slideshow/securing-the-future-of-...

It bears repeating that Nvidia is not strictly speaking a SW company. It is a semiconductors company. That 30k employees figure includes all Nvidia employees, not all of which are in software.

I am rather skeptical of AI in this context. Until you have verifiably correct AI assistants, you still need a highly skilled human in the loop to catch subtle errors in the proofs or the whole result is moot anyway.

And there _are_ tools out there capable of verifying C code, but for a greenfield project implementation/verification in a higher-level, formal language + verified compilation might make more sense.

> Article doesn't say what parts of Nvidia's stack use SPARK.

Their linked case study lists three examples and one category, https://www.adacore.com/uploads/techPapers/222559-adacore-nv...

  - image authentication and integrity checks for the overall GPU firmware image
  - BootROM and secure monitor firmware
  - formally verified components of an isolation kernel for an embedded operating system
  - In general, their targets tend to be smaller code bases that would benefit the most from SPARK’s strong typing, absence of runtime errors, and in some cases, rigorous formal verification of functional properties

> NVRISCV is NVIDIA’s implementation of the RISC-V ISA and Peregrine subsystem includes NVRISCV and multiple peripherals. They show how fine-grain access controls, formally verified for correctness, allow following the principle of least privilege for each partition. NVRISCV provides secure boot that starts with an immutable HW, the chain of trust extends to the Secure Monitor in SW, where partition policies are set up and isolation enforced using HW controls.. Boot and Secure Monitor software is implemented in SPARK.

The article seems fairly clear that it is the security folks within Nvidia that are spearheading this. 50 engineers on the security team doesn't seem unreasonable for a company of that size.

I feel like it’s going to be a step further and we won’t write actual “code” but more like comprehensive tests and it generates the code . Sort of like the movement from assembly to C

Totally agree that AI is going to have a huge impact on security of languages, and will change many paradigms.

formal verification is normally used on the most security critical code so even 50 programmers is a lot.

> After briefly skimming through their talk they mention they're a third party consultancy company making recommendations on safety for NVIDIA, so "Nvidia Security Team" take it how you will.

This is a marketing case study by the major Ada tools and training vendor, on years of engineering work done by their customer, Nvidia. It includes quotes from Nvidia employees and their blog references a Defcon video by the head of the Nvidia Offensive Security team, https://www.adacore.com/uploads/techPapers/222559-adacore-nv...

  Principal Software Engineer
  Manager, GPU Firmware Security 
  Senior Manager, GPU Software Security
  VP, Software Security

  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.. Several NVIDIA teams are now using SPARK for a 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.

The focus of their work seems to be low-level firmware, and not CUDA or any kind of compute. It makes sense a lot there because you won't need as many libraries.

The syntax is really a red-herring especially when you get contracts, proof of absence of runtime errors and higher-lever functional proof, mostly automated, or assisted with annotations. If you're actually going with this effort, the lack of curly braces, ampersands shouldn't be a main concern.

I forget sometimes that the papers and talks issued by teams at most companies are for PR and resume-padding. They hype the findings that justify that team's budget, and bury any negatives.

The other funny thing I noticed is the formal verification just means the program implements the standard - it doesn't mean the standard doesn't have security holes! And sometimes the security holes are implementation-specific, like timing attacks, which can require weird low-level tricks to solve.

> moving towards a completely different language always bug me, especially when the syntax is also completely different.

Why do syntax differences bug you? I could understand most concerns about switching ecosystems, but surely the difference between e.g. C++ and Java and JavaScript are orders of magnitude larger than that between C++ and Ada. Syntax is the smallest piece of it all, as far as I'm concerned.

> Then there's like everything libraries wise and CUDA is all C/C++ if I'm not mistaken.

Ada has excellent C interop.

Maybe it's naive of me but I also don't really perceive much of a security imperative for NVIDIA. They make graphics cards and slop generator cards for the most part. What exactly is the threat model here that requires switching to prioritizing memory safety? Are there a lot of graphics card related codes that are being exploited in the wild?

In general, NVIDIA never had proper bug-free support in C for well over a decade (hidden de-allocation errors etc.), and essentially everyone focused on the cuda compiler with the C++ API.

To be honest, it still bothers me an awful GPU mailbox design is still the cutting-edge tech for modern computing. GPU rootkits are already a thing... Best of luck =3

Yeah, when I see the equivalent to slang written in Ada/Spark, I'll actually believe them.

Yeah, it completely loses all weight when it’s an external consultancy suggesting it.

It’s easy to say “rewrite everything in X because Y” when you don’t have to deal with the burden of figuring out how to do that.

Flagged the article because the title is super misleading.

That does nothing to fix the vast majority of security issues, which are caused by trusted but not memory safe programs running on untrusted input.

It's also an extremely unrealistic goal. First of all, you run into a massive problem with companies and copyright. Second of all, it will be very hard to convince users that it's normal for their Chrome installation to take half an hour or more while using their CPU at 100% the whole time.

I feel like you might as well ask "why not world peace"?

There are a huge number of practical issues to be solved to make that be viable.

The VST Lab at Princeton works on this sort of problem: https://vst.cs.princeton.edu/

"The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context."

Some of the same researchers worked on TAL (typed assembly language), which sounds like it could be one of the "intermediate representations" you mentioned.

For a while, Apple required apps to be submitted as bitcode (LLVM IR) to the App Store, where they would be converted to x86 or Arm machine code during device install. They stopped that a couple of years ago, after migration to Apple Silicon.

There is a rule that if somebody poses this hypothetical with the word "just" in it, they have signed themselves up to go and implement it.

So, congratulations, take it and run with it.

> "What if we just stopped distributing and blindly executing untrusted binary blobs?"

You can do that right now with open source software and Bootstrappable Builds.

https://bootstrappable.org/ https://lwn.net/Articles/983340/

> huge promotional opportunity

Right? Yet they published this customer case study in 2022 and it never reached HN. Found in 2025 search on GPU firmware security.

Love that feature, along with derived types[1] and subtype predicates[2]. There's a special place in my heart partitioned for things that won't let you screw things up.

[1] https://learn.adacore.com/courses/intro-to-ada/chapters/stro...

[2] https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Devel...

Alright, this is Hacker news, so I'm gonna nitpick...

> It even would have a special instruction for unpacking UTF-8 characters

From https://en.wikipedia.org/wiki/Reduced_instruction_set_comput... :

> The term "reduced" in that phrase was intended to describe the fact that the amount of work any single instruction accomplishes is reduced—at most a single data memory cycle—compared to the "complex instructions" of CISC CPUs that may require dozens of data memory cycles in order to execute a single instruction.

I don't think what you're describing is a RISC processor at all.

This doesn't strike me as that different than an enum.

Not only Ada?

Pascal is less esoteric and has had that forever.

Their PDF has a bit more detail, https://news.ycombinator.com/item?id=43043541

There's a GPL version of GNATprove, which you can install with Alire (https://alire.ada.dev). That's the version I use.

You wouldn't guess it from AdaCore's homepage, but SPARK tooling (including provers) and the GNAT Ada compiler are both made freely available, with the goal of attracting interest from FOSS projects.

Here's a page on this: https://blog.adacore.com/a-new-era-for-ada-spark-open-source...

ajxs is right to say that the way to get your hands on this tooling is to use the Alire package-manager. AdaCore no longer offer alternative means of distribution (except, presumably, to paying customers).

It failed to catch on outside the defense industry because that is where is started. It was long sneered at as a "language designed by committee".

In one programming class, in college, we used a text-book called "Oh my, Modula 3!". On the back they explained the title, saying "better 'Oh my, Modula 3!' than 'Oh no, Ada!'".