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.
> 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.
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.
You still do the same thing that you would when calling a C library: you serialize your STL objects into plain C objects, pass them to the external library, and deserialize back. If you need callbacks, you make sure that they catch any exception and return an error code. It's really no different from virtually any other C++ interop.
There are a few languages that interop with C++ at a deeper level, essentially building a small part of a C++ compiler into their runtime. But they're relatively obscure - Clasp, an implementation of Common Lisp, is probably the only one that can really take an arbitrary C++ object (say, an std::vector<std::list<int>>) as an input to a Common Lisp function and work with it.
The bookkeeping overheads might be trivial though. If it boils down to a handful of instructions per call, that's probably not so bad, depending on context. If large buffers are being copied, that's a problem, but hopefully that can generally be avoided.
I don’t think your problem has anything to do with Ada itself. You’d have the same issues using Rust or Go or Swift or Zig or whatever - if you make heavy use of C++’s features, it can make interop with other languages harder
100% It seems like any language other than C has poor interoperability with anything other than C. C++ doesn't know how to deal with the rust borrow checker. Go will have issues with both.
D is an exception - D supports C++ (I'm not sure how or how well, but they at least have some C++ ABI constructors). there are others (some languages running on the JVM usually work with java not C)
> It seems like any language other than C has poor interoperability with anything other than C
Interop between C and classic 3rd generation languages such as Fortran, Pascal, Basic, COBOL, Algol, PL/I, tends to not be that hard [0] – because their feature set is at roughly the same level as C's: just functions/procedures without polymorphism or inheritance, relatively simple (non-OO) data types, etc.
Whereas, C++/Go/Rust/Swift/Ada/etc all add lots of complex features on top, and it is when you use all those complex features, interop with C and classic 3GLs gets harder. Sometimes you can define a subset which omits many of those more complex features and makes interop easier, but then you lose out on the benefits those features bring
[0] one complexity, is for historical reasons, sometimes these languages use different calling conventions than C – but on platforms on which that is an issue, it isn't uncommon for C compilers to support those additional calling conventions as an extension, and newer implementations of those languages for newer platforms are generally converging to C's calling conventions. Another is that some of these languages have data types for which C lacks native support – e.g. many COBOL implementations feature BCD arithmetic – but it is easy to write a routine in C to convert BCD to binary and back.
All the while I've been calling C and C++ code (hard stuff but C++ interop is ... hard) from Ada for 15+ years and calling Ada code from C too. python from Ada and Ada from python too. Ada from Java through JNI. Writing postgres extensions in Ada. It's not always a panacea but it's possible.
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.
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?
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%.
~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.
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.
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
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.
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.
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
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.
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.