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

Original Article ↗ Hacker News Discussion ↗

Scope and Reality of “Stopping C” at Nvidia

  • Several commenters note the title is misleading: Nvidia did not drop C wholesale; SPARK/Ada is used in specific, security‑critical components.
  • Case study material (linked in thread) indicates SPARK is used mainly for:
    • GPU firmware image authentication and integrity checks
    • BootROM and secure monitor firmware
    • Parts of an isolation kernel for an embedded OS on a RISC‑V root‑of‑trust core
  • Overall usage is described as “significant in important places” but a tiny fraction of Nvidia’s total codebase; most drivers and CUDA stack remain C/C++.

Marketing vs Engineering Substance

  • Some see the piece as AdaCore marketing, arguing external consultants can recommend radical rewrites without bearing migration cost.
  • Others counter that multiple Nvidia security engineers, training investment, and multi‑year adoption suggest real internal buy‑in, not just PR.

Why SPARK/Ada for Firmware

  • SPARK offers:
    • Strong typing, range types, and rich numeric/packet modeling
    • Formal proofs of absence of run‑time errors and selected functional properties
  • This is seen as a good fit for small, stable, security‑critical firmware and isolation kernels, less for large, fast‑moving codebases like drivers or CUDA libraries.

Syntax, Approachability, and Interoperability

  • Debate over Ada’s “unapproachable” syntax:
    • Some argue syntax is a red herring compared to safety/contracts; others claim a curly‑brace dialect would greatly boost adoption.
  • Interop concerns:
    • Ada interoperates well with C, and to a degree C++, but heavy modern C++ (STL, unique_ptr, templates) complicates clean boundaries.
    • Serialization/deserialization at language boundaries can add overhead and complexity; this is framed as a general multi‑language problem, not Ada‑specific.

Formal Verification vs Testing and C

  • Some commenters applaud emphasizing provability over testing for high‑integrity code; others warn verification only proves conformance to a (possibly flawed) spec and doesn’t cover timing side channels, microarchitectural flaws, etc.
  • Comparisons raised:
    • SPARK vs Rust: SPARK can express and prove more properties (e.g., range types, functional proofs), while Rust primarily targets memory safety.
    • Verified C paths (CompCert, Frama‑C, proprietary tools) are mentioned; several people who tried both say SPARK’s type system makes proofs easier than for pointer‑heavy C.
  • Skeptics doubt any language will truly “replace C” for OS/low‑level work; they see this more as adding a verified island inside a C sea.

AI, Proof Assistants, and the Future

  • Some argue the real future path to pervasive verification is AI‑assisted proof and code generation, not niche languages.
  • Others are cautious:
    • Current LLMs struggle with non‑mainstream domains (Ada/SPARK, advanced math, borrow checkers) and often hallucinate APIs or incorrect arguments.
    • AI‑generated code in non‑verified languages may increase subtle concurrency and logic bugs if developers over‑trust completions.
  • A promising niche proposed: AI as a helper for generating verification annotations and boilerplate in already‑formal ecosystems (SPARK, Coq‑based systems), where results are still checked by deterministic tools.

GPU Security and Threat Model

  • Some initially question why Nvidia needs strong security: “they just make graphics cards.”
  • Counterpoints:
    • Modern GPUs carry RISC‑V roots of trust akin to T2/ME/PSP, enforce secure boot chains, isolation, and feature segmentation.
    • GPUs are central to national‑scale AI infrastructure and used in safety‑critical domains (automotive, drones); compromise of firmware or RoT is high‑impact.
  • Discussion touches on GPU rootkits and DMA capabilities; concerns about “kludgey” GPU architectures and mailbox/VRAM transfer bottlenecks surface.

SPARK Tooling, Licensing, and Activity

  • Clarifications:
    • SPARK and GNATprove are open source and freely available; commercial “SPARK Pro” mainly adds support, newer releases, and “wavefronts” (details not fully explained in thread).
    • The project’s commit history is cited as evidence it’s actively developed, countering claims of being “largely untouched.”
  • Alire is highlighted as the de‑facto package manager/distribution channel for the free toolchain.

Language Design and Safety Features

  • Ada/SPARK features praised:
    • Range types, derived types, subtype predicates, and bounds‑checked arrays/strings that prevent many classes of errors by construction.
    • Ease of modeling bit‑packed registers and network/packet formats compared to many mainstream languages.
  • Some view these strong types as “creepy” or alien compared to plain integers; fans argue they eliminate whole bug categories and are closer to what safety‑critical domains need.

Alternatives and Broader System Ideas

  • Suggestions include:
    • Using verifiable C subsets and verified compilers instead of switching languages.
    • Avoiding opaque binary blobs entirely by distributing intermediate representations and compiling on‑device; critics label this unrealistic due to performance, IP, and ecosystem hurdles.
  • There is recurring tension between “ideal” verified stacks and messy real‑world constraints (existing C++ ecosystems, proprietary drivers, hardware quirks).