EDF bewertet die Softwaresicherheit eines Kernkraftwerks mit formalen Methoden mithilfe von Polyspace
Diese Vorgehensweise sorgt für die Einhaltung internationaler Standards und minimiert gleichzeitig softwarebezogene Risiken
„Die Polyspace-Analyse schafft Vertrauen, da sie einen starken, verlässlichen Nachweis darüber liefert, dass der Code frei von Laufzeitproblemen ist. Außerdem half sie uns bei der Sicherheitsbegründung für unseren vorhandenen Kraftwerkpark, wo veraltete Hardware-Instrumente durch softwarebasierte ersetzt werden mussten. Unser Einsatz von Polyspace-Tools untermauert eine Verringerung eigenverantwortlicher Testdurchführungen. Beispielsweise kann in Polyspace Bug Finder die Software-Fehlerresistenz mithilfe strengerer Überprüfungen gezeigt und mit Polyspace Code Prover belegt werden, sodass das Testen auf die funktionalen Eigenschaften der Software konzentriert werden kann.“
Wichtigste Ergebnisse
- Polyspace-Tools trugen dazu bei, die Abwesenheit von Laufzeitfehlern und Schwachstellen in Zulieferer-Software zu belegen
- Mit Polyspace Code Prover und Polyspace Bug Finder konnte EDF die strengen Qualifizierungsvorgaben der Kernindustrie einhalten
- Mit Polyspace-Tools konnte eine Fehlerdichte von nur 0,07 Fehlern pro 1000 Codezeilen belegt werden
EDF verwendet Polyspace-Produkte, um die strengen Qualifizierungsvorgaben an die Kernenergie einzuhalten, die auf unabhängige Weise das Vertrauen in sicherheitskritischen Code aufbauen.
EDF ist der größte britische Anbieter kohlenstofffreier Energie. Zur Sicherstellung einer einheitlichen Softwarequalität in seiner neuesten Generation von Kernkraftwerken verwendet EDF Polyspace®-Tools. Auf diese Weise kann die Softwaresicherheit von zugeliefertem Programmcode unabhängig bewertet werden.
Die Betreiber britischer Kernkraftwerke für den Zivilbedarf müssen strenge Qualifizierungsvorgaben einhalten, um zu belegen, dass softwarebezogene Risiken im Sicherheitssystem minimiert werden. Das Durchsetzen von Programmierregeln und die statische Codeanalyse auf Basis formaler Methoden, um die Abwesenheit bestimmter Arten von Fehlern und Schwachstellen zu belegen, liefern stabile Nachweise, dass dieses Ziel erreicht wird.
Die Qualifizierungsvorgaben beruhen auf zwei unabhängigen Säulen gemäß NS-TAST-GD-046: Produktionskompetenz (Production Excellence, PE) und unabhängige vertrauensbildende Maßnahmen (Independent Confidence Building Measures, ICBM). PE erfordert, dass die Software relevanten internationalen Standards wie IEC 61508, IEC 62138 und IEC 60880 genügt, während ICBM aus zusätzlich durchgeführten Tests und Analysen besteht, die ganz unabhängig vom Zulieferer durchgeführt werden. Während die statische Codeanalyse im Rahmen der ICBM für die Sicherheitsklasse 2 erwartet wird, ist sie für ICBM der Sicherheitsklasse 1 verpflichtend. Darüber hinaus liefert der Einsatz formaler Methoden zum Beweis der Abwesenheit von Laufzeitfehlern und Schwachstellen einen starken Nachweis dafür, dass die Risiken aus der Software in ihren Sicherheitssystemen verringert wurden.
Im Rahmen von PE nutzt EDF Polyspace-Produkte, um auf Schwachstellen zu prüfen und die MISRA™-Programmierkonformität durchzusetzen. Hinsichtlich ICBM wird Polyspace Bug Finder™ in der Regel bei Anwendungen der Klasse 2 verwendet, um Schutz- und Sicherheitsschwachstellen zu entdecken, die dann von Analysten untersucht werden, um ihre Auswirkungen auf die Systemsicherheit festzustellen. Bei Anwendungen der Klasse 1 kommt zusätzlich Polyspace Code Prover™ zum Einsatz, um die Abwesenheit von Laufzeitfehlern zu belegen.
Mithilfe dieser Überprüfungen kann EDF nachweisen, dass bestimmte Laufzeitfehler minimiert werden. Das ergibt eine solide Grundlage für die Genehmigung und stellt die Kompetenz in der gesamten Lieferkette sicher. In einem kürzlich durchgeführten Projekt zeigte das EDF-Team eine äußerst geringe Fehlerdichte von 0,07 pro 1000 Codezeilen. Angesichts dieser Vorteile tragen Polyspace-Werkzeuge auch zur Sicherheitslegitimierung des bestehenden EDF-Kraftwerkparks bei. Sie unterstützen geplante Instrumentenstilllegungen, wo hardwarebasierte Instrumente nicht mehr verfügbar sind und ihre softwarebasierten Ersetzungen begründet werden müssen.
