Quellcode des vom US-Verteidigungsministerium unterstützten sicheren Unix-Vorläufers KSOS in öffentlichem Archiv veröffentlicht

Der Quellcode von KSOS, einem frühen sicherheitsorientierten Unix-ähnlichen Betriebssystem, das Ende der 1970er- und in den 1980er-Jahren vom US-Verteidigungsministerium finanziert wurde, ist erstmals über das Archiv der Unix Heritage Society (TUHS) öffentlich zugänglich gemacht worden.

Warren Toomey, der Gründer von TUHS, gab die Aufnahme in die Mailingliste der Gruppe bekannt. TUHS ist vor allem für die Bewahrung historischer Unix-Quellcodes und -Dokumentationen bekannt. Die Veröffentlichung von KSOS erweitert diese Arbeit um eine Software, die zur Entwicklung späterer Konzepte für sichere Betriebssysteme beitrug.

KSOS steht für „Kernelized Secure Operating System“ und wurde entwickelt, um eine nachweislich sichere Umgebung für größere Minicomputer bereitzustellen. Im Gegensatz zu vielen Unix-Abkömmlingen, die in C geschrieben wurden, entstand KSOS in Modula, einer typsicheren Sprache, die mit Niklaus Wirth verbunden ist. Die Entwickler strebten eine formale Verifikation an. Das System sollte also mathematisch analysiert und für den Einsatz in Hochsicherheitsumgebungen vertrauenswürdig gemacht werden.

Seiner Zeit voraus

Das Projekt begann 1978 bei Ford Aerospace und wurde später bei Logicon fortgeführt. Zu den Beteiligten gehörten der Sicherheitsforscher Peter Neumann und der Ingenieur Tom Perrine, die das System später dokumentierten und in Vorträgen und Artikeln erörterten. Obwohl sich KSOS an Unix-Konzepten orientierte und im Supervisormodus Kompatibilität mit Unix-Systemaufrufen bot, enthielt es keinen Unix-Kernelcode.

KSOS war nicht nur ein Forschungsprototyp. Historischen Berichten zufolge wurde es in sicheren, mehrstufigen Nachrichtendienstsystemen produktiv eingesetzt, darunter in vertrauenswürdigen Umgebungen zur Herabstufung von Informationen, die von Regierungsbehörden genutzt wurden. Außerdem gab es eine VAX-Version namens KSOS-32, während die frühere PDP-11-Version später als KSOS-11 bezeichnet wurde.

• In Modula statt in C geschrieben
• Für formale Verifikation und starke Isolation entwickelt
• Auf handelsüblicher Hardware eingesetzt
• Unter Unix kompiliert, statt sich selbst zu hosten

Die Veröffentlichung wurde möglich, nachdem Perrine ein altes Quellcode-Tarball bereitgestellt hatte, das von seinem Entwicklerkollegen Jeff Makey aufbewahrt worden war. John O Goyo und Thalia Archibald halfen dabei, es in das TUHS-Archiv aufzunehmen. Ein historisches Rätsel bleibt jedoch ungelöst: Der ursprüngliche Compiler, mit dem das System erstellt wurde, konnte bislang nicht identifiziert werden.

Die Wiederentdeckung fügt der Sammlung von TUHS zur Geschichte früher Betriebssysteme ein weiteres bemerkenswertes Artefakt hinzu. Sie zeigt, dass Fragen zu sicherem Design und Typsicherheit bereits Jahrzehnte untersucht wurden, bevor moderne Sprachen wie Rust diese Konzepte wieder in den Mainstream brachten.