Il codice sorgente del precursore Unix sicuro KSOS, sostenuto dal DoD, aggiunto a un archivio pubblico

Il codice sorgente di KSOS, uno dei primi sistemi operativi simili a Unix incentrati sulla sicurezza, finanziato dal Dipartimento della Difesa degli Stati Uniti tra la fine degli anni ’70 e gli anni ’80, è stato reso pubblico per la prima volta attraverso l’archivio di The Unix Heritage Society (TUHS).

Warren Toomey, fondatore di TUHS, ha annunciato l’aggiunta alla mailing list del gruppo. TUHS è nota soprattutto per la conservazione del codice sorgente e della documentazione storica di Unix, e il rilascio di KSOS amplia questo impegno includendo un software che ha contribuito a plasmare le successive concezioni dei sistemi operativi sicuri.

KSOS, acronimo di Kernelized Secure Operating System, è stato progettato per fornire un ambiente dimostrabilmente sicuro per minicomputer di grandi dimensioni. A differenza di molti derivati di Unix realizzati in C, KSOS è stato scritto in Modula, un linguaggio type-safe associato a Niklaus Wirth. I suoi sviluppatori puntavano alla verifica formale: il sistema doveva essere analizzato matematicamente e considerato affidabile per l’uso in contesti ad alta sicurezza.

In anticipo sui tempi

Il progetto è iniziato nel 1978 presso Ford Aerospace ed è poi proseguito presso Logicon. Tra le persone coinvolte figuravano il ricercatore di sicurezza Peter Neumann e l’ingegnere Tom Perrine, che in seguito hanno documentato il sistema e ne hanno parlato in conferenze e articoli. Sebbene KSOS traesse ispirazione dalle idee di Unix e offrisse la compatibilità con le chiamate di sistema Unix in modalità supervisore, non condivideva codice del kernel Unix.

KSOS non era soltanto un prototipo di ricerca. Secondo le ricostruzioni storiche, è stato impiegato in produzione per sistemi di intelligence sicuri a più livelli, inclusi ambienti di declassamento affidabili utilizzati da agenzie governative. Esisteva anche una versione per VAX, nota come KSOS-32, mentre la precedente versione per PDP-11 è stata in seguito chiamata KSOS-11.

• Scritto in Modula anziché in C
• Progettato per la verifica formale e un forte isolamento
• Utilizzato su hardware commerciale
• Compilato sotto Unix anziché essere autocompilato

Il rilascio è stato possibile dopo che Perrine ha fornito un vecchio archivio tar del codice sorgente, conservato dal collega sviluppatore Jeff Makey, con l’aiuto di John O Goyo e Thalia Archibald per inserirlo nell’archivio di TUHS. Un interrogativo storico ancora irrisolto riguarda il compilatore originale utilizzato per compilare il sistema, che non è stato ancora identificato.

Il recupero aggiunge un altro importante reperto alla collezione di TUHS dedicata alla storia dei primi sistemi operativi e dimostra che le preoccupazioni relative alla progettazione sicura e alla sicurezza dei tipi erano già oggetto di studio decenni prima che linguaggi moderni come Rust riportassero queste idee nel mainstream.