[HN Gopher] Nvidia Security Team: "What if we just stopped using...
___________________________________________________________________
Nvidia Security Team: "What if we just stopped using C?" (2022)
Author : transpute
Score : 37 points
Date : 2025-02-10 09:16 UTC (3 days ago)
(HTM) web link (blog.adacore.com)
(TXT) w3m dump (blog.adacore.com)
| r1chardnl wrote:
| 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.
| kortilla wrote:
| 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.
| touisteur wrote:
| 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 wrote:
| Ada's refusal to make their language any more approachable is
| a problem.
| Joel_Mckay wrote:
| 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
| jasonpeacock wrote:
| They used SPARK instead: SPARK is a formally
| defined computer programming language based on the Ada
| programming language, intended for the development of high
| integrity software used in systems where predictable and
| highly reliable operation is essential. It facilitates the
| development of applications that demand safety, security,
| or business integrity.
|
| https://en.wikipedia.org/wiki/SPARK_(programming_language)
| roenxi wrote:
| 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.
| bitwize wrote:
| Wow, was not expecting Boomer Rust to take center stage here.
| Awesome results by the security team.
| indolering wrote:
| That's an incredible title!
| NavinF wrote:
| Article doesn't say what parts of Nvidia's stack use SPARK.
| Considering Nvidia is a huge software company with ~30,000
| employees, "There are now over fifty developers trained and
| numerous components implemented in SPARK" doesn't inspire
| confidence.
|
| IMO the realistic path towards formal verification is AI proof
| assistants that automate the tedious parts instead of forcing you
| to write your code in a weird way that's easier to prove
| antirez wrote:
| Totally agree that AI is going to have a huge impact on
| security of languages, and will change many paradigms.
| mr_toad wrote:
| [delayed]
| alexashka wrote:
| > What if we just stopped using C
|
| Then you'd need to have actually competent people in charge.
|
| What happens currently is you just hire nerds and they do their
| nerd stuff. Whatever they do has to be what everyone else is
| doing so that when things aren't working - you can replace them.
|
| If you 'just stop' doing the industry standard practice, you lose
| the option of replacing as means of fixing - you have to actually
| _understand_ what the hell is going on.
|
| People who run things don't like that.
|
| The older I get, the more I'm convinced the limiting factor on
| progress is largely people who get to a senior position, get
| kids, mentally check out at work and just sit there, preventing
| anything that threatens their ability to receive a nice paycheque
| for the next 30-35 years for not doing much of anything.
|
| What facet of society have these clueless schmucks not ruined?
| Whatever people name - it will surely be not because of, but in
| spite of their earnest idiotic efforts.
___________________________________________________________________
(page generated 2025-02-13 23:00 UTC)