In recent years, trusted execution environments (TEEs) have seen increasing deployment in computing devices to protect security-critical software from run-time attacks and provide isolation from an untrustworthy operating system (OS). A trusted party verifies the software that runs in a TEE using remote attestation procedures. However, the publication of transient execution attacks such as Spectre and Meltdown revealed fundamental weaknesses in many TEE architectures, including Intel Software Guard Exentsions (SGX) and Arm TrustZone. These attacks can extract cryptographic secrets, thereby compromising the integrity of the remote attestation procedure. In this work, we design and develop a TEE architecture that provides remote attestation integrity protection even when confidentiality of the TEE is compromised. We use the formally verified seL4 microkernel to build the TEE, which ensures strong isolation and integrity. We offload cryptographic operations to a secure co-processor that does not share any vulnerable microarchitectural hardware units with the main processor, to protect against transient execution attacks. Our design guarantees integrity of the remote attestation procedure. It can be extended to leverage co-processors from Google and Apple, for wide-scale deployment on mobile devices. / Under de senaste åren används betrodda exekveringsmiljöer (TEE) allt mera i datorutrustning för att skydda säkerhetskritisk programvara från attacker och för att isolera dem från ett opålitligt operativsystem. En betrodd part verifierar programvaran som körs i en TEE med hjälp av fjärrattestering. Nyliga mikroarkitekturella anfall, t.ex. Spectre och Meltdown, har dock visat grundläggande svagheter i många TEE-arkitekturer, inklusive Intel SGX och Arm TrustZone. Dessa attacker kan avslöja kryptografiska hemligheter och därmed äventyra integriteten av fjärrattestning. I det här arbetet utvecklar vi en arkitektur för en betrodd exekveringsmiljö (TEE) som ger integritetsskydd genom fjärrattestering även när TEE:s konfidentialitet äventyras. Vi använder den formellt verifierade seL4-mikrokärnan för att bygga TEE:n som garanterar stark isolering och integritet. För att skydda kryptografiska operationer, overför vi dem till en säker samprocessor som inte delar någon sårbar mikroarkitektur med huvudprocessorn. Vår arktektur garanterar fjärrattesteringens integritet och kan utnyttja medprocessorer från Google och Apple för att användas i stor skala på mobila enheter.

Communication in microkernel-based systems is much more frequent than system calls known from monolithic kernels. This can be attributed to the placement of system services into their own protection domains. Communication has to be fast to avoid unnecessary overhead. Also, communication channels in microkernel-based systems are used for more than just remote procedure calls. In distributed systems, which also have a componentized design, it is state of the art to use tools to generate stubs for the communication between components. The communication interfaces of components are described in an interface definition language (IDL). In contrast to distributed systems, components of a microkernel-based system run on the same architecture and message delivery is guaranteed. In this Thesis, I explore the different kinds of communication, which can be used in microkernel-based systems, as well as their possible representation in IDL. Specifically, I introduce the syntax to describe kernel objects in IDL. I discuss the complexity of IDL compilers and its relation to the complexity of the IDL. Furthermore, I evaluate the performance of the communication stubs generated by different IDL compilers and discuss techniques to minimize performance overhead in generated stubs. I validated these techniques by implementing the Drops IDL Compiler - Dice. Finally, this Thesis presents a mechanism to measure the frequency and performance of invocations of generated communication code. I used this technique to conduct measurements in highly complex systems and introducing the least possible overhead.

This thesis describes the primary goal of the HelenOS microkernel multiserver operating system. The primary goal of the HelenOS project is to create a comprehensive research and development platform in the domain of general-purpose operating systems that would support state-of-the-art approaches and methods (such as verification of correctness) while at the same time focusing on practical relevance. The text of the thesis describes what specific means in terms of design (based on software components), implementation, development process and verification are used to achieve the primary goal. The thesis also evaluates the current state of HelenOS. Powered by TCPDF (www.tcpdf.org)

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.

Communication in microkernel-based systems is much more frequent than system calls known from monolithic kernels. This can be attributed to the placement of system services into their own protection domains. Communication has to be fast to avoid unnecessary overhead. Also, communication channels in microkernel-based systems are used for more than just remote procedure calls. In distributed systems, which also have a componentized design, it is state of the art to use tools to generate stubs for the communication between components. The communication interfaces of components are described in an interface definition language (IDL). In contrast to distributed systems, components of a microkernel-based system run on the same architecture and message delivery is guaranteed. In this Thesis, I explore the different kinds of communication, which can be used in microkernel-based systems, as well as their possible representation in IDL. Specifically, I introduce the syntax to describe kernel objects in IDL. I discuss the complexity of IDL compilers and its relation to the complexity of the IDL. Furthermore, I evaluate the performance of the communication stubs generated by different IDL compilers and discuss techniques to minimize performance overhead in generated stubs. I validated these techniques by implementing the Drops IDL Compiler - Dice. Finally, this Thesis presents a mechanism to measure the frequency and performance of invocations of generated communication code. I used this technique to conduct measurements in highly complex systems and introducing the least possible overhead.

<p>Teza se bavi povećanjem ukupne oslonljivosti modularnog mikrokernel<br />operativnog sistem MINIX 3 kroz povećanje pouzdanosti njegovog<br />mrežnog podsistema. To je postignuto tako što je ovom operativnom<br />sistemu dodata agregacija mrežnih veza, čime je podražana<br />tolerancija na poremećaj komunikacionih linija. Na kraju je data<br />analiza kako dodati deo utiče na ukupne mrežne performanse.</p> / <p>The thesis deals with the way to increase the dependability of the modular<br />microkernel operating system MINIX 3 through the increase of the reliability<br />of its network subsystem. This is achieved by adding link aggregation to this<br />operating system, which added fault tolerance for the communication lines. At<br />the end, the analysis is given of how new module affects the overall network<br />performance.</p>

This thesis deals with the implementation of ACP protocol which serves to manage the access for operation system based on L4 microkernel. The theoretical part of the thesis deals with methods of access management in computer networks. It focuses primarily on AAA systems which make access management possible. Furthermore it describes in detail the ACP protocol, the types of messages and their feedback. The next theoretical part is dedicated to operation systems and in particular to their architecture and services. Then we get a closer look at L4 microkernel family, their philosophy and properties. We continue with a detailed description of the L4 application interface and its ways of expansion. The practical section deals with the implemented concept of system for ACP protocol support in computers. General concept is then applied in real implementation of ACP protocol into the L4 operation system environment based on the L4 platform. To assist, I also included a detailed tutorial explaining the modeling and compilation of software for this platform. At this point we describe the methods used at the implementation and the description of particular modules and features. The end of the thesis concludes the information about the ways of testing and the implementation properties.