{"id":105309,"date":"2022-10-15T15:37:02","date_gmt":"2022-10-15T13:37:02","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/google-otkryl-kod-zashhishhyonnoj-operaczionnoj-sistemy-kataos"},"modified":"2022-10-15T15:37:02","modified_gmt":"2022-10-15T13:37:02","slug":"google-otkryl-kod-zashhishhyonnoj-operaczionnoj-sistemy-kataos","status":"publish","type":"post","link":"https:\/\/prohoster.info\/it\/blog\/novosti-interneta\/google-otkryl-kod-zashhishhyonnoj-operaczionnoj-sistemy-kataos","title":{"rendered":"Google ha aperto il codice del sistema operativo protetto KataOS","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Google ha annunciato l'apertura di progetti legati a KataOS, un sistema operativo sicuro progettato per dispositivi embedded. I componenti di sistema di KataOS sono scritti in Rust e vengono eseguiti su un microkernel seL4, per il quale sono state fornite prove matematiche di affidabilit\u00e0 sui sistemi RISC-V, che attestano la completa conformit\u00e0 del codice alle specifiche definite in un linguaggio formale. Il codice del progetto \u00e8 aperto sotto licenza Apache 2.0. <\/p>\n
Il sistema supporta piattaforme basate su architetture RISC-V e ARM64. Per simulare il funzionamento di seL4 e dell'ambiente KataOS sopra l'hardware durante il processo di sviluppo, viene utilizzato il framework Renode. Come implementazione di riferimento, \u00e8 proposto un complesso software e hardware chiamato Sparrow, che combina KataOS con chip sicuri basati sulla piattaforma OpenTitan. La soluzione proposta consente di unire un kernel di sistema operativo logicamente verificato con componenti hardware affidabili (RoT, Root of Trust), costruiti utilizzando la piattaforma OpenTitan e l'architettura RISC-V. Oltre al codice di KataOS, in futuro \u00e8 previsto l'apertura di tutti gli altri componenti di Sparrow, compresi quelli hardware. <\/p>\n
La piattaforma si sviluppa tenendo conto dell'uso in chip specializzati, progettati per eseguire applicazioni per l'apprendimento automatico e l'elaborazione di informazioni riservate, che richiedono un particolare livello di protezione e conferma dell'assenza di malfunzionamenti. Un esempio di tali applicazioni \u00e8 rappresentato da sistemi che manipolano le immagini delle persone e le registrazioni vocali. L'uso di KataOS per la verifica dell'affidabilit\u00e0 garantisce che, in caso di guasto in una parte del sistema, tale guasto non si propaghi al resto del sistema e, in particolare, al nucleo e alle parti critiche. <\/p>\n
L'architettura seL4 \u00e8 notevole per l'estrazione delle parti di gestione delle risorse del nucleo nell'area utente e per l'applicazione agli stessi risorse degli stessi strumenti di accesso impiegati per le risorse utente. Il microkernel non offre astrazioni di alto livello pronte per la gestione di file, processi, connessioni di rete, ecc.; al contrario, fornisce solo meccanismi minimi per gestire l'accesso allo spazio fisico degli indirizzi, alle interruzioni e alle risorse della CPU. Le astrazioni di alto livello e i driver per interagire con l'hardware vengono implementati separatamente sopra il microkernel sotto forma di attivit\u00e0 eseguite a livello utente. L'accesso a queste risorse da parte delle attivit\u00e0 che operano a livello utente \u00e8 organizzato attraverso la definizione di regole. <\/p>\n
Per una maggiore sicurezza, tutti i componenti, ad eccezione del microkernel, sono inizialmente sviluppati in Rust utilizzando pratiche di programmazione sicure che minimizzano gli errori di gestione della memoria, evitando problemi come l'accesso alla memoria dopo la sua liberazione, dereferenziazione di puntatori nulli e overflow del buffer. In Rust sono scritti anche il caricatore delle applicazioni nell'ambiente seL4, i servizi di sistema, il framework per lo sviluppo di applicazioni, l'API per l'accesso alle chiamate di sistema, il gestore dei processi, il meccanismo di allocazione dinamica della memoria, e cos\u00ec via. Per la build verificata \u00e8 stato utilizzato lo strumento CAmkES, sviluppato dal progetto seL4. I componenti per CAmkES possono essere creati anche in Rust. <\/p>\n
La gestione sicura della memoria in Rust avviene durante la fase di compilazione attraverso la verifica dei riferimenti, il monitoraggio della propriet\u00e0 degli oggetti e la gestione della durata di vita degli oggetti (scope), nonch\u00e9 attraverso la valutazione della correttezza dell'accesso alla memoria durante l'esecuzione del codice. Rust offre anche strumenti per proteggere contro il overflow intero, richiede l'inizializzazione obbligatoria delle variabili prima del loro utilizzo, applica il concetto di immutabilit\u00e0 (immutable) per riferimenti e variabili per impostazione predefinita, e propone un forte sistema di tipi statici per minimizzare gli errori logici. \n Fonte: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"