Startseite > Medizintechnik > E-Health > Von der Vision zur Wirklichkeit

Fehlerfreie Medizinsoftware

Von der Vision zur Wirklichkeit

15. April 2019, 16:33 Uhr | Daniel Kästner (Absint)

▶ Diesen Artikel anhören

Fortsetzung des Artikels von Teil 2

Nachweis der Echtzeitfähigkeit

Viele Tasks in sicherheitskritischen eingebetteten Systemen haben harte Echtzeitanforderungen. Das heißt, die Einhaltung ihrer Deadlines ist zum korrekten Funktionieren des Systems erforderlich. Statische Analysatoren auf Basis der Abstrakten Interpretation können garantierte und präzise obere Schranken der maximalen Ausführungszeit berücksichtigen [31, 32]. Sie sind für komplexe Prozessoren mit Caches, komplexen Pipelines, Single-Core und Multi-Core Prozessoren verfügbar. Eine Voraussetzung ist jedoch, dass das Zeitverhalten des Prozessors deterministisch vorhersagbar ist. Dies ist bei der jüngsten Generation ursprünglich für den Consumer-Bereich entwickelter High-Performance Multicore System-On-Chips oft nicht mehr erfüllt. Der Hauptgrund liegt in Interferenzen zwischen den einzelnen Cores der betroffenen Multicore-Architekturen, die sich nicht vermeiden oder begrenzen lassen [33]. Hier bieten sich hybride WCET-Analysatoren an, die auf Basis nicht-invasiver Echtzeit-Traces das Zeitverhalten der ausführbaren Codestücke unter Berücksichtigung typischer Interferenzen messen und daraus einen kritischen Ausführungspfad konstruieren [34, 35].

Ausschluss von Laufzeitfehlern

Eine weitere Klasse kritischer Fehler sind Programmierfehler aufgrund undefinierten oder nicht spezifizierten Verhaltens der eingesetzten Programmiersprache, die sogenannten Laufzeitfehler. Hierzu zählen arithmetische Überläufe, Feldgrenzenverletzungen, Pufferüberläufe, aber auch Datenwettläufe oder Deadlocks. Solche Fehler können die Datenintegrität zerstören, falsche Systemreaktionen verursachen und zu einem Softwareabsturz führen. Sie sind gleichzeitig die kritischsten Einfalltore für Cybersecurity-Attacken auf Code-Ebene [36]. Ein Beispiel für einen statischen Laufzeitfehler-Analysator auf Basis der Abstrakten Interpretation ist das Tool Astrée [37], das alle potentiellen Laufzeitfehler in C-Programmen entdeckt und damit den sicheren Nachweis der Abwesenheit solcher Fehler ermöglicht. Astrée verfügt über eine leistungsstarke Analysekern, die eine hohe Analysepräzision erreicht, aber dennoch für komplexe Industrieanwendungen skaliert. Beispielsweise konnte eine vollständige kommerzielle Flugzeugsteuerung von über 500.000 Zeilen Code ohne jeden Fehlalarm analysiert werden [38]; das bislang größte analysierte Programm besteht aus 110 Millionen Zeilen präprozessierten Codes, für die knapp 2 Tage Analysezeit erforderlich waren [39].

Compiler-Fehler

Stacküberläufe und Laufzeitfehler sind zwei Hauptursachen software-verursachter Speicherkorruption. Die dritte Hauptursache sind Compiler-Fehler: Der Compiler erzeugt fehlerhaften Code für ein korrektes Eingabeprogramm. Durch Einsatz eines formal bewiesenen Compilers kann Fehlcompilierung ausgeschlossen werden; somit können alle drei Hauptursachen software-verursachter Speicherkorruption eliminiert werden [40, 41].

Zusammenfassung

Sicherheitsorientierte Codierrichtlinien ermöglichen einen auf Minimierung von Programmierfehlern ausgerichteten Programmierstil. Funktionale Korrektheit kann durch formale Verifikationsverfahren bewiesen oder durch automatisierte Testverfahren geprüft werden. Die Abwesenheit von sicherheitskritischen nicht-funktionalen Fehlern, darunter Stacküberläufe, Zeitüberschreitungen, Laufzeitfehler und Datenwettläufe, kann durch statische Analysatoren auf Basis der Abstrakten Interpretation bewiesen werden. Formal verifizierte Compiler stehen zur Verfügung, bei denen mathematische Beweise vorliegen, dass es keine Fehlcompilierung geben kann. Den Entwicklern steht somit ein mächtiger Baukasten von Software-Werkzeugen zur Verfügung, die einen hohen Zuverlässigkeitsgrad sicherheitskritischer Software ermöglichen.