Non c’erano riuscite le grandi università americane. Non c’erano riuscite le grandi società monopolistiche come IBM e Microsoft. Non c’erano riuscite le grandi società innovatrici e generatrici di creatività digitale, come Sun Microsystems, Dec, Digital, Compaq, HP, Apple e tutte le altre. Non c’erano riuscite le folle ordinate di Linux. Insomma, non c’era mai riuscito nessuno, fino a ieri.
Poi, i ragazzi del Nicta, l’Information and Communications Technology Centre of Excellence, ce l’hanno fatta. Hanno tirato fuori un microkernel (sorry, Torvalds) chiamato “Secure Embedded L4”, o seL4 per gli amici. E sostengono che sia perfetto, almeno dal punto di vista della sicurezza.
Non è una cosa da poco, si dice, perché poter utilizzare un kernel sicuro al 100 per cento, senza margine di errore, serve per una serie di applicazioni critiche: è ottimo per mandare gli astronauti sulla Luna, su Marte e anche oltre, è ottimo per far girare le mini-centrali nucleari in un sottoscala in pieno centro, è ottimo per far volare 600 persone su un mega-jumbo totalmente automatizzato.
Ma come si fa a sapere che in effetti il kernel è perfettamente sicuro, è super-blindato e funzionante, a prova di bug? I quattro anni di ricerca degli australiani sono serviti soprattutto a questa seconda cosa: il Nicta ha lavorato duramente per capire se le 7.500 linee di codice scritte in C erano davvero a prova di bomba. Essendo tutta roba che funziona sul computer, hanno provato con sistemi di analisi matematica molto raffinata. E sostengono di esserci riusciti: proprio questa è la “scoperta” del progetto di ricerca.
200mila righe di prova formale, 10mila teoremi intermedi provati per la prima volta, controlli automatici di tutti i tipi. In pratica, grazie a software di analisi e prova-teoremi interattivi come “Isabelle”, è stato condotta la più grande sperimentazione di questo tipo che il pianeta abbia mai conosciuto. Ed ha condotto a risultati sicuri e definitivi. seL4 è il sistema operativo più perfettamente sicuro della seppur breve storia dei sistemi operativi.
Grazie a questo test di 4 anni il team del Nicta ha scoperto una serie di cose finora ignote sia dal punto di vista della ricerca “sul campo” per la profilazione, prototipazione, test e verifica del software in real time, usando matematica mai tentata prima su un kernel di queste dimensioni e non per test limitati a specifiche funzionalità , ma per tutta quanta la vita operativa del kernel. E il risultato è, come dicevamo sopra, aver prodotto non solo e non tanto il kernel perfetto (e bisogna prendere ovviamente “cum grano salis” questa affermazione scientifica e non metafisica) quanto una nuova generazione di strumenti software e concettuali per la costruzione e la verifica di manufatti software complessi.
