NVIDIA setzt auf formale Verifikation mit SPARK: verbesserte Sicherheit, ohne Performance-Einbußen

Angesichts zunehmender Cyberbedrohungen hat das Sicherheitsteam von NVIDIA traditionelle Tests aufgegeben und die formale Verifikation mit SPARK eingeführt. Ein Proof-of-Concept-Projekt hat in nur drei Monaten erfolgreich sicherheitskritischen C-Code in SPARK umgewandelt und eine verbesserte Sicherheit ohne Performance-Einbußen gezeigt. Mittlerweile sind über fünfzig NVIDIA-Entwickler in SPARK geschult, und zahlreiche Produkte werden mit SPARK-Komponenten ausgeliefert. Diese Fallstudie unterstreicht die erfolgreiche Einführung der formalen Verifikation und bietet wertvolle Lehren für andere Organisationen, die ihre Sicherheit verbessern möchten.