SeL4 Microkernel Operating System

seL4 is a microkernel (the small core of an operating system), not a full desktop operating system. seL4 is known as a high-assurance and high-performance operating system at the kernel level. It provides a great level of verification features without affecting compute resources. It is an open-source operating system. [1] seL4 also provides fine-grained access controls, and controls communications between components in the system. One of its greatest key features is its mathematical proof of correctness where there should be no errors (mathematically) and (bug-free), enforcing its security properties. [2] Some of the pros of using seL4 are notably its assurance of isolation between applications where if one part of the system is compromised it can be contained from affecting other parts of the operating system. Some other pros have already been mentioned like it being the first OS to be mathematically proven correct and it being bug free in terms of it being formally verified. It can be relied upon and has even been used for DARPA funded projects. Some cons for this OS are it can be complex to set up and maintain, where someone will need to know how to set it up to be used properly. Also, it is still a small open-source project with limited ecosystem buy in from the OSS community.

Qubes Operating System

Qubes OS is an open-source, security-oriented operating system for single-user desktops computing. [3] Qubes OS uses the xen-based virtualization architecture to allow for the management of isolated compartments called “Qubes”. Some of the key pros for using this OS is the ability to have isolated applications running in a single view. You can manage your network stacks and firewalls in one VM, surf the web on another, and work on professional projects like a coding an application all in separate VMs and under one management view. If malware affects one VM it will be isolated to that VM. The Qubes OS also offers multi-layered security features on top of having VMs like network segmentation – adding to its defense in depth. Some of the cons of the Qubes OS are it is resource intensive whereby running multiple VMs at one time can drastically drain your computers CPUs resources.

Tails Operating System

The Tails Operating System is a privacy-focused Linux distribution you can run on as a live OS from a USB or DVD. It uses the Tor network by default to increase anonymity. Tor is a network that hides where web traffic comes from by passing it through several volunteer computers. [4] It also only runs once its live, erases all data when turned off and leaves no trace on the host system it runs on. Tails OS is also an free open-source repo. [5]  I found it interesting that on the tails.net website on their front page they advertise who uses tails: activists, Journalists, and domestic violence survivors. They advertise if you’re one of these people, you can use tails to hide what you do on the internet. “Domestic violence survivors..use tails to escape surveillance at home,” as stated on the website. Tails is technology that gives power back to the people bottom line. Another interesting read I found was a post on reddit where someone says they have an online stalker/creep for many years and continue to monitor their online activity and mentioned tails being recommended for privacy. [6]Some cons of using the tails OS are its performance slowing down due to using the Tor network, having to log in again after booting back up, and it just not being a long-term solution for everyday computer use, it should just be used for privacy.

Related reading: Keyloggers Explained: Uses, Risks, and Ethics. Both posts discuss protecting people from being watched.

References