[r1chardnl]

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. Also I think these drastic changes moving towards a completely different language always bug me, especially when the syntax is also completely different.

Then there's like everything libraries wise and CUDA is all C/C++ if I'm not mistaken. In every large project I'm sure you're eventually going to find some exploit attack vector. Especially if the focus from what I believe for GPU/CUDA until recently wasn't mostly focused on security rather than performance and those are always trade-offs.

[transpute]

> 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.

[touisteur]

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.

[indolering]

Ada's refusal to make their language any more approachable is a problem.

[yjftsjthsd-h]

What's unapproachable about it? And if your answer involves syntax, how do you explain Python?

[bluGill]

Mostly I have no clue how I would use it in my project without rewriting from scratch.

[yjftsjthsd-h]

You either write the main program in C and call Ada libaries, or you write the main program in Ada and call C libaries: https://learn.adacore.com/courses/intro-to-ada/chapters/inte...

(And this seems pretty general; you'd have to do roughly the same thing to mix C/Rust, C/Pascal, Rust/Python, ...)

[bluGill]

Problem is my main program is c++ complete with the stl that makes it useful. Vectors unique-ptr and all the other weird stuff that makes c++ better that c.

[0xbadcafebee]

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.

[edelbitter]

>bury any negatives

I was looking for the x86-specific rant, and did not find it. You'd think that team would have had something to say about architecture complexity.

[transpute]

Nvidia’s GPU root of trust, where they are using SPARK, is based on RISC-V, they have a talk about that choice, https://news.ycombinator.com/item?id=43045952

[kqr]

> 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.

[ForOldHack]

https://news.ycombinator.com/item?id=27317403

!!!

[zifpanachr23]

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?

[transpute]

NVIDIA GPU RISC-V root of trust is analogous to Apple T2 secure enclave, AMD PSP, or Intel ME, which all perform security-critical functions.

> What exactly is the threat model here

It probably varies by product, but one commercial possibility is protection of price premiums, e.g. enforce feature segmentation for different products or customers, while using common silicon. NVIDIA operating margin reached 50%, unusually high for a hardware company, https://www.macrotrends.net/stocks/charts/NVDA/nvidia/operat.... AMD margin is below 20%.

2021, https://www.youtube.com/watch?v=l7i1kfHvWNI

2024, https://static.sched.com/hosted_files/riscvsummit2024/fe/Key...

  ~1 Billion RISC-V cores shipping in 2024 NVIDIA chips
  Unified embedded HW and SW across all NVIDIA products
    • Eliminates replication in basic primitives (isolation, crypto etc.)
    • Maximizes SW/HW leverage across NVIDIA
  Configuration: pay only for what is needed
  Custom extensions: additional functionality, security, and performance
  Our HW and SW architecture enable differentiation

There are upcoming open hardware/firmware RoT building blocks like OpenTitan (RISC-V), OCP Caliptra and TockOS (Rust) that could be used by competing device and platform vendors.

> don't really perceive much of a security imperative for NVIDIA

When countries start budgeting hundreds of billions of dollars for national investment in LLM-based AI based on GPUs, they may introduce new security requirements for the underlying infrastructure.

[tonyarkles]

Yeah, there's a whole bunch of places where NVIDIA kit is used outside of "graphics cards and slop generators". I work on a drone system based around the Orin AGX and we definitely have "leverage the root of trust functionality to lock down the code that can run on the Orin" on the roadmap before we ever let the hardware end up directly in customers' hands. Root of trust -> Signed Bootloader -> Signed Kernel -> Signed Binaries. There's too much IP that we've spent too much money on to risk having end-users getting access to the raw TensorRT models involved.

[guipsp]

Are you aware of how the nintendo switch got piracy?

[Joel_Mckay]

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

[MrLeap]

GPU rootkits are sounds like misnomer unless they start getting rewritable persistent storage (maybe they do now and my knowledge is out of date).

If you've got malicious code in your GPU, shut it off wait a few seconds, turn it back on.

Actually looking at the definition, my understanding might be off or the definition has morphed over time. I used to think it wasn't a rootkit unless it survived reinstalling the OS.

[Joel_Mckay]

These have direct access to the dma channel of your storage device, and POC have proven mmu/CPU bypass is feasible.

My point was the current architecture is a kludge built on a kludge... =3

[einpoklum]

> with the C++ API

The funny thing is that the "C++ API" is almost entirely C-like, foregoing almost everything beneficial and convenient about C++, while at the same time not being properly limited to C.

(which is why I wrote this: https://github.com/eyalroz/cuda-api-wrappers/ )

> an awful GPU mailbox design is still the cutting-edge tech

Can you elaborate on what you mean by a "mailbox design"?

[pjmlp]

Depends on which CUDA API one is looking to,

https://docs.nvidia.com/cuda/cuda-c-std/index.html

[einpoklum]

I meant the fundamental ones, mostly:

* CUDA Driver API: https://docs.nvidia.com/cuda/cuda-driver-api/index.html * NVRTC: https://docs.nvidia.com/cuda/nvrtc/index.html * (CUDA Runtime API, very popular but not entirely fundamental as it rests on the driver API)

the CUDA C++ library is a behemoth that sits on top of other things.

[Joel_Mckay]

In general, a modern GPU must copy its workload into/out-of its own working area in vram regardless of the compute capability number, and thus is constrained by the same clock-domain-crossing performance bottleneck many times per transfer.

At least the C++ part of the systems were functional enough to build the current house of cards. Best of luck =3

[bsder]

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

[sitzkrieg]

i personaly find firmware in a fighter jet a little more impressive

[timbit42]

ADA and SPARK are used in writing air traffic control systems. I find that impressive.

[kortilla]

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.

[transpute]

> Flagged the article because the title is super misleading

From the case study, the question was posed by Nvidia employees, before finding Ada/SPARK and Adacore, https://news.ycombinator.com/item?id=43043381

  NVIDIA began to ask themselves, “Can we change our fundamental approach? And if so, which of these tools can we actually use?” They put these questions to their software 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?” This led to other questions, like, “What alternative languages and tools are available to support the use of formal methods?” In trying to answer those questions, NVIDIA discovered SPARK.