Skip to content
Hallway
0:00 / 0:00

#ada#spark#nvidia

NVIDIA — Securing the Future of Safety and Security of Embedded Software (Captioned)

AdaCore

4.4K subscribers • 2 videos on Hallway

YouTube
  • Recommended by 1 person: 1 on Hacker News.
  • Made by the vendor. The company whose product it covers made or sponsored it.

Intermediate. Assumes working knowledge.

4.9K views5 years ago1 recommendation

SecurityProgramming languagesEmbedded systemsWeb and application securityFormal methods and verification

NVIDIA engineers explain why and how they adopted the Ada and SPARK programming languages for security-critical embedded firmware.

SPARK / Ada Journey to Adoption As software becomes more complex, the chances of human error greatly increase, opening up potential for security and safety risks. NVIDIA is working with AdaCore to implement Ada and SPARK programming languages into certain firmware elements to reduce this potential error. In this webinar you will learn how the combination of NVIDIA hardware with Ada and SPARK delivers robustness and security, improving efficiency and safety in the development pipeline. - Intro by Patrick Mannion - Business context for Ada and SPARK at NVIDIA by Daniel Rohrer - Technical aspects of NVIDIA's adoption of SPARK by Dhawal Kumar - Firmwares and their environment - What is this SPARK that we've all been raving about? - SPARK alternatives considered (and dismissed) - Proof of Concept — It's conclusions and concerns - Benefits and Summary - Q and A

Why it's here

1 person recommends this

What people say. Recommended as a practical case study of adopting formal methods and safe languages in production firmware.

tnballoon Hacker News • Recommends

On “High Assurance Rust: Developing Secure and Robust Software”

Author of the book here, thank you for your feedback! Though not an Ada expert, I have used the SPARK subset. And I’ve worked on security assessment of military systems with components written in Ada. Although we looked at binaries and not source code, because our assurance model did not consider the Ada compiler to be part of the chain of trust (so we test the artifact the CPU will execute). I really like Ada and hope to use more of it in the future! The HN community may be interested in this 1 hour presentation 1 on Nvidia's adoption of Ada, including why they chose it over Rust in 2019 (regulatory certification was one factor). There’s also a great academic paper 2 on the recent advan…
View on Hacker News

kevlar700on Hacker News • Mentions

On “Is it time to retire C and C++ for Rust in new programs?”

Ada offers security and simplicity and is already part of GCC but also has llvm now. Linux kernel drivers have also been demonstrated. Perhaps it would be healthier for Rust to have competition? link link link Nvidia also chose Spark; a built in subset of Ada as being more cost effective for secure code than C++. link to this video Assembly is also supported by Ada and I found it far easier to add than with C even. C interface support is also excellent.
View on Hacker News

kevlar700on Hacker News • Mentions

On “Is it time to retire C and C++ for Rust in new programs?”

Ada offers security and simplicity and is already part of GCC but also has llvm now. Linux kernel drivers have also been demonstrated. Perhaps it would be healthier for Rust to have competition? link link link Nvidia also chose Spark; a built in subset of Ada as being more cost effective for secure code than C++. link to this video Assembly is also supported by Ada and I found it far easier to add than with C even. C interface support is also excellent.
View on Hacker News

kevlar700on Hacker News • Mentions

On “It's time to halt starting any new projects in C/C++”

Ada offers security and simplicity and is already part of GCC but also has llvm now. Linux kernel drivers have also been demonstrated. Perhaps it would be healthier for Rust to have competition? link link link Nvidia also chose Spark; a built in subset of Ada as being more cost effective for secure code than C++. link to this video Assembly is also supported by Ada and I found it far easier to add than with C even. C interface support is also excellent.
View on Hacker News

adezxcon Hacker News • Mentions

On “Ada Continues to Climb in June Tiobe Index and PYPL”

There's this talk by AdaCore and a SWE@nVidia on how nVidia utilized Ada/Spark for Embedded software: link to this video
View on Hacker News

cpetersoon Hacker News • Mentions

On “Introduction to Ada: a project-based exploration with rosettas”

Here’s a related talk: “NVIDIA - Securing the Future of Safety and Security of Embedded Software” link to this video > NVIDIA is working with AdaCore to implement Ada and SPARK programming languages into certain firmware elements to reduce this potential error. In this webinar you will learn how the combination of NVIDIA hardware with Ada and SPARK delivers robustness and security, improving efficiency and safety in the development pipeline.
View on Hacker News

cpetersoon Hacker News • Mentions

On “CUDA-oxide: Nvidia's official Rust to CUDA compiler”

Here's a recording of a 2020 presentation ("Securing the Future of Safety and Security of Embedded Software") from NVIDIA at the AdaCore conference: link to this video
View on Hacker News