Funktionale Sicherheit
Statische Analysen schützen Patienten
Aktuelle Sicherheitsstandards für die Medizintechnik fordern den Nachweis, dass die funktionalen Software-Anforderungen erfüllt werden und dass bestimmte schwerwiegende Softwarefehler niemals auftreten können. Hierzu zählen Timing-Fehler, Stacküberläufe und Laufzeitfehler. Statische Analysen auf Basis der abstrakten Interpretation können beweisen, dass der Code frei von solchen Fehlern ist.
Sicherheitskritische Funktionen werden in eingebetteten Systemen immer mehr durch Software realisiert. Dieser Trend ist nicht nur in der Luftfahrt- und Automobilindustrie, sondern zunehmend auch im Bereich der Medizintechnik zu beobachten. Eine Fehlfunktion der Steuerungssoftware kann im Extremfall Menschenleben gefährden, aber auch in weniger kritischen Systemen hohe Kosten verursachen - nicht zuletzt durch Rückrufaktionen. Innerhalb der letzten fünf Jahre gingen bei der US-amerikanischen FDA (Food and Drug Administration) beispielsweise 56 000 Berichte von schwerwiegenden Ereignissen im Zusammenhang mit Infusionspumpen ein.
Nach Aussage der FDA wurden mehr als 500 Tote registriert und 87 Rückrufe von Infusionspumpen zwischen 2005 und 2009 aus Sicherheitsgründen durchgeführt. Die Behörde hat diese schwerwiegenden Ereignisse analysiert und Softwarefehler als eine der Hauptursachen identifiziert. Dies unterstreicht die zentrale Bedeutung der Software-Validierung: Ihr Ziel ist ein objektiver Nachweis, dass die relevanten Anforderungen an die Software erfüllt worden sind und keine Sicherheitsverletzungen auftreten können.
Bei Medizinprodukten ist in Deutschland der Nachweis der Übereinstimmung mit dem Medizinproduktegesetz (MPG) erforderlich. Darüber hinaus sind verschiedene Normen zu berücksichtigen. So definiert die DIN EN 60601-1-4 Anforderungen an den Lebenszyklus und das Risikomanagement von Medizinprodukte-Software. DIN EN 62304 beschreibt die Implementierung eines Entwicklungs-Lebenszyklus für Software mit besonderem Fokus auf Software-Wartungsprozesse und komponentenorientierte Softwarearchitekturen.
Von zentraler Bedeutung für die Software-Validierung ist die EG-Richtlinie 2007/47/EG, die mit dem vierten MPG-Novellierungsgesetz vom 21.3.2010 in deutsches Recht umgesetzt wurde. Sie besagt, dass auch »Software als solche« ein eigenständiges Medizinprodukt darstellt, wenn sie für einen medizinischen Zweck bestimmt ist. Software als integraler Bestandteil eines Medizinprodukts, beispielsweise Software zur Steuerung und Überwachung eines aktiven Medizinprodukts, zum Beispiel einer Infusionspumpe, eines Beatmungs- oder eines Durchleuchtungsgeräts, unterliegt grundsätzlich dem Medizinprodukterecht.
Die Richtlinie 2007/47/EG fordert in Absatz (20) explizit, Software für Medizinprodukte - entweder als eigenständiges Element oder als Bestandteil eines Medizinproduktes - in Übereinstimmung mit dem Stand der Technik zu validieren. Aktuelle Sicherheitsstandards aus dem Luftfahrt- oder Automobilbereich wie DO-178B und ISO 26262 geben konkretere Ziele vor und fordern die Identifikation funktionaler und nicht-funktionaler Gefahrenstellen sowie den Nachweis, dass die Software die relevanten Sicherheitsziele erfüllt.
Zum Korrektheitsnachweis für funktionale Programmeigenschaften haben sich automatische und modellbasierte Testverfahren neben formalen Methoden wie »Model Checking« etabliert. Bei der Systemkorrektheit spielen jedoch auch nicht-funktionale Eigenschaften eine wichtige Rolle: So darf das Programm unter anderem nicht wegen Speicherfehlern abstürzen, und die Reaktionen von Steuerungssoftware müssen oft innerhalb einer vorgegebenen Zeit erfolgen.
Die Folgen nicht-funktionaler Fehler können schwerwiegend sein - wie die Explosion der Ariane 5 im Jahr 1996 als Beispiel aus dem Luftfahrtbereich zeigt. Die Überprüfung nicht-funktionaler Programmeigenschaften durch Testverfahren ist problematisch. Tests und Messungen können prinzipiell nicht die Abwesenheit von Fehlern beweisen. Erschwerend kommt hinzu, dass keine spezifischen Testfälle zum Beispiel zur Stimulation der längstmöglichen Laufzeit oder des maximalen Stackverbrauchs zur Verfügung stehen.
Auch die Bestimmung sinnvoller Kriterien, wann ein Test von Eigenschaften wie Timing, Stackverbrauch oder dem Auftreten von Laufzeitfehlern (z.B. Division durch Null oder arithmetische Überläufe) tatsächlich beendet ist, stellt ein ungelöstes Problem dar. Der Testprozesss ist somit prinzipell unfokussiert, der erforderliche Testaufwand hoch und die Testabdeckung unvollständig.
In den letzten Jahren haben sich statische Analysatoren auf Basis der »abstrakten Interpretation« zum Stand der Technik bei der Verifikation nicht-funktionaler Eigenschaften entwickelt. Der Begriff »statischer Analysator« ist dabei weit gefasst: Im weitesten Sinne bezeichnet er ein Softwarewerkzeug, das zur Ermittlung der Analyseergebnisse keine Ausführung des zu untersuchenden Programmes benötigt.
Die sogenannten sicheren statischen Analysatoren, die auf der Theorie der abstrakten Interpretation basieren, zählen zu den formalen Verifikationsmethoden. Die abstrakte Interpretation ist eine semantikbasierte Methodik für Programmanalysen. Mit ihr lassen sich Aussagen beweisen, die für alle möglichen Programmausführungen und alle möglichen Eingabeszenarien gelten. So erzielt dieser Ansatz eine vollständige Abdeckung und reduziert gleichzeitig den Testaufwand. Statische Analysen erfordern keinen Zugriff auf die physikalische Zielhardware, sie lassen sich in den Entwicklungsprozess integrieren - beispielsweise durch Kopplung mit modellbasierten Code-Erzeugern -, und sie ermöglichen dem Entwickler, Fehler in frühen Entwicklungsphasen zu entdecken. Moderne statische Analysatoren skalieren gut und erlauben die Analyse vollständiger sicherheitskritischer Industrieanwendungen.
Längste Ausführungszeit finden
Beispiele für statische Analysatoren auf Basis der abstrakten Interpretation sind Softwarewerkzeuge für den Nachweis der längstmöglichen Ausführungszeit und des maximalen Stackverbrauchs von Tasks sowie für den Ausschluss des Auftretens von Laufzeitfehlern. Stacküberläufe können schwerwiegende Fehler verursachen, die zu fehlerhaften Programmausführungen oder zu Abstürzen führen können. Außerdem haben sie das Potenzial, die Datenintegrität zu zerstören und damit unerwünschte Interferenzen zwischen Softwarekomponenten zu verursachen.
Wenn Stacküberläufe auftreten, sind sie oft schwierig zu diagnostizieren und zu reproduzieren. Das Tool »StackAnalyzer« von AbsInt berechnet, wie die Stackhöhe entlang der verschiedenen Kontrollpfade zu- und abnimmt. Mit dieser Information lässt sich der maximale Stackverbrauch einer Task berechnen und damit die Abwesenheit von Stacküberläufen beweisen.
Viele Tasks in sicherheitskritischen eingebetteten Systemen haben harte Echtzeitanforderungen. Für die korrekte Funktion des Systems ist es also erforderlich, die Deadlines dieser Anforderungen einzuhalten. Aufgrund von Architektureigenschaften moderner Hardware und moderner Software stellt die Bestimmung der längstmöglichen Ausführungszeit (Worst Case Execution Time, WCET) ein schwieriges Problem dar.
Der WCET-Analysator »aiT« ist ein statischer Analysator auf Basis der abstrakten Interpretation, der eine sichere Approximation aller möglichen Cache- und Pipeline-Zustände für alle Programmpunkte und jede beliebige Eingabe berechnet. Aus den Ergebnissen lässt sich mit ganzzahliger Programmierung ein längster Pfad bestimmen, der gleichzeitig eine garantierte obere Schranke der längstmöglichen Ausführungszeit liefert (Bild 1).
aiT und StackAnalyzer arbeiten auf vollständig gelinkten ausführbaren Binärdateien und erfordern weder Codemodifikation noch Debuginformation. Die berechneten Schranken sind präzise und gelten für jede mögliche Programmausführung und jedes mögliche Eingabeszenario. Eine weitere Klasse kritischer Fehler sind die so genannten Laufzeitfehler. Beispiele dafür sind arithmetische Überläufe, Feldgrenzenverletzungen oder ungültige Zeigerzugriffe. Sie können die Datenintegrität zerstören, völlig falsche Systemreaktionen verursachen und zu einem Softwareabsturz führen.
So kam es beispielsweise aufgrund eines arithmetischen Überlaufs zu einem schweren Funktionsfehler des Bestrahlungsgeräts »Therac-25« von AECL Medical, der von Juni 1985 bis 1987 drei Patienten das Leben kostete und drei weitere schwer verletzte. Das Analysetool »Astrée« entdeckt alle potenziellen Laufzeitfehler in C-Programmen (Bild 2) und ermöglicht damit den sicheren Nachweis der Abwesenheit solcher Fehler.
Es verfügt über eine leistungsstarke Analyse-Engine und erlaubt es, die Präzision der Analyse genau an das zu analysierende Programm anzupassen. Dies ermöglicht eine sehr niedrige Fehlalarmrate: Sicherheitskritische Avionik-Software im Umfang von über 500 000 Zeilen C-Code konnte durch Astrée mit null Fehlalarmen analysiert werden.
Abstrakte Interpretation ist als formale Verifikationsmethode anerkannt und liefert sichere Ergebnisse. Statische Analysatoren auf Basis der abstrakten Interpretation lassen sich zur Zertifizierung nach allen Sicherheitsstandards einsetzen. Für die Analysewerkzeuge aiT, StackAnalyzer und Astrée stehen zudem »Qualification Support Kits« zur Verfügung. Diese dienen dem Nachweis, dass das Tool im operationalen Kontext des Benutzers korrekt funktioniert und ermöglichen eine automatische Tool-Qualifizierung bis zu den höchsten Sicherheitsstufen.
Über den Autor:
Dr. Daniel Kästner ist technischer Direktor (CTO) bei AbsInt.
Lesen Sie mehr zum Thema
Das könnte Sie auch interessieren
