Die Programmiersprachen Ada und SPARK von AdaCore helfen, die Kosten für die Entwicklung und Verifizierung sicherheitskritischer Software zu reduzieren.
AdaCore, ein führender Anbieter von Softwareentwicklungs- und Verifikationstools, arbeitet ab sofort mit NVIDIA bei der Nutzung der Programmiersprachen Ada und SPARK für die Implementierung ausgewählter sicherheitskritischer Firmware zusammen. Diese wird in Anwendungen eingesetzt, die strenge Safety- und Security-Funktionen erfordern, beispielsweise beim automatisierten und autonomen Fahren.
Einige System-on-a-Chip-Produkte von NVIDIA werden auf eine neue RISC-V Instruction Set Architecture (ISA) umgestellt. Darüber hinaus plant NVIDIA eine Aktualisierung ausgewählter sicherheitskritischer Firmware und wechselt dabei von C auf Ada und SPARK. Beide Schritte zielen darauf ab, die Verifikationseffizienz zu erhöhen und die ISO-26262-Norm für funktionale Sicherheit einzuhalten.
„Die Entscheidung von NVIDIA für Ada und SPARK leitet eine neue Ära in der Geschichte der sicherheitskritischen Softwareentwicklung ein“, sagt Quentin Ochem, Lead of Business Development bei AdaCore. „Wir sind stolz darauf, einen Beitrag zu den Industriestandards eines Marktführers zu leisten.“
Zwei Programmiersprachen für höchste Sicherheitsanforderungen
Ada und SPARK wurden entwickelt, um die strengsten Softwareanforderungen für Safety und Security zu erfüllen. Die Programmiersprache Ada verfügt über zahlreiche integrierte Funktionen, die frühzeitig Codefehler im Software-Lebenszyklus erkennen und so den Aufwand für Peer Review und Tests verringern. Die SPARK-Sprache – eine Variante von Ada, die die Durchführung eines formalen mathematischen Beweises ermöglicht – erhöht die Sicherheit, Fehler rechtzeitig zu erkennen, die sonst vielleicht nicht erkannt worden wären. SPARK vereinfacht die statische Analyse, die formal bestimmte Eigenschaften des Codes nachweisen kann, angefangen von der korrekten Verwendung von Daten und dem Ausschluss von Laufzeitfehlern wie Pufferüberläufen bis hin zu komplexeren Eigenschaften wie der Erfüllung funktionaler Anforderungen.
„Selbstfahrende Autos sind extrem komplex und erfordern eine ausgereifte Software, die die strengsten Standards erfüllt“, erläutert Daniel Rohrer, Vice President of Software Security bei NVIDIA. „Maßnahmen wie die Integration der Ada- und SPARK-Sprachen in NVIDIA-Plattformen können die Robustheit und Verlässlichkeit unserer Fahrzeugsicherheit verbessern.“
