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, to name just a few.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.
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.
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.
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.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
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.
My point was the current architecture is a kludge built on a kludge... =3
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"?
At least the C++ part of the systems were functional enough to build the current house of cards. Best of luck =3
* 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.
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.
(And this seems pretty general; you'd have to do roughly the same thing to mix C/Rust, C/Pascal, Rust/Python, ...)
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)
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.
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 other approach is to compile to C++ source.
> 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
> 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.
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.
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.