Questo sito contiene link di affiliazione per cui può essere compensato

Home » Hi-Tech » Nuove Tecnologie » Il kernel perfetto e blindato? Esiste ed è stato creato in Australia

Il kernel perfetto e blindato? Esiste ed è stato creato in Australia

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.

Offerte Apple e Tecnologia

Le offerte dell'ultimo minuto le trovi nel nostro canale Telegram

Top offerte Apple su Amazon

Prezzo bomba per il MacBook Air M2, solo 999 euro

Amazon sconta sullo sconto Apple per il MacBook Air M2: lo pagate solo 999, 250 euro meno del prezzo di ufficiale con uno sconto del 26%

Ultimi articoli

Pubblicità