Hintergrund und Inhalt

Anwendung von formaler Programmverifikation für IT-Sicherheit bei Betriebssystemen in der Praxis

Systeme und Geräte mit eingebetteten IT-Funktionen sind höchstens so sicher wie das Betriebssystem (BS), das als zentrale Basis aufbauend auf der Hardware verwendet wird. Der BS-Kern läuft im freizügigsten Modus der Hardware, wenn er kompromittiert wird, kann das Verhalten aller Hard- und Software-Komponenten im System modifiziert werden. Programmierfehler können direkt zu unerwünschtem Verhalten führen oder sie bilden ein Einfallstor für Angriffe. Die wirksamste Maßnahme gegen Fehler ist ein formaler Beweis der Fehlerfreiheit. Allerdings sind solche Beweise bisher nur für Programme durchführbar, die deutlich kleiner als praktisch verwendete BS-Kerne sind.

Mikrokerne

Die Antwort darauf sind Mikrokerne mit stark reduziertem Funktionsumfang, die klein genug für formale Verifikation sind. Die wichtigste verbleibende Funktionalität ist die strikte Separierung der übrigen Software-Komponenten untereinander, vom Mikrokern und von der Hardware. Mit solchen weiteren Komponenten können dann die übrigen BS-Funktionen implementiert werden. Zusammen mit dem Mikrokern ergeben sie ein vollständiges Betriebssystem.

Der seL4 Mikrokern wurde bereits erfolgreich formal verifiziert. Seine Architektur erlaubt die Entwicklung von Betriebssystemen, die ähnlich performant sind wie die existierenden monolithischen BS-Kerne. Das durch HENSOLDT Cyber entwickelte BS TRENTOS ist in dieser Weise aufgebaut. Das Ziel des HoBIT-Projekts waren Methoden und Werkzeuge, mit denen sich mittels formaler Verifikation ähnliche Sicherheitseigenschaften für das Betriebssystem erreichen lassen wie für den Mikrokern selbst.

Die strikte Trennung der übrigen Komponenten hat zur Folge, dass sich die Kompromittierung einer Komponente nicht auf andere Teile des Systems auswirken kann. Eine kompromittierte Komponente kann aber immer noch ein hohes Sicherheitsrisiko für Systeme in einer kritischen Umgebung darstellen. Ein kompromittierter Netzwerk-Treiber kann beispielsweise wichtige Kommunikationskanäle blockieren oder vertrauliche Daten in andere Kanäle umleiten. Daher ist es notwendig, formale Verifikation zumindest auf einen Teil der weiteren BS-Komponenten anzuwenden.

Verifikation von BS-Komponenten für die Praxis

Formale Verifikation funktioniert am besten, wenn ein Programm von vornherein für dieses Ziel entwickelt wird, möglichst in einer dafür geeigneten höheren Programmiersprache. Im HoBIT-Projekt untersuchten wir die von Data61 entwickelte funktionale Programmiersprache Cogent. Neben der Übersetzung von abstrakter Hochsprachen-Ebene in ausführbaren Code wird hier ein "Refinement"-Beweis dafür generiert, dass sich das Ergebnis wie erwartet verhält.

In der Praxis werden BS-Komponenten aber meist in C programmiert, einer maschinennahen Programmiersprache und ein Alptraum für formale Verifikation. Dies betrifft auch noch neu entwickelte Komponenten, da den hoch spezialisierten Entwicklern C meist am vertrautesten ist. Unser Ansatz in HoBIT war es daher, für die formale Verifikation von C-Code das Unterstützungs-Werkzeug Gencot zu entwickeln, das halbautomatisch C nach Cogent übersetzt. Sein Ziel ist die Unterstützung von C-Programmierern bei der Überführung von C-Programmen nach Cogent, um so eine formale Verifikation zu ermöglichen. Als Demonstration wurde es erfolgreich verwendet, um für in C implementierte TRENTOS-Komponenten alternative Cogent-Implementierungen zu erzeugen. Gencot ist open Source und verfügbar auf GitHub.