Over the past decade, researches on operating systems have been shifted from monolithic kernels towards microkernels for several reasons. Of them are: (1) It is easier to understand and debug because the kernel is much smaller. (2) It is much more secure and flexible because the kernel is small, and most of the kernel functions can be implemented as servers running in the user space instead of in the kernel space. (3) The message passing technique that is in the core of the microkernel has been improved, and thus the overhead required for the message passing has been highly reduced. Minix 3 is one of the microkernels developed over the past decade and is aimed for educational purpose and small PCs. It is implemented on the IA-32 architecture and is based on the segmented memory model of IA-32. The purpose of this thesis is to use Minix 3 as a case study and to convert the segmented memory model adopted by the current implementation to coexisted with the demand paged memory model, which is also supported by the IA-32 architecture. That said, the thesis can be divided into two parts: The first part is to implement a new server called pager, which would take over the memory management subsystem of the Minix 3 microkernel and be used to offload the overhead of the kernel. The second part is to implement a virtual memory management subsystem that uses the segmentation with paging memory model of the IA-32 architecture.

Traditional network stacks in monolithic kernels have reliability and security concerns. Any fault in a network stack affects the entire system owing to lack of isolation in the monolithic kernel. Moreover, the large code size of the network stack enlarges the attack surface of the system. A multiserver OS design solves this problem. In contrast to the traditional network stack, a multiserver OS pushes the network stack into the network server as a user process, which performs three enhancements: (i) allows the network server to run in user mode while having its own address space and isolating any fault occurring in the network server; (ii) minimizes the attack surface of the system because the trusted computing base contracts; (iii) enables failure recovery, which is an important feature supported by a multiserver OS. This thesis proposes a network server for LibrettOS, an operating system based on rumprun unikernels and the Xen Hypervisor developed by Virginia Tech. The proposed network server is a service domain providing an L2 frame forwarding service for application domains and based on rumprun such that the existing device drivers of NetBSD can be leveraged with little modification. In this model, the TCP/IP stack runs directly in the address space of applications. This allows retaining the client state even if the network server crashes and makes it possible to recover from a network server failure. We leverage the Xen PCI passthrough to access a NIC (Network Interface Controller) from the network server. Our experimental evaluation demonstrates that the performance of the network server is good and comparable with Linux and NetBSD. We also demonstrate the successful recovery after a failure. / This research is based upon work supported by the Office of the Director of National Intelligence (ODNI), Intelligence Advanced Research Projects Activity (IARPA). The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the ODNI, IARPA, or the U.S. Government. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright annotation thereon. This research is also based upon work supported by the Office of Naval Research (ONR) under grants N00014-16-1-2104, N00014-16-1-2711, and N00014-18-1-2022. / Master of Science / When it comes to reliability and security in networking systems, concerns have been shown in traditional operating systems (OSs) such as Windows, MacOS, NetBSD, and Linux. Any fault in a networking system can have impacts on the entire system owing to lack of isolation in the OSs. Moreover, the large code size of a networking system enlarges the attack surface of the system. A multiserver OS design solves this problem by running a networking system as a network server, which performs three enhancements: (i) isolates any fault occurring in the network server itself; (ii) minimizes the attack surface of the system; and (iii) enables failure recovery. This thesis proposes a network server for LibrettOS, an operating system developed by Virginia Tech. The proposed network has two-pronged merits: (i) provides a system server providing a network packet forwarding service for applications; (ii) enables the existing device drivers of NetBSD to be leveraged with low amount of modification. Our experimental evaluation demonstrates that the performance of the network server outperforms state-of-the-art and comparable with Linux and that a successful recovery is possible after a failure.

Capability to route can be considered as one of the key features of a modern multipurpose operating system, which HelenOS aims to be. The goal of this master thesis is to explore current HelenOS routing capabilities, enhance them and empower HelenOS with BIRD. HelenOS will become a routing operating system with awareness of its surroundings. It will be capable of dynamic adaptation to changes in the network and their propagation.

