Armor SK: a Rust-based separation kernel for safety-critical systems

Virtualization technologies are increasingly being used today in embedded and safety-critical systems because they allow the execution of multiple operating systems, called virtual machines, on the same hardware platform, leading to savings in cost and physical space used. The hypervisor is the program which is responsible for providing isolation and security between the virtual machines; in safety-critical systems, its design is usually based on the static partitioning architecture, which reduces the complexity and provides strong determinism. The programming language mostly used for this kind of applications is C which, however, is considered unsafe because it does not apply any memory check, neither at compile time nor at runtime. Therefore, this thesis presents Armor SK, a lightweight separation kernel written in Rust, which is a programming language mainly known for its memory safety checks. Armor SK targets MPU-based architectures, which are used in safety-critical systems, and its design is based on the use of Rust features called traits and generics. A comparison with Bao, a static partitioning hypervisor developed in C, is presented to examine the different approaches to manage portability of the code and illustrating how Rust traits and generics can help for a simpler porting to a new architecture. An assessment is carried out to determine whether a Rust-based hypervisor can perform similarly to a C-based one, even when bound checking is applied at runtime. Finally, this thesis highlights the differences in the ELF sections of Armor SK and Bao, motivating the reasons behind them.

Le tecnologie di virtualizzazione sono sempre maggiormente utilizzate oggi nei sistemi embedded e in sistemi critici per la sicurezza poiché permettono l'esecuzione di più sistemi operativi, chiamati macchine virtuali, sulla stessa piattaforma hardware, portando ad un risparmio di costi e di spazio fisico occupato. L'hypervisor è il programma che ha il compito di fornire isolamento e sicurezza tra le macchine virtuali; nei sistemi critici, il suo design si basa spesso su un'architettura a partizionamento statico, che riduce la complessità e garantisce un maggiore determinismo. Il linguaggio più utilizzato per questo tipo di applicazioni è il C che, tuttavia, è considerato non sicuro poiché non dispone di controlli della memoria, né in fase di compilazione né durante l'esecuzione del programma. Questa tesi presenta Armor SK, un hypervisor minimale e compatto a partizionamento statico scritto in Rust, un linguaggio di programmazione conosciuto principalmente per i suoi controlli di sicurezza sulla memoria. Armor SK si focalizza su architetture utilizzate in sistemi critici per la sicurezza, le quali sfruttano l'unità di protezione della memoria, ed il suo design si basa su funzionalità fornite da Rust chiamate tratti e generici. Viene presentato un confronto con Bao, un hypervisor a partizionamento statico sviluppato in C, per esaminare le tecniche utilizzate per migliorare la portabilità del codice e illustrando come tratti e tipi generici di Rust possano facilitare il porting su una nuova architettura. Viene condotta una valutazione sulle performance di Armor SK per determinare se un hypervisor scritto in Rust possa raggiungere prestazioni comparabili ad uno sviluppato in C, stimando anche l'impatto dei controlli sugli accessi agli array. Infine, questa tesi analizza le differenze nelle sezioni dei file ELF di Armor SK e Bao, spiegandone le cause.