L'azienda Google ha presentato il complesso software e hardware Open Se Cura, progettato per semplificare la creazione di chip protetti, destinati a risolvere problemi legati all'apprendimento automatico e all'intelligenza artificiale. Il progetto include il sistema operativo CantripOS e l'hardware basato sulla piattaforma OpenTitan e su un core di processore basato sull'architettura RISC-V. Durante lo sviluppo, Open Se Cura e CantripOS sono stati conosciuti come Sparrow e KataOS, ma per evitare sovrapposizioni con altri progetti, i prodotti finali sono stati rinominati. I materiali del progetto, compresi i codici sorgente dei servizi di sistema e gli schemi RTL (Register Transfer Level), sono distribuiti sotto licenza Apache 2.0.
Il sistema operativo CantripOS si basa su un microkernel seL4, sopra il quale viene eseguito un ambiente di sistema scritto in linguaggio Rust. Su sistemi RISC-V, per il microkernel seL4 è fornita una prova matematica di affidabilità, che dimostra la piena conformità del codice alle specifiche definite in un linguaggio formale. L'architettura seL4 è notevole per il fatto che sposta parti della gestione delle risorse del kernel nello spazio utente e applica agli stessi strumenti di separazione degli accessi utilizzati per le risorse utente.
Il microkernel non fornisce astrazioni di alto livello pronte per la gestione di file, processi, connessioni di rete, ecc.; invece, fornisce solo meccanismi minimi per la gestione dell'accesso allo spazio indirizzi fisico, alle interruzioni e alle risorse del processore. Le astrazioni di alto livello e i driver per interagire con l'hardware sono implementati separatamente sopra il microkernel sotto forma di task eseguiti a livello utente. L'accesso di tali task alle risorse disponibili del microkernel è organizzato attraverso la definizione di regole.
Tutti i componenti del sistema operativo, ad eccezione del microkernel, sono stati originariamente scritti in Rust utilizzando approcci di programmazione sicuri che minimizzano gli errori nella gestione della memoria. In Rust, tra le altre cose, è stato scritto il caricatore di applicazioni nell'ambiente seL4, i servizi di sistema, un framework per lo sviluppo di applicazioni, un'API per l'accesso alle chiamate di sistema, un gestore dei processi e un meccanismo di allocazione dinamica della memoria.
Per la build verificata è stato utilizzato l'insieme di strumenti CAmkES, sviluppato dal progetto seL4. Per lo sviluppo delle applicazioni finali, che possono essere caricate dinamicamente dai servizi di sistema, si propone di utilizzare l'SDK AmbiML, mentre per l'esecuzione dei modelli di apprendimento automatico si utilizza l'insieme di strumenti IREE (Intermediate Representation Execution Environment). I componenti scritti in Rust e i servizi di sistema sono stati sviluppati utilizzando i framework Cantrip.
Tra i campi di applicazione della piattaforma si segnalano i chip specializzati che richiedono un livello particolare di protezione e conferma dell'assenza di guasti. Ad esempio, la piattaforma può essere utilizzata in prodotti di apprendimento automatico legati all'elaborazione di informazioni riservate, come i sistemi di riconoscimento delle persone e di elaborazione delle registrazioni vocali. La combinazione di un kernel di sistema operativo logicamente verificato con componenti hardware affidabili (RoT, Root of Trust) garantisce che, in caso di guasto in una parte del sistema, tale guasto non si propaghi al resto del sistema e, in particolare, al kernel e alle parti critiche.
Oltre a Google, nello sviluppo dell'insieme di strumenti e degli elementi dell'infrastruttura hanno partecipato l'organizzazione no-profit lowRISC, che supervisiona lo sviluppo di un microprocessore open source basato sull'architettura RISC-V, e le aziende Antmicro e VeriSilicon. Il processore sviluppato da lowRISC è stato utilizzato come base per la costruzione di componenti hardware affidabili (RoT, Root of Trust). L'azienda Antmicro ha fornito al progetto il simulatore Renode, che permette di testare CantripOS e il microkernel seL4 senza hardware reale. L'azienda VeriSilicon ha condiviso la propria esperienza nella progettazione di chip e nello sviluppo di BSP (Board Support Package).
Fonte: opennet.ru
