Tool-basierte statische Codeanalyse hat sich als Standardverfahren der Softwareentwicklung etabliert. Sie ermöglicht einen hocheffizienten Entwicklungsprozess durch automatische Prüfung des Codes nach einer Vielzahl von Kriterien. Hierzu zählen nicht nur die Prüfung von Codierrichtlinien, sondern auch tiefgehende semantische Analysen.

Aufgrund der Implementierungskomplexität stellt der Einsatz statischer Analysen auf Betriebssystemcode besondere Herausforderungen. PikeOS ist ein Echtzeitbetriebssystem, das in hochsicherheitskritischen Anwendungen eingesetzt wird. Aufgrund zunehmender Kommunikationsanforderungen spielen Security-Anforderungen eine immer größere Rolle. Um diesen Anforderungen zu genügen, wurde ein massgenschneiderter Satz von Codierrichtlinien auf Basis von MISRA C:2012, CERT-C und CWE entwickelt. Darüber hinaus wurde ein Konzept zur sicheren statischen Analyse der Betriebsystemschicht unter Verwendung des statischen Analysators Astrée entwickelt, mit dem die Abwesenheit von Laufzeitfehlern in kritischen Betriebssystemfunktionen sichergestellt werden kann. Mit Hilfe der Taint-Analyse von Astrée wurde zudem eine Erkennungs von Spectre-Verwundbarkeiten realisiert, die Vorkommen von Spectre v1, Spectre v1.1 und SplitSpectre-Verwundbarkeiten im Code meldet. Auf ähnliche Weise können auch funktionale Security-Anforderungen geprüft werden und Datenkorruptionsanalysen durchgeführt werden. Im Vortrag warden alle genannten Punkte vorstellt und experimentell belegt.

Was lernen die Zuhörer in dem Vortrag?

• Safety- und Security-Anforderungen an moderne Echtzeitbetriebssysteme
• Überblick über aktuelle Codierrichtlinien, insbesondere MISRA C:2012, CERT-C, CWE
• Vorgehensweise und Kriterien zum Tailoring der Codierrichtlinien-Standards an eignene Anforderungen
• Funktionsweise sicherer statischer Analyse und Anwendung auf Betriebssystemcode
• Funktionsweise von Taint-Analyse
• Funktionsweise von SPECTRE und entsprechender Code-Verwundbarkeiten
• Statische Analyse zur Erkennung von SPECTRE-Verwundbarkeiten