[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 : 289 points
Date : 2025-02-10 09:16 UTC (4 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.
| transpute wrote:
| _> 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.
| 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.
| yjftsjthsd-h wrote:
| What's unapproachable about it? And if your answer involves
| syntax, how do you explain Python?
| bluGill wrote:
| Mostly I have no clue how I would use it in my project
| without rewriting from scratch.
| yjftsjthsd-h wrote:
| 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 wrote:
| 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.
| skissane wrote:
| 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
| LiamPowell wrote:
| It's actually a little easier if you use GCC because you
| have interop at the class level:
| https://gcc.gnu.org/onlinedocs/gnat_ugn/Building-Mixed-
| Ada-a...
| bluGill wrote:
| 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)
| tsimionescu wrote:
| 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.
| bluGill wrote:
| now interoperability costs performance for all the
| serialize/deserialize operations and so the language is
| too slow to be practical.
| sitzkrieg wrote:
| not an ada issue
| 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
| MrLeap wrote:
| 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 wrote:
| 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 wrote:
| > 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"?
| Joel_Mckay wrote:
| 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
| pjmlp wrote:
| Depends on which CUDA API one is looking to,
|
| https://docs.nvidia.com/cuda/cuda-c-std/index.html
| einpoklum wrote:
| 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.
| bsder wrote:
| Yeah, when I see the equivalent to slang written in Ada/Spark,
| I'll actually believe them.
| sitzkrieg wrote:
| i personaly find firmware in a fighter jet a little more
| impressive
| 0xbadcafebee wrote:
| 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 wrote:
| >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 wrote:
| 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
| transpute 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._
|
| 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.
| zifpanachr23 wrote:
| 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 wrote:
| 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.macrotrend
| s.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/f
| e/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.
| guipsp wrote:
| Are you aware of how the nintendo switch got piracy?
| kqr wrote:
| > 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.
| 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.
| MichaelDickens wrote:
| Nothing in the article explained what SPARK is. I appreciated
| GP's comment.
| RachelF wrote:
| They actually had to use the non-cutdown version of SPARK that
| this company sells, called SPARK Pro.
| kevlar700 wrote:
| SPARK is free for all to use and is open source. They chose
| to pay for Adacores pro support services and verified pro Ada
| compiler over the FSF GCC/Gnat Ada compiler. Spark is
| actually part of the Gnat compiler (compatibility) but
| actually the slower analysis is done by gnatprove thereby
| keeping compilation and iterative development fast. Nvidia
| can certainly afford to do so of course.
| simon4ada wrote:
| AdaCore's pro support includes more recent releases and, in
| case of problems, wavefronts. That said, the free version
| is fairly recent, and you can get community (and sometimes
| vendor) support.
| SkyMarshal wrote:
| What are wavefronts? Not getting many search results on
| that, besides a few github issues mentioning them.
|
| https://github.com/AdaCore/RecordFlux/issues/955
|
| https://learn.adacore.com/search.html?q=wavefront&check_k
| eyw... (nada)
|
| https://docs.adacore.com/spark2014-docs/html/ug/search.ht
| ml?... (nada)
|
| https://github.com/AdaCore/spark2014/issues?q=wavefront%2
| 0 (nada)
| alberth wrote:
| I really wish there was more active development on SPARK.
|
| It's largely untouched over the last 10-years.
|
| https://github.com/AdaCore/spark2014
|
| For those not aware, SPARK gives even more
| safeguards/guarantees than Rust (see below) ... and also does
| it at compile time (when not all of Rust safeguards are at
| compile time).
|
| https://blog.adacore.com/should-i-choose-ada-spark-or-rust-o...
| mbonnet wrote:
| SPARK has some adherents in spacecraft programming for its
| formal verifiability and safety features.
| 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!
| bitwize wrote:
| Yeah, I gave a talk on Ada a few months back at a local
| meetup. Calling it "Boomer Rust" at the start helped break
| the ice, everyone laughed, and it also helped them get the
| gist of Ada's particular value-add while I went into details.
| harry8 wrote:
| Ada = Boomer Rust <==> Rust = Millennial Ada
|
| I can imagine Boomers laughing but the Rustaceans not seeing
| the humour in it at all. I could be wrong...
| sgt wrote:
| Millennials are getting old though. When is Gen Z going to
| build a language? They probably won't though, because it's
| hard to ask an AI to build a brand new Ada for you.
| xvilka wrote:
| Sadly, Rust still lacks some features that Ada has. For
| example, range types[1] (a narrow case of the dependent
| types).
|
| [1] https://en.wikibooks.org/wiki/Ada_Programming/Types/range
| 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.
| codr7 wrote:
| No doubt, regardless of whether it fails epically or not.
| antirez wrote:
| lol good point.
| mr_toad wrote:
| There are probably 50 developers working on the actual drivers
| and several thousand on GeForce Experience.
| sdwr wrote:
| Don't they release custom tuning patches for every single AAA
| game that comes out? Geforce Experience is basically just a
| spoonful of sugar to make sure people install new drivers.
| dogma1138 wrote:
| I'm not entirely sure they are writing any portion of their
| driver using SPARC the presentation they gave 5 years ago seems
| to indicate they are limiting the usage to firmware for their
| embedded RISC-V co-processor, they may have expanded the usage
| of it but I still think it's predominantly firmware related
| with possibly some expansion to their automotive and robotics
| solutions.
|
| https://www.slideshare.net/slideshow/securing-the-future-of-...
| ipsum2 wrote:
| SPARC and SPARK are two entirely different things.
| dogma1138 wrote:
| Indeed they are, the misspelling is on my end :)
| zitterbewegung wrote:
| I feel like it's going to be a step further and we won't write
| actual "code" but more like comprehensive tests and it
| generates the code . Sort of like the movement from assembly to
| C
| bawolff wrote:
| Historically AI has been pretty bad with this. Machine
| learning is famous for finding solutions that pass all the
| test cases in out of the box ways but don't do what you want.
| makeitdouble wrote:
| Writing comprehensive tests is the part we're weakest at
| IMHO.
|
| That's the same paradigm as outsourcing development at some
| cheap place and doing acceptance tests against the result. It
| saves money but that's not how you'd build an airplane for
| instance...
| randomNumber7 wrote:
| > that's not how you'd build an airplane for instance...
|
| Unless you want it going boing boing boeing.
| Jean-Papoulos wrote:
| Unfortunately humans will probably stay very bad at writing
| tests that covers all possible cases. And who's gonna test
| the tests ?
| btown wrote:
| I'd also add that AI code generation in non-formally-verifiable
| languages, at places with concurrency requirements like Nvidia,
| might end up in the short-term creating _more_ hard-to-spot
| concurrency bugs than before, as developers become incentivized
| to tab-complete code without fully thinking through the
| implications as they type.
|
| But AI code generation for _formally verifiable programs_? And
| to assist in writing custom domain-specific verifiers? Now that
| 's the sweet spot. The programming languages of the future, and
| the metaprogramming libraries on top of them, will look really,
| really cool.
| erichocean wrote:
| > But AI code generation for formally verifiable programs?
|
| For verifiable domains, this really is the sweet spot.
|
| An annoying aspect of verification-in-practice is that it is
| just really bulky--there's a lot to type in, and it's
| tedious.
|
| LLMs, especially the latest crop of weak-reasoning models,
| are great for this.
| atiedebee wrote:
| I tested o3-mini yesterday, having it verify a bit-hack for
| "vectorizing" 8x8bit integer addition using a single 64 bit
| int value[0]. Suffice to say, I am not impressed. I asked
| it to give me a counter example that would make the
| function fail, or to tell me that it works if it does. It
| mentioned problems regarding endianness which weren't
| present, it mentioned carries that would spill over which
| couldn't happen. I had given it chances to give counter
| examples, but the counterexamples he gave didn't fail.
|
| Only after telling it that I tested the code and that it
| works did it somewhat accept that the solution worked.
|
| I think a deterministic, unambiguous process is a lot more
| valuable for formal verification.
|
| [0] https://chatgpt.com/share/67aefb63-f60c-8002-bfc6-c7c45
| b4520...
| hyperman1 wrote:
| A limitation I see with AI for coding is that your
| problem must be mainstream to get decent results.
|
| In my experience, if I ask it to do web things in PHP or
| Java, data things in Python, ... it gives a good enough
| result. If I ask it a postgis question, I get an answer
| with hallucinated APIs, bugs, and something that doesn't
| even do what I want if it works.
|
| I suspect the ADA/Spark world and the formal verification
| world are to small to decently train the AI.
| amoss wrote:
| > A limitation I see with AI for coding is that your
| problem must be mainstream to get decent results.
|
| Or to phrase it another way, there must examples of the
| technique that you want to "generate" in the training set
| otherwise the horrifically overfitted model cannot work.
|
| Probably a little bit too cynical but this is my
| experience asking LLMs "unusual" questions.
| nottorp wrote:
| Seems realistic.
|
| I tried asking a LLM for a full code snippet for the
| first time yesterday (i've been using them as search
| engines better than google, which isn't saying much,
| before).
|
| It produced code that compiled but failed to do anything
| because the 3rd api call it generated returned an error
| instead of doing what the LLM said it would do.
|
| Didn't spend time on seeing what was wrong because we
| already had a library that did the same thing; I was more
| testing what the LLM can do.
| TheOtherHobbes wrote:
| No, that's about where we are. Today's LLM coding is
| basically automated Stack Overflow copy/paste - not too
| bad for anything simple and mainstream, but unable to
| reason about code from first principles, and fond of
| making up random shit that looks good but doesn't work.
| brabel wrote:
| I thought OP was saying AI can generate the code that can
| then be formally verified based on your non-verifiable
| code, not that the AI itself is verifying it? I could be
| wrong, of course.
| atiedebee wrote:
| Perhaps I misread it then. I think that if you're at the
| point of using formal verification you're likely to be
| very meticulous in whatever you're writing, so an AI
| would be used quite carefully
| stefan_ wrote:
| Have you tried it for Rust, arguably a much lower bar than
| actually fully formally verifiable? Sorry to say but AI can't
| figure out the borrow checker. I'd speculate it does poor on
| a lot of things that are sort of implicit in the code /
| properties of the grand structure rather than incremental
| text things.
| kevlar700 wrote:
| There is a podcast and blackhat? video about Nvidia
| choosing SPARK over Rust. Not because of formal
| verification at all but because it is a more developed
| prospect and offers better security even without any formal
| verification. This isn't mentioned but Ada is also far
| better at modelling registers or even network packets.
|
| I might consider AI if it utilised SPARKs gnat prove but I
| wouldn't usw AI otherwise.
| LiamPowell wrote:
| As an example of modelling packets, here's an example of
| modelling a complex packet which is a bit-packed tagged
| union. I don't think many other languages make such
| packets so easy to declare: https://gist.github.com/liamp
| wll/abaaa1f84827a1d81bcdb2f5f17...
| xxpor wrote:
| p4? Granted, that's not something that just compiles to a
| usable language.
| TheOtherHobbes wrote:
| AI means some future more rigorous system than today's
| Clippy++ LLMs.
|
| At least that's what it should mean. It's not clear if
| that's going to happen.
| steveklabnik wrote:
| > Sorry to say but AI can't figure out the borrow checker.
| I'd speculate it does poor on a lot of things that are sort
| of implicit in the code / properties of the grand structure
| rather than incremental text things.
|
| I don't really use AI tools, but in the past few weeks I've
| tried it with Rust and while it had problems, borrow
| checking errors were never part of them.
|
| I fully agree that LLMs don't "understand," but people also
| really oversell the amount of thinking needed to satisfy
| borrowing in a lot of cases.
| siknad wrote:
| Maybe better performance can be achieved with specialized
| models. There are some that were able to solve mathematical
| olympiad problems, e.g. AlphaProof.
| dmix wrote:
| > as developers become incentivized to tab-complete code
| without fully thinking through the implications as they type.
|
| Is this true? There should always be a QA process and you
| should always carefully review when committing. The writing
| process doesn't influence that unless you're automating whole
| swaths you don't understand during reviews.
| nostrademons wrote:
| I had a production bug (caught in canary) introduced into
| Google Play in just this manner. The AI code review assist
| suggested switching a method to a more modern alternative,
| both the author and code reviewer thought the AI suggestion
| was a good one, the new alternative was documented as not
| being safe to use in the onCreate() method of an Android
| activity, the code in question was not in onCreate but was in
| a method transitively called by onCreate in a different
| Activity, boom goes an unrelated Activity. Would've been
| caught trivially by an expressive type system, but the LLM
| doesn't know that.
| transpute wrote:
| _> Article doesn 't say what parts of Nvidia's stack use
| SPARK._
|
| Their linked case study lists three examples and one category,
| https://www.adacore.com/uploads/techPapers/222559-adacore-nv...
| - image authentication and integrity checks for the overall GPU
| firmware image - BootROM and secure monitor firmware
| - formally verified components of an isolation kernel for an
| embedded operating system - In general, their targets
| tend to be smaller code bases that would benefit the most from
| SPARK's strong typing, absence of runtime errors, and in some
| cases, rigorous formal verification of functional properties
|
| More details in 2021 talk on RISC-V root of trust in Nvidia
| GPUs, https://www.youtube.com/watch?v=l7i1kfHvWNI
|
| _> NVRISCV is NVIDIA's implementation of the RISC-V ISA and
| Peregrine subsystem includes NVRISCV and multiple peripherals.
| They show how fine-grain access controls, formally verified for
| correctness, allow following the principle of least privilege
| for each partition. NVRISCV provides secure boot that starts
| with an immutable HW, the chain of trust extends to the Secure
| Monitor in SW, where partition policies are set up and
| isolation enforced using HW controls.. Boot and Secure Monitor
| software is implemented in SPARK._
| antonvs wrote:
| > doesn't inspire confidence.
|
| Haha what?
|
| What are you comparing this to?
| UltraSane wrote:
| formal verification is normally used on the most security
| critical code so even 50 programmers is a lot.
| lou1306 wrote:
| It bears repeating that Nvidia is not strictly speaking a SW
| company. It is a semiconductors company. That 30k employees
| figure includes _all_ Nvidia employees, not all of which are in
| software.
|
| I am rather skeptical of AI in this context. Until you have
| verifiably correct AI assistants, you still need a highly
| skilled human in the loop to catch subtle errors in the proofs
| or the whole result is moot anyway.
|
| And there _are_ tools out there capable of verifying C code,
| but for a greenfield project implementation/verification in a
| higher-level, formal language + verified compilation might make
| more sense.
| swiftcoder wrote:
| The article seems fairly clear that it is the security folks
| within Nvidia that are spearheading this. 50 engineers on the
| security team doesn't seem unreasonable for a company of that
| size.
| einpoklum wrote:
| TBH, this sounds like somewhat of a nothing-burger published by
| an organization with a motivation to overstate the use of Ada /
| Spark.
|
| Specifically, the article does not claim that any significant bit
| of code at NVIDIA uses SPARK or Ada.
| uxp100 wrote:
| Significant bits of code at NVIDIA use SPARK. Small percentage
| of total code written, but in significant places.
| einpoklum wrote:
| > Significant bits of code at NVIDIA use SPARK.
|
| That is a vacuous statement, because:
|
| * We don't know what constitutes "significant"
|
| * We don't know what it's significant _for_
|
| * "code at NVIDIA" is an extremely wide definition.
| transpute wrote:
| Details, slides and video are in this HN discussion, linked
| from sibling response. vacuous: Devoid of
| substance or meaning; vapid or inane.
| disingenuous: Pretending to be unaware or unsophisticated;
| faux-naif. guarded: Cautious; restrained.
| transpute wrote:
| The linked Nvidia case study names GPU firmware components,
| https://news.ycombinator.com/item?id=43043541
| chadcmulligan wrote:
| Any Spark compiler? I've found https://www.adacore.com/sparkpro
| which says request pricing - never good, any open ones suitable
| for playing with?
| ajxs wrote:
| There's a GPL version of GNATprove, which you can install with
| Alire (https://alire.ada.dev). That's the version I use.
| LeFantome wrote:
| Pretty huge promotional opportunity for AdaCore. You can tell
| because this was written by AdaCore.
|
| Still, I am a bit convinced. The NVIDIA name is increase the
| chance that I will evaluate SPARK sometime soon. I have to admit,
| other than knowing it exists, I am not super familiar with it.
| What I have seen before now has felt like them using the
| popularity of Rust as a platform for promotion. This, at least,
| appears to be a use case where they came in on their own merits.
| transpute wrote:
| _> huge promotional opportunity_
|
| Right? Yet they published this customer case study in 2022 and
| it never reached HN. Found in 2025 search on GPU firmware
| security.
| Aissen wrote:
| Already a year late, but this one made the rounds:
|
| https://news.ycombinator.com/item?id=33504206
| transpute wrote:
| Thanks. Just three weeks before the ChatGPT launch that
| would accelerate Nvidia's fortunes!
| 8organicbits wrote:
| It's hard to tell what components are now written in spark. The
| driver is mostly c, and none of the open source repos are
| identified as spark.
|
| https://github.com/NVIDIA/open-gpu-kernel-modules
|
| https://github.com/NVIDIA/
| transpute wrote:
| Their PDF has a bit more detail,
| https://news.ycombinator.com/item?id=43043541
| cxr wrote:
| I maintain conviction in my position that if AdaCore and/or other
| champions of Ada were to undertake a serious project (i.e. not an
| April Fools' Day joke blog post[1]) to ship a compiler that
| accepts a curly-braced dialect of the language[2][3], then there
| would be at least twice as many new, earnest users of the vulgar
| "skinned" form as there are programmers today using the existing
| language, and that this tripling would happen virtually
| overnight.
|
| I'm not even talking about major revisions to the grammar. I'm
| saying fork the lexer to accept a different set of terminals, and
| leave the nonterminals alone.
|
| Is this stupid and unreasonable and should programmers just get
| over themselves and use a language on the strength of its merits
| instead of being turned off by surface-level stuff? Yeah, it is,
| and yeah, they should. But people are fickle.
|
| 1. <https://blog.adacore.com/a-modern-syntax-for-ada>
|
| 2. <https://news.ycombinator.com/item?id=24367358>
|
| 3. <https://news.ycombinator.com/item?id=35217839>
| coliveira wrote:
| Nothing prevents anyone from creating a preprocessor that maps
| { to BEGIN and } to END.
| cxr wrote:
| Nothing prevents anyone from trying to eat spaghetti with a
| spoon. (Or from modifying the lexer to accept a different set
| of terminals, even.)
|
| > _Kramer: "Yeah, well, I could do it. I don't wanna do it."_
|
| > _Jerry: "We didn't bet if you wanted to do it. We bet on if
| it would be done."_
|
| > _Kramer: "And-- and it could be done."_
|
| > _Jerry: "Well of course it COULD be done. Anything COULD be
| done. But it's only is done if it's done! Show me the levels!
| The bet is the levels!"_
|
| > _Kramer: "I don't want the levels!"_
|
| > _Jerry: "That's the bet!"_
|
| <https://www.youtube.com/watch?v=4CxIVvLaGKI>
| SSLy wrote:
| Spaghetti is eaten with spoon and fork...
| windward wrote:
| Impelementing the grammar is the easiest 0.1% of programming
| language dissemination.
|
| Adding explicit non-const to g++ would be so, so easy. But
| pointless.
| rramadass wrote:
| Not related to Ada, but Dafny is a "Verification aware
| programming Language" where both Formal Specification and
| Verification are combined together in the same source language
| - https://dafny.org It uses curly braces and can generate code
| for a number of different languages at the backend (eg. Java,
| C#, Go, Python, Javascript, C++).
|
| I haven't played with it yet but just from reading the
| documentation i really like this approach since you need learn
| only one language/toolchain for both formal
| specification/verification and implementation. But by giving
| one the flexibility to generate code to various mainstream
| languages you can slowly add verified code module by module to
| existing codebases.
| juped wrote:
| I'm also desperate to stop Rust by any means, but I don't think
| you're correct; I think the sticking point for language
| adoption is the presence or absence of a big npm clone.
| steveklabnik wrote:
| Alire has existed for a long time now; the oldest release on
| GitHub is 0.4 from 2018.
| devit wrote:
| That would be a good start as the current syntax is absurd.
| marssaxman wrote:
| It's not absurd, it's just out of fashion. Ada syntax comes
| from the same heritage as Pascal, which was as popular as C
| during the 80s (and sometimes even more so).
| mbonnet wrote:
| Pascal died for several very good reasons.
| marssaxman wrote:
| That may well be, but syntax was not one of them. Someone
| who came into programming more recently and has only used
| curly-brace languages might not immediately understand
| what they are looking at, but that doesn't make it
| _absurd_ - it 's just different.
| shipp02 wrote:
| You are right but the vhdl-like syntax is quite nice. It does
| some surprisingly modern things.
| PaulHoule wrote:
| Efficiency of Ada should be pretty close to C, but that strange
| thing Ada does where you define your own numeric types like
| type Day_type is range 1 .. 31;
|
| creeps me out a little, it makes me think I have to throw _Hacker
| 's Delight_ [1] in the trash if I want to use it but I could be
| wrong. It makes me think of the the deep history of computing,
| where there were a few straggler architectures (like the PDP-10
| [2]) that didn't use the 8-bit byte were around and when Knuth
| wrote a set of programming books based on an instruction set that
| wasn't necessarily binary.
|
| (Lately I was thinking about making a fantasy computer that could
| be hosted in Javascript which was going to be RISC but otherwise
| totally over the top, like there would be bitwise addressing like
| the PDP-10. First I wanted it to be 24 bit but then I figured I
| could pack 48 bits in a double so I might as well. It even would
| have a special instruction for unpacking UTF-8 characters and a
| video system intended for mixing latin and CJK characters. Still
| boils down to an 8-bit byte but like the PDP-10 it could cut out
| 11-bit slices or whatever you want. I was going to say _screw C_
| but then I figured out you could compile C for it)
|
| [1] https://en.wikipedia.org/wiki/Hacker%27s_Delight
|
| [2] https://en.wikipedia.org/wiki/PDP-10
| taurknaut wrote:
| This doesn't strike me as that different than an enum.
| MathMonkeyMan wrote:
| Arithmetic is defined on range types. So day 30 + day 4 is
| 34, which if you then try to coerce into a day will throw an
| exception.
| dragonwriter wrote:
| And... So? It seems you are saying Day_type + Integer is
| Integer, and Integer (in general) cannot safely be coerced
| into Day_type and... that's logically correct?
| MathMonkeyMan wrote:
| `Day_type + Day_type` is also defined, and it overflows.
| That's like normal integers, and unlike enums.
| Tadpole9181 wrote:
| Love that feature, along with derived types[1] and subtype
| predicates[2]. There's a special place in my heart partitioned
| for things that won't let you screw things up.
|
| [1] https://learn.adacore.com/courses/intro-to-
| ada/chapters/stro...
|
| [2]
| https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Devel...
| yjftsjthsd-h wrote:
| Alright, this is Hacker news, so I'm gonna nitpick...
|
| > It even would have a special instruction for unpacking UTF-8
| characters
|
| From
| https://en.wikipedia.org/wiki/Reduced_instruction_set_comput...
| :
|
| > The term "reduced" in that phrase was intended to describe
| the fact that the amount of work any single instruction
| accomplishes is reduced--at most a single data memory cycle--
| compared to the "complex instructions" of CISC CPUs that may
| require dozens of data memory cycles in order to execute a
| single instruction.
|
| I don't think what you're describing is a RISC processor at
| all.
| kbolino wrote:
| Whether accelerated UTF-8 decoding breaks RISC-ness is an
| interesting question, and not one with an obvious answer IMO.
|
| Supposing we loaded 4 bytes into a register with a load
| instruction (quite RISC), we could then have a "decode UTF-8"
| instruction which could set two output registers: one
| receiving the decoded code point, and the other receiving the
| number of bytes consumed (1-4). That's another perfectly
| RISCy operation: read one input register, operate on it,
| update two output registers. Most RISC architectures also
| allow base+offset addressing at least, so you can chain this
| to another load using the output of that second register;
| worst case, you'd need to add base+offset in a dedicated
| instruction. No violations of RISC here.
|
| However, you'd start running into problems with alignment.
| Loading 4 bytes into a register typically requires 4-byte
| alignment, but UTF-8 is a variable-length encoding (hence the
| desire to accelerate it in the first place!). Is unaligned
| load RISCy? Many architectures now support it, but they
| usually didn't start off with it. Then again, 64-bit
| architectures can just ignore the problem entirely, since
| they can load 8 bytes at a time, which will always be enough
| to fit an arbitrary 4-byte value at any alignment. You'd just
| need to shift the value in the register by the amount of the
| misalignment, which is another valid RISC operation.
|
| If you wanted to sidestep the alignment issue, then an
| alternate solution would be to decode the UTF-8 sequence
| straight from memory, but that definitely feels more like
| CISC to me.
| nottorp wrote:
| Not only Ada?
|
| Pascal is less esoteric and has had that forever.
| PaulHoule wrote:
| My feelings about Pascal are pretty mixed.
|
| Pedagogically oriented computer science profs circa 1980 were
| aghast that BASIC had become the standard for teaching young
| people to program. It was difficult to fit Pascal into a
| microcomputer then, so we were stuck with the atrocious UCSD
| Pascal [1] which used a virtual machine to make up for the
| weak instruction sets of many micros, particularly the 6502.
| Since the compiler ran inside the VM, compiling a small
| Pascal program was like compiling a large C++ program today.
|
| Not long after that I got to use Pascal on a VAX which was
| not so bad, but pretty obviously not up to doing systems
| programming, particularly compared to C, which was starting
| to show up on micros such as Z-80s running CP/M and the
| TRS-80 Color Computer running OS-9.
|
| Then I got a 80286 computer and I _really_ liked Turbo Pascal
| because it added the (non-standard) facilities you need to do
| systems work, but went back to C when I went to school
| because it was portable to the 68k and SPARC based Sun
| machines we had.
|
| [1] https://en.wikipedia.org/wiki/UCSD_Pascal
| nottorp wrote:
| > compared to C, which was starting to show up on micros
| such as Z-80s running CP/M
|
| I had some very limited access to CP/M z80 machines.
| Probably somewhere between 86-90. All I remember about the
| C compiler they had is that I had to swap 2 or 3 floppies
| to produce a linked executable, so it sounds similar to
| this UCSD Pascal.
|
| My first real contact with Pascal was Turbo Pascal, and
| that ran loops around any other compiler I had access to
| back then...
| PaulHoule wrote:
| I had a Coco with 2 floppies, I could compile C without
| any swapping. OS-9 was a real multitasking operating
| system, I could log into it with the keyboard and mouse
| and two serial ports at the same time (one with a UART,
| another with the terrible bit banger) The latter wasn't
| too bad with the portable DEC printing terminal I got
| that that was surplus at a credit agency.
|
| UCSD Pascal was one of very few compiled languages you
| could get for the Apple ][ and other 6502 machines
| because the virtual machine was an answer to problem of
| code generation for that terrible instruction set with
| insufficient registers and addressing modes.
| TZubiri wrote:
| "Testing security is pretty much impossible. It's hard to know if
| you're ever done,"
|
| "We wanted to emphasize provability over testing as a preferred
| verification method"
|
| Yet another developer seeking a panacea that will allow them to
| keep their job while diminishing their workload.
|
| For typical workers, it's a fact that work is infinite, so you
| put your 8 hours and then do it again the other day.
|
| Whenever devs get put in this position they go for the nuclear
| option of going for the moon.
|
| Man just keep finding bugs to the best of your ability, it will
| never be 100% secure, except insofar as you gerrymander what's a
| vulnerability and what is your responsibility.
|
| Good luck. But if I have to put my chips in Nvidia's VP vs C, I
| put them in C. The list of C contenders has been long, and it
| seems more likely that the vp is at the peak of their life ala
| musk or altmann and they have their own delusions. Not sure
| whether going to mars is crazier or whether finally replacing C
| is.
| tombert wrote:
| I've never used SPARK, but the Wikipedia page makes it seem
| pretty interesting.
|
| For that matter, Ada seems interesting, I kind of wish it had
| caught on outside of the defense industry.
| numeromancer wrote:
| It failed to catch on outside the defense industry because that
| is where is started. It was long sneered at as a "language
| designed by committee".
|
| In one programming class, in college, we used a text-book
| called "Oh my, Modula 3!". On the back they explained the
| title, saying "better 'Oh my, Modula 3!' than 'Oh no, Ada!'".
| tombert wrote:
| Yeah, people have explained to me here before.
|
| It's just too bad, because Ada looks like a language that
| should have gotten more popular. I was playing with some of
| the concurrency constructs built into it, and it was fairly
| pleasant, and it makes me think about the "what if?" universe
| where it caught on instead of C++ dominating the 90's and
| 2000's.
| dang wrote:
| Discussed at the time:
|
| _Nvidia Security Team: "What if we just stopped using C?"_ -
| https://news.ycombinator.com/item?id=33504206 - Nov 2022 (362
| comments)
| white-flame wrote:
| The real problem is deeper than this. The actual question to ask
| is:
|
| "What if we just stopped distributing and blindly executing
| untrusted binary blobs?"
|
| A trusted compiler in the OS, and some set of intermediate
| representations for code distribution would solve a massive
| amount of security issues, increase compatibility, and allow for
| future performance increases and disallowing suspect code
| patterns (spectre, rowhammer, etc). Specializing programs at
| install time for the local hardware makes way more sense than
| being locked into hardware machine code compatibility.
| bawolff wrote:
| I feel like you might as well ask "why not world peace"?
|
| There are a huge number of practical issues to be solved to
| make that be viable.
| grayhatter wrote:
| could you list a few of the problems you predict?
| tsimionescu wrote:
| That does nothing to fix the vast majority of security issues,
| which are caused by trusted but not memory safe programs
| running on untrusted input.
|
| It's also an extremely unrealistic goal. First of all, you run
| into a massive problem with companies and copyright. Second of
| all, it will be very hard to convince users that it's normal
| for their Chrome installation to take half an hour or more
| while using their CPU at 100% the whole time.
| transpute wrote:
| For a while, Apple required apps to be submitted as bitcode
| (LLVM IR) to the App Store, where they would be converted to
| x86 or Arm machine code during device install. They stopped
| that a couple of years ago, after migration to Apple Silicon.
| refulgentis wrote:
| Apple used to require bitcode (LLVM IR) for App Store
| submissions.
|
| Rest is interesting, nothing was done on install, it wasn't
| converted or anything to machine code.
|
| In fact, in practice, it never ended up being used.
|
| Well, that's not particularly relevant: the idea was never to
| do something on device anyway.
|
| Really excellent post here summarizing that I can vouch for:
| https://stackoverflow.com/questions/72543728/xcode-14-deprec.
| ..
| transpute wrote:
| Thanks for the correction and link. Relevant to the comment
| above about binary blobs:
|
| _> The idea to have apps in a CPU neutral form available
| on the app store is not a bad one; that 's why Android
| chose Java Byte Code (JBC). Yet JBC is a pretty stable
| representation that is well documented and understood,
| Bitcode isn't. Also on Android the device itself transforms
| JBC to CPU code (AOT nowadays)._
| kbolino wrote:
| The general idea is correct, but a rather significant
| detail is not.
|
| Android did not choose Java bytecode, it chose Dalvik
| bytecode [1]. This was done for several reasons, but at a
| high level, Dalvik bytecode more closely matches how real
| computers work while Java bytecode targets a more
| abstract virtual machine. This result is that Dalvik
| bytecode is easier to transform into machine code, and
| more optimizations are done in the source code ->
| bytecode phase rather than the bytecode -> machine code
| phase, relative to Java bytecode.
|
| [1]: https://source.android.com/docs/core/runtime/dalvik-
| bytecode
| transpute wrote:
| Thanks for the additional detail,
| https://en.wikipedia.org/wiki/Dalvik_(software)
|
| _> Programs for Android are commonly written in Java and
| compiled to bytecode for the Java Virtual Machine, which
| is then translated to Dalvik bytecode.. The successor of
| Dalvik is Android Runtime (ART), which uses the same
| bytecode and .dex files (but not .odex files), with the
| succession aiming at performance improvements._
| arbitrandomuser wrote:
| How did that work though ? Isn't bitcode tied to a target
| triplet ?
| pabs3 wrote:
| > "What if we just stopped distributing and blindly executing
| untrusted binary blobs?"
|
| You can do that right now with open source software and
| Bootstrappable Builds.
|
| https://bootstrappable.org/ https://lwn.net/Articles/983340/
| watt wrote:
| There is a rule that if somebody poses this hypothetical with
| the word "just" in it, they have signed themselves up to go and
| implement it.
|
| So, congratulations, take it and run with it.
| Taikonerd wrote:
| The VST Lab at Princeton works on this sort of problem:
| https://vst.cs.princeton.edu/
|
| "The Verified Software Toolchain project assures with machine-
| checked proofs that the assertions claimed at the top of the
| toolchain really hold in the machine-language program, running
| in the operating-system context."
|
| Some of the same researchers worked on TAL (typed assembly
| language), which sounds like it could be one of the
| "intermediate representations" you mentioned.
| skirge wrote:
| ""Beware of bugs in the above code; I have only proved it
| correct, but didn't test it"
| randomNumber7 wrote:
| Yes, lets just use pascal. Who needs dynamic memory allocation
| and functions that can take strings of multiple length?
| bawolff wrote:
| We are talking about firmware. I am just a web dev and dont
| know much about the embedded space, but my impression was that
| dynamic memory allocation is usually problematic in firmware in
| general.
| LiamPowell wrote:
| SPARK supports both of these things.
| nottorp wrote:
| Spark is Ada not Pascal.
|
| Pascal strings used to have their actual length in a field at
| the beginning of the string. Imagine how many off by one errors
| and how many (even hidden) calls to strlen() that saves.
|
| All they needed to modernize Pascal is some library code to
| resize the buffer if needed, just like curly brace languages.
| It may already be present in modern Pascal implementations, I
| haven't followed.
|
| Pascal also has array bounds checking by default. Imagine how
| many out of bounds errors this could prevent.
|
| But no, you have to have curly braces instead and build layers
| and layers of classes and languages over classes, all over the
| same impractical string representation.
| pjmlp wrote:
| Object Pascal and Delphi dialects have had open arrays for
| ages.
|
| And this was even fixed in ISO Extended Pascal by 1990.
|
| Not to mention that Wirth fixed this in Modula-2 in 1978,
| already, which everyone keeps forgeting it was actually
| designed for systems programming, while Pascal was originally
| designed in 1972 for teaching programming concepts.
|
| But sure enough, lets complain about ISO Pascal from 1976.
| pjmlp wrote:
| Stuck in 1976 Pascal?
| anta40 wrote:
| Imagine if "we" are OS/embedded dev folks.
|
| I mean, for writing userland apps, various langs come and go. But
| for writing OS, after more than 4 decades, C is still there.
|
| :D
| sylware wrote:
| It would mean we need more RISC-V performant hardware. Because
| the real and honnest way out from C is assembly (with super high
| level languages with interpreters written in assembly). And it
| means a worldwide royalty free standard.
|
| I guess we could get a middle ground with a simpler C dialect
| with the bits required for modern hardware architecture
| programming (no integer promotion, no implicit casts, only sized
| type, only one loop keyword, no switch...). The defining criteria
| for this language: it must be easy to get a real-life bootstrap
| compiler with one dev (reasonable amount of time, effort, etc).
|
| I am currently coding many of my applications in RISC-V assembly,
| with a small interpreter to run them on x86_64, dodging complex
| macro-preprocessors (I use the basic features of a C
| preprocessor, I don't even use the RISC-V pseudo-ops).
|
| The only thing keeping me on x86_64 are video games for linux and
| the fact that x86_64 micro-archs are mature, performant wise.
| tehologist wrote:
| Why not just use a verifiable subset of C?
| https://compcert.org/compcert-C.html
| aeneasmackenzie wrote:
| Compcert guarantees that the executable that comes out does
| what the code that went in said, it doesn't guarantee much
| about the code that went in.
| LiamPowell wrote:
| There's also Frama-C, but having used both Frama-C and SPARK
| I can say I'd pick SPARK any day. Having a rich type system
| and not having to work with pointers makes proving a program
| so much easier.
| outside1234 wrote:
| And then they invented their own language with security holes.
| cdevries wrote:
| "Beware of bugs in the above code; I have only proved it correct,
| not tried it." - Donald Knuth
___________________________________________________________________
(page generated 2025-02-14 23:02 UTC)