Google hà annunziatu a scuperta di sviluppi ligati à u prughjettu KataOS, destinatu à creà un sistema operatore sicuru per u hardware integratu. I cumpunenti di u sistema KataOS sò scritti in Rust è eseguite nantu à u microkernel seL4, per quale una prova matematica di affidabilità hè stata furnita nantu à i sistemi RISC-V, chì indicanu chì u codice hè cumplettamente cumpletu cù e specificazioni specificate in a lingua formale. U codice di u prugettu hè apertu sottu a licenza Apache 2.0.
U sistema furnisce supportu per e piattaforme basate nantu à l'architetture RISC-V è ARM64. Per simule l'operazione di seL4 è l'ambiente KataOS in cima di u hardware, u framework Renode hè utilizatu durante u prucessu di sviluppu. Cum'è una implementazione di riferimentu, u cumplessu di software è hardware Sparrow hè prupostu, cumminendu KataOS cù chips sicuri basati nantu à a piattaforma OpenTitan. A suluzione pruposta permette di cumminà un kernel di u sistema operatore verificatu logicamente cù cumpunenti hardware di fiducia (RoT, Root of Trust), custruitu cù a piattaforma OpenTitan è l'architettura RISC-V. In più di u codice KataOS, hè previstu di apre tutti l'altri cumpunenti Sparrow, cumpresu u cumpunente hardware, in u futuru.
A piattaforma hè sviluppata cun un ochju à l'applicazione in chips specializati cuncepiti per eseguisce applicazioni per l'apprendimentu automaticu è l'elaborazione di l'infurmazioni cunfidenziale, chì necessitanu un livellu speciale di prutezzione è cunferma di l'assenza di fallimenti. Esempii di tali applicazioni includenu sistemi chì manipulanu l'imaghjini di e persone è e registrazioni di voce. L'usu di KataOS di verificazione di affidabilità assicura chì, se una parte di u sistema falla, u fallimentu ùn si sparghjerà micca à u restu di u sistema è, in particulare, à u kernel è e parti critiche.
L'architettura seL4 hè notevule per u muvimentu di e parti per a gestione di e risorse di u kernel in u spaziu di l'utilizatori è l'applicà i stessi strumenti di cuntrollu d'accessu per tali risorse cum'è per i risorse di l'utilizatori. U microkernel ùn furnisce micca astrazioni d'altu livellu prontu per a gestione di fugliali, prucessi, cunnessione di rete, è simili; invece, furnisce solu miccanismi minimi per cuntrullà l'accessu à u spaziu di indirizzu fisicu, interruzioni è risorse di processore. L'astrazioni d'altu livellu è i driver per l'interazzione cù u hardware sò implementati separatamente nantu à u microkernel in forma di attività à livellu d'utilizatore. L'accessu di tali compiti à e risorse dispunibili à u microkernel hè urganizatu per mezu di a definizione di regule.
Per una prutezzione supplementaria, tutti i cumpunenti eccettu u microkernel sò sviluppati in modu nativu in Rust utilizendu tecniche di prugrammazione sicura chì minimizzanu l'errore di memoria chì portanu à prublemi cum'è l'accessu à a memoria dopu a liberazione, dereferences di puntatori nulli è buffer overruns. Un caricatore di l'applicazioni in l'ambiente seL4, i servizii di sistema, un framework per u sviluppu di l'applicazioni, una API per accede à e chjama di u sistema, un gestore di prucessu, un mecanismu per l'assignazione di memoria dinamica, etc. sò stati scritti in Rust. L'assemblea verificata usa u toolkit CAmkES, sviluppatu da u prughjettu seL4. I cumpunenti per CAmkES ponu ancu esse creati in Rust.
Rust rafforza a sicurità di a memoria in tempu di compilazione attraversu a verificazione di riferimentu, a pruprietà di l'ughjettu è u seguimentu di a vita di l'ughjettu (scopi), è evaluendu a correttezza di l'accessi di memoria in runtime. Rust furnisce ancu prutezzione contra i overflows integer, richiede valori variabili per esse inizializzati prima di l'usu, usa u cuncettu di referenze immutabili è variabili per difettu, è offre una forte tipografia statica per minimizzà l'errori lògichi.
Source: opennet.ru