Capability to route can be considered one of key features of modern multipurpose operating system, which HelenOS aims to be. Goal of this master thesis is to explore current HelenOS routing capabilities, enhance them and empower HelenOS with BIRD. Thanks to BIRD, HelenOS will become a routing operating system, that is aware of its surroundings and is capable of dynamic adaptation to changes in network, it is part of.

Software-Defined Networking (SDN) is a technology that is increasing in popularity. However, with increased prevalence comes increased opportunity to exploit vulnerabilities that exist within the technology. In this thesis, several attack vectors that can be used to attack SDN controllers were identified through a literature review. Among these vectors there is one that is concerned with the vulnerabilities present on the host of the SDN controller. One promising method that could be used to mitigate this attack vector is to deploy the SDN controller on a microkernel. The microkernel chosen in this thesis is the formally verified microkernel seL4®. This thesis investigate the possible ways of deploying an SDN controller on seL4. A deployment of an SDN controller is also performed in this thesis in order to assess the difficulties and possible performance tradeoffs present in adapting an SDN controller for seL4. The deployment of the SDN controller uses seL4’s virtualization capabilities and leaves the majority of the controller running in a virtual machine on seL4. A small part of the controller is moved to a separate and isolated component in order to showcase how the isolation capabilities of seL4 can be utilized. The performances of the unmodified and the modified controller are then compared. A significant increase in execution time when communicating between the VM and the separate component was discovered. However, such increases may also be attributed to dynamic binary translation used when simulating seL4 using QEMU. Thus, properly quantifying these overheads would require a different setup, either without simulation or with hardware-assisted virtualization.

Title: Security containers and access rights in HelenOS Author: Štěpán Henek Department: Department of Software Engineering Supervisor: Mgr. Martin Děcký Supervisor's e-mail address: decky@ksi.mff.cuni.cz Abstract: The goal of this thesis is to design and implement security containers (contexts) for tasks and access rights mechanisms for microkernel operating systems. The access rights mechanisms implement common paradigms such as user identification, groups of users, system entities (tasks, files) ownership, user capabilities and access control lists. Moreover, the design allows to implement hierarchical security domains, where each domain is able to delegate a subset of its permissions to its subdomains. The design also enables the implementa- tion of containers, which mutually isolate those tasks, which are situated in security domains with an empty intersection. The thesis comprises of an analysis and evaluation of possible approaches, a prototype imple- mentation in HelenOS with respect to its specific properties (emphasis on a small context switch overhead, delegation of security mechanisms to privileged user space tasks, etc.) and also com- parison with implementations of security containers and access rights mechanisms in generally available operating systems. Keywords: security contexts, access...

Most of today's widely used operating systems are based on a monolithic design and have a very large code size which complicates verification of security-critical applications. One approach to solving this problem is to use a microkernel, i.e., a small kernel which only implements the bare necessities. A system usinga microkernel can be constructed using the operating-system framework Genode, which provides security features and a strict process hierarchy. However, these systems may still be vulnerable to microarchitectural attacks, which can bypassan operating system's security features, exploiting vulnerable hardware. This thesis aims to investigate whether microkernels are vulnerable to the microarchitectural attacks Meltdown and Spectre version 1 in the context of Genode. Furthermore, the thesis analyzes the execution cost of mitigating Spectre version 1 in a Genode's remote procedure call. The result shows how Genode does not mitigate the Meltdown attack, which will be confirmed by demonstrating a working Meltdown attack on Genode+Linux. We also determine that microkernels are vulnerable to Spectre by demonstrating a working attack against two microkernels. However, we show that the cost of mitigating this Spectre attack is small, with a cost of < 3 slowdown for remote procedure calls in Genode.

Although modern computer systems process increasing amounts of sensitive, private, and valuable information, most of today’s operating systems (OSs) fail to protect confidential data against unauthorized disclosure over covert channels. Securing the large code bases of these OSs and checking the secured code for the absence of covert channels would come at enormous costs. Microkernels significantly reduce the necessarily trusted code. However, cost-efficient, provable confidential-data protection in microkernel-based systems is still challenging. This thesis makes two central contributions to the provable protection of confidential data against disclosure over covert channels: • A budget-enforcing, fixed-priority scheduler that provably eliminates covert timing channels in open microkernel-based systems; and • A sound control-flow-sensitive security type system for low-level operating-system code. To prevent scheduling-related timing channels, the proposed scheduler treats possibly leaking, blocked threads as if they were runnable. When it selects such a thread, it runs a higher classified budget consumer. A characterization of budget-consumer time as a blocking term makes it possible to reuse a large class of existing admission tests to determine whether the proposed scheduler can meet the real-time guarantees of all threads we envisage to run. Compared to contemporary information-flow-secure schedulers, significantly more real-time threads can be admitted for the proposed scheduler. The role of the proposed security type system is to prove those system components free of security policy violating information flows that simultaneously operate on behalf of differently classified clients. In an open microkernel-based system, these are the microkernel and the necessarily trusted multilevel servers. To reduce the complexity of the security type system, C++ operating-system code is translated into a corresponding Toy program, which in turn is complemented with calls to Toy procedures describing the side effects of interactions with the underlying hardware. Toy is a non-deterministic intermediate programming language, which I have designed specifically for this purpose. A universal lattice for shared-memory programs enables the type system to check the resulting Toy code for potentially harmful information flows, even if the security policy of the system is not known at the time of the analysis. I demonstrate the feasibility of the proposed analysis in three case studies: a virtual-memory access, L4 inter-process communication and a secure buffer cache. In addition, I prove Osvik’s countermeasure effective against AES cache side-channel attacks. To my best knowledge, this is the first security-type-system-based proof of such a countermeasure. The ability of a security type system to tolerate temporary breaches of confidentiality in lock-protected shared-memory regions turned out to be fundamental for this proof.

Existing Building Automation Systems (BASs) and Building Automation Networks (BANs) have been shown to have serious cybersecurity problems. Due to the safety-critical and interconnected nature of building subsystems, local and network access control needs to be finer grained, taking into consideration the varying criticality of applications running on heterogeneous devices. In this paper, we present a secure communication framework for BASs that 1) enforces rich access control policy for operating system services and objects, leveraging a microkernel-based architecture; 2) supports fine-grained network access control on a per-process basis; 3) unifies the security control of inter-device and intra-device communication using proxy processes; 4) tunnels legacy insecure communication protocols (e.g., BACnet) through a secure channel, such as SSL, in a manner transparent to legacy applications. We implemented the framework on seL4, a formally verified microkernel. We conducted extensive experiments and analysis to compare the performance and effectiveness of our communication systems against a traditional Linux-based implementation of the same control scenario. Our experiments show that the communication performance of our system is faster or comparable to the Linux-based architecture in embedded systems.

Most operating systems provide protection and isolation to user processes, but not to critical system components such as device drivers or other systems code. Consequently, failures in these components often lead to system failures. VirtuOS is an operating system that exploits a new method of decomposition to protect against such failures. VirtuOS exploits virtualization to isolate and protect vertical slices of existing OS kernels in separate service domains. Each service domain represents a partition of an existing kernel, which implements a subset of that kernel's functionality. Service domains directly service system calls from user processes. VirtuOS exploits an exceptionless model, avoiding the cost of a system call trap in many cases. We illustrate how to apply exceptionless system calls across virtualized domains. To demonstrate the viability of VirtuOS's approach, we implemented a prototype based on the Linux kernel and Xen hypervisor. We created and evaluated a network and a storage service domain. Our prototype retains compatibility with existing applications, can survive the failure of individual service domains while outperforming alternative approaches such as isolated driver domains and even exceeding the performance of native Linux for some multithreaded workloads. The evaluation of VirtuOS revealed costs due to decomposition, memory management, and communication, which necessitated a fine-grained analysis to understand their impact on the system's performance. The interaction of virtual machines with multiple underlying software and hardware layers in virtualized environment makes this task difficult. Moreover, performance analysis tools commonly used in native environments were not available in virtualized environments. Our work addresses this problem to enable an in-depth performance analysis of VirtuOS. Our Perfctr-Xen framework provides capabilities for per-thread analysis with both accumulative event counts and interrupt-driven event sampling. Perfctr-Xen is a flexible and generic tool, supports different modes of virtualization, and can be used for many applications outside of VirtuOS. / Ph. D.