Verve è l'ultimo sistema operativo non Windows per il quale Microsoft ha deciso di condividerne le informazioni attraverso il libro bianco in pdf intitolato "Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System". Ancora solo un prototipo di Microsoft Research, Verve è concepito come un sistema operativo e run-time di sistema che il gigante del software si è sforzato di rendere sicuro. Secondo l'azienda di Redmond, Verve è lo spin-off di un altro sistema operativo non Windows con cui gli utenti potrebbero già avere familiarità.
La piattaforma del progetto è singolare, si tratta d'un sistema operativo scritto in codice utilizzato per scopi di ricerca, che ha ispirato le nuove piattaforme come Verve, ma anche Midori, su cui sono a disposizione piccoli dettagli. Microsoft rivela che la sicurezza generale è garantita meccanicamente dal sistema operativo verificando ogni istruzione in linguaggio assembly nello stack software della sicurezza. In sostanza, tutte le istruzioni di tutti i software che gira sopra della piattaforma vengono controllati. "Il linguaggio assembly tipizzato (TAL) e la logica di Hoare possono verificare l'assenza di molti tipi di errori nel codice di basso livello.
Noi usiamo logica TAL e Hoare per raggiungere automatizzazioni elevate, la verifica statica della sicurezza di un nuovo sistema operativo chiamato Verve. Le nostre tecniche e gli strumenti verificano meccanicamente la sicurezza di ogni istruzione in linguaggio assembly nel sistema operativo, in fase di esecuzione del sistema, driver e le applicazioni (infatti, ogni parte del software di sistema, tranne il boot loader)", si legge un estratto dal libro bianco che accompagna il sistema operativo. In effetti gli assembler tipizzati non sono una novità per Microsoft, ma con Verve è la prima volta che vengono impiegati in un vasto progetto.
Dal punto di vista dell'architettura Verve si distingue da Windows perchè il kernel è affiancato da un Nucleo che si occupa del collegamento con l'hardware. Il kernel funge sostanzialmente da interfaccia tramite la quale i programmi possono avviare thread e processi. In Verve sia il kernel che i programmi sono compilati tramite assembler tipizzato, questo fa sì che non solo la struttura di base sia priva di errori e sicura ma anche tutto il resto del sistema e i programmi.
"Verve è costituito da un Nucleo, che fornisce l'accesso all'hardware primitivo e la memoria, un kernel che costruisce i servizi sulla parte superiore del Nucleo, e le applicazioni che vengono eseguite sul kernel superiore. Il Nucleo, scritto in linguaggio assembly verificato, implementa l'allocazione, la garbage collection, le stack multiple, la gestione degli interrupt, e l'accesso al dispositivo. Il kernel, scritto in C # e compilato in TAL, costruisce il più alto livello di servizi, come ad esempio i thread preventivi, sulla parte superiore del Nucleo. Una TAL checker verifica la sicurezza del kernel e le applicazioni. Un verificatore Hoare-style con un automated theorem prover (ATP), verifica sia la sicurezza che la correttezza del Nucleo", fà notare la società.
Microsoft rivela che Verve è il primo sistema operativo sia per la verifica meccanica che la sicurezza della memoria. In pratica su Verve non è possibile generare alcun buffer overflow, perchè durante la traduzione del codice programma il modello può essere verificato. I programmi utilizzati in fase di sviluppo sono ancora benchmark e non è stata implementata la connessione Tcp. Inoltre il sistema operativo gira attualmente solo su Cpu single core. Chi vuol provare Verve, compilando preventivamente il codice sorgente, può collegarsi al portale open source di Microsoft all'indirizzo www.codeplex.com. Non è dato sapere se le innovazioni di Verve verranno già implementate nel prossimo sistema operativo Windows 8.
Nessun commento:
Posta un commento