Dissertation/Thesis Abstract

Antikernel: A decentralized secure hardware-software operating system architecture
by Zonenberg, Andrew D., Ph.D., Rensselaer Polytechnic Institute, 2015, 148; 3705663
Abstract (Summary)

Security of monolithic kernels, and even microkernels, relies on a large and complex body of code (including both software and hardware components) being entirely bug-free. Most contemporary operating systems can be completely compromised by a bug anywhere in this codebase, from the network stack to the CPU pipeline's handling of privilege levels, regardless of whether a particular application uses that feature or not. Even formally verified software is vulnerable to failure when the hardware, or the hardware-software interface, has not been verified.

This thesis describes Antikernel, a novel operating system architecture consisting of both hardware and software components and designed to be fundamentally more secure than the existing state of the art. In order to make formal verification easier, and improve parallelism, the Antikernel system is highly modular and consists of many independent hardware state machines (one or more of which may be a general-purpose CPU running application or systems software) connected by a packet-switched network-on-chip (NoC).

The Antikernel architecture is unique in that there is no "all-powerful" software which has the ability to read or modify arbitrary data on the system, gain low-level control of the hardware, etc. All software is unprivileged; the concept of "root" or "kernel mode" simply does not exist so there is no possibility of malicious software achieving such capabilities.

The prototype Antikernel system was written in a mixture of Verilog, C, and MIPS assembly language for the actual operating system, plus a large body of C++ in debug/support tools which are used for development but do not actually run on the target system. The prototype was verified with a combination of simulation (Xilinx ISim), formal model checking (using the MiniSAT solver integrated with yosys), and hardware testing (using a batch processing cluster consisting of Xilinx Spartan-3A, Spartan-6, Artix-7, and Kintex-7 FPGAs).

Supplemental Files

Some files may require a special program or browser plug-in. More Information

Indexing (document details)
Advisor: Yener, Bulent
Commitee: Carothers, Christopher D., McDonald, John F., Szymanski, Boleslaw K.
School: Rensselaer Polytechnic Institute
Department: Computer Science
School Location: United States -- New York
Source: DAI-B 76/10(E), Dissertation Abstracts International
Subjects: Computer Engineering, Electrical engineering, Computer science
Keywords: Embedded systems, Hardware acceleration, Network on chip, Operating systems, Security, System on chip
Publication Number: 3705663
ISBN: 9781321789836
Copyright © 2019 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy