[NEWS] Il microkernel più sicuro del mondo

[c.m.g]

martedì 29 settembre 2009

Spoiler:

Ricercatori australiani sostengono di aver realizzato un progresso senza precedenti nel settore dei sistemi operativi: un kernel privo di bug. Lo hanno testato matematicamente

Roma - Non usano mezzi termini, i ricercatori della UNSW e del centro di ricerca NICTA, nel descrivere i risultati di un lavoro durato più di sei anni: seL4, microkernel della famiglia L4 realizzato come base ideale per utilizzi in cui la sicurezza sia la priorità assoluta, è il primo codice di basso livello certificato per essere esente al 100 per cento da bug ed errori di programmazione assortiti.

SeL4 è un microkernel di terza generazione che ha passato indenne i tanti e laboriosi test a cui lo hanno sottoposto i suoi sei autori: un risultato che vale come prova matematica del fatto che l'implementazione delle 7.500 linee di codice di cui è composto risulta consistente con le specifiche ed è assolutamente priva di vulnerabilità di sicurezza, punti morti o errori di buffer overflow da exploitare per condurre ogni genere di azione non autorizzata.

"Una regola empirica dice che un software ragionevolmente ingegnerizzato include 10 bug per mille linee di codice" spiega il professor Gernot Heiser del NICTA, "mentre con software di altissima qualità si può scendere magari a uno o a tre bug per mille linee di codice". Con sistemi operativi e kernel complessi come lo sono quelli moderni, Windows o Linux che siano poco importa, una tale regola implica l'esistenza di parecchi bachi all'interno di codice vitale per l'intera piattaforma.

"Quello che abbiamo dimostrato - continua il professore - è che è possibile realizzare la parte più critica, e in un certo qual senso più pericolosa del sistema senza alcun errore e poi dimostrarne le qualità". "Non penso sia un'esagerazione" aggiunge ancora Heiser "sostenere che questa ricerca apra davvero un mondo completamente nuovo in seno allo sviluppo di sistemi altamente affidabili, altamente sicuri e privi di rischi".

Nell'attesa di verificare quello che avrà combinato Microsoft con il suo ancora misterioso progetto Midori (quantomeno dal punto di vista della verifica formale del codice), il nuovo microkernel australiano si candida come core ideale per ambiti applicativi a rischio zero quali macchinari medico-chirurgici, sistemi militari, cacciabombardieri e via elencando.

Alfonso Maruccia





Fonte: Punto Informatico