Le code source de KSOS, précurseur sécurisé d’Unix soutenu par le DoD, ajouté à une archive publique

Le code source de KSOS, un ancien système d’exploitation de type Unix axé sur la sécurité et financé par le département de la Défense des États-Unis à la fin des années 1970 et dans les années 1980, a été rendu public pour la première fois par l’intermédiaire des archives de The Unix Heritage Society (TUHS).

Warren Toomey, fondateur de TUHS, a annoncé cet ajout sur la liste de diffusion du groupe. TUHS est surtout connue pour préserver le code source et la documentation historiques d’Unix, et cette publication de KSOS élargit cet effort avec un logiciel qui a contribué à façonner les concepts ultérieurs de systèmes d’exploitation sécurisés.

KSOS, abréviation de Kernelized Secure Operating System, a été conçu pour fournir un environnement dont la sécurité pouvait être prouvée sur de grands mini-ordinateurs. Contrairement à de nombreux descendants d’Unix écrits en C, KSOS a été développé en Modula, un langage à typage sûr associé à Niklaus Wirth. Ses développeurs visaient une vérification formelle, c’est-à-dire que le système devait être analysé mathématiquement et considéré comme fiable pour des usages nécessitant un haut niveau de sécurité.

En avance sur son temps

Le projet a débuté en 1978 chez Ford Aerospace, puis s’est poursuivi chez Logicon. Parmi les personnes impliquées figuraient le chercheur en sécurité Peter Neumann et l’ingénieur Tom Perrine, qui ont par la suite documenté le système et l’ont présenté dans des conférences et des articles. Bien que KSOS s’inspire des concepts d’Unix et offre une compatibilité avec les appels système Unix en mode superviseur, il ne partageait aucun code du noyau Unix.

KSOS n’était pas qu’un prototype de recherche. Selon des récits historiques, il a été déployé en production pour des systèmes de renseignement sécurisés à plusieurs niveaux, notamment dans des environnements de déclassement de niveau de sécurité approuvés et utilisés par des agences gouvernementales. Il disposait également d’une version pour VAX, connue sous le nom de KSOS-32, tandis que la version antérieure pour PDP-11 a ensuite été appelée KSOS-11.

• Écrit en Modula plutôt qu’en C
• Conçu pour la vérification formelle et une isolation renforcée
• Utilisé sur du matériel courant
• Compilé sous Unix plutôt que compilé sur lui-même

La publication a été rendue possible après que Perrine a fourni une ancienne archive tar du code source, conservée par son collègue développeur Jeff Makey, avec l’aide de John O Goyo et de Thalia Archibald pour l’intégrer aux archives de TUHS. Une énigme historique subsiste : le compilateur d’origine utilisé pour compiler le système n’a pas encore été identifié.

Cette récupération ajoute un nouvel artefact notable à la collection de TUHS consacrée aux débuts de l’histoire des systèmes d’exploitation. Elle montre que les préoccupations liées à la conception sécurisée et à la sûreté du typage étaient étudiées des décennies avant que des langages modernes tels que Rust ne remettent ces idées au premier plan.