5 ms·

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 deve

by NavinF 2y ago

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 2y ago
Totally agree that AI is going to have a huge impact on security of languages, and will change many paradigms.
- codr7 2y ago
  No doubt, regardless of whether it fails epically or not.
  - antirez 2y ago
    lol good point.
mr_toad 2y ago
There are probably 50 developers working on the actual drivers and several thousand on GeForce Experience.
- sdwr 2y ago
  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 2y ago
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-safety-and-security-of-embedded-software/217232842 https://www.slideshare.net/slideshow/securing-the-future-of-...
- ipsum2 2y ago
  SPARC and SPARK are two entirely different things.
  - dogma1138 2y ago
    Indeed they are, the misspelling is on my end :)
- deleted 2y ago
  [deleted]
zitterbewegung 2y ago
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 2y ago
  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.
  - NavinF 2y ago
    That hasn't been my experience. I've mostly seen fake stories along those lines. Eg https://gwern.net/tank https://gwern.net/tank
- makeitdouble 2y ago
  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 2y ago
    > that's not how you'd build an airplane for instance... Unless you want it going boing boing boeing.
- Jean-Papoulos 2y ago
  Unfortunately humans will probably stay very bad at writing tests that covers all possible cases. And who's gonna test the tests ?
btown 2y ago
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 2y ago
  > 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 2y ago
    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-c7c45b452018 https://chatgpt.com/share/67aefb63-f60c-8002-bfc6-c7c45b4520...
    - hyperman1 2y ago
      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.
transpute 2y ago
> 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-nvidia-case-study-v5.pdf 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 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 2y ago
> doesn't inspire confidence. Haha what? What are you comparing this to?
- NavinF 2y ago
  Compared to the other 99.9% of the company that doesn't use SPARK. It's all tests and static analysis
UltraSane 2y ago
formal verification is normally used on the most security critical code so even 50 programmers is a lot.
lou1306 2y ago
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 2y ago
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.
- NavinF 2y ago
  I don't believe that: https://news.ycombinator.com/item?id=43042166 https://news.ycombinator.com/item?id=43042166

by NavinF 2y ago

antirez 2y ago

Totally agree that AI is going to have a huge impact on security of languages, and will change many paradigms.

codr7 2y ago
No doubt, regardless of whether it fails epically or not.
- antirez 2y ago
  lol good point.

mr_toad 2y ago

There are probably 50 developers working on the actual drivers and several thousand on GeForce Experience.

sdwr 2y ago
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 2y ago

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-safety-and-security-of-embedded-software/217232842 https://www.slideshare.net/slideshow/securing-the-future-of-...

ipsum2 2y ago
SPARC and SPARK are two entirely different things.
- dogma1138 2y ago
  Indeed they are, the misspelling is on my end :)
deleted 2y ago
[deleted]

zitterbewegung 2y ago

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 2y ago
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.
- NavinF 2y ago
  That hasn't been my experience. I've mostly seen fake stories along those lines. Eg https://gwern.net/tank https://gwern.net/tank
makeitdouble 2y ago
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 2y ago
  > that's not how you'd build an airplane for instance... Unless you want it going boing boing boeing.
Jean-Papoulos 2y ago
Unfortunately humans will probably stay very bad at writing tests that covers all possible cases. And who's gonna test the tests ?

btown 2y ago

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 2y ago
> 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 2y ago
  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-c7c45b452018 https://chatgpt.com/share/67aefb63-f60c-8002-bfc6-c7c45b4520...
  - hyperman1 2y ago
    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.

transpute 2y ago

> 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-nvidia-case-study-v5.pdf 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 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 2y ago

> doesn't inspire confidence. Haha what? What are you comparing this to?

NavinF 2y ago
Compared to the other 99.9% of the company that doesn't use SPARK. It's all tests and static analysis

UltraSane 2y ago

formal verification is normally used on the most security critical code so even 50 programmers is a lot.

lou1306 2y ago

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 2y ago

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.

NavinF 2y ago
I don't believe that: https://news.ycombinator.com/item?id=43042166 https://news.ycombinator.com/item?id=43042166