Trustworthy Systems

Trianqles: Porting qubes to seL4

Authors

A. Felizzi

    School of Computer Science and Engineering
    UNSW,
    Sydney 2052, Australia

Abstract

Qubes is a security-oriented desktop operating system architecture, aiming to provide security through compartmentalization and isolation. This approach focuses on separating applications and operating system services across separate virtual machines (VMs), preventing exploited applications from compromising the entire operating system.

An integral part of Qubes system architecture is its use of the Xen hypervisor to provide all of its underlying virtualization. Qubes has currently reported 27 CVE’s (Common Vulnerabilities and Exposures) relating to Xen in 2017 alone [Pro17a], and multiple more since its inception in 2010, a substantial portion of which directly compromises the security of Qubes users. Thus Qubes security guarantees are dependent on a relatively heavyweight and unsecure hypervisor to enforce its isolation. Porting Qubes to a more secure architecture becomes increasingly justifiable, motivating a project to move Qubes to seL4, a formally verified microkernel to provide stronger guarantees for achieving isolation and security.

This thesis aims to start laying the necessary implementation framework for achieving a port of Qubes on seL4. This is demonstrated by porting a viable subset of the Qubes architecture to run on seL4.

BibTeX Entry

  @mastersthesis{Felizzi:bsc,
    address          = {Sydney, Australia},
    author           = {A. Felizzi},
    month            = nov,
    paperUrl         = {https://trustworthy.systems/publications/theses_public/17/Felizzi%3Absc.pdf},
    school           = {School of Computer Science and Engineering},
    title            = {Trianqles: Porting Qubes to {seL4}},
    year             = {2017}
  }

Download