Abstract
This dissertation is a continuation of an Air Force Research Laboratory (AFRL) project focused on the development of a new security tagged microprocessor architecture and a supporting operating system. Security tagging schemes are promising mechanisms for enhancing the security of computer systems. The idea behind security tagging schemes is to attach metadata tags to memory and registers to carry information about the data. These tags are then used to protect the system and user software from security attacks and invalid information access. Research has shown that tagging schemes can be used to enhance the traditional protection mechanisms of microprocessors, going beyond basic memory management and supervisor/user mode (and even beyond protection rings). This dissertation summarizes the major security tagging schemes proposed in recent years, introduces a security tagging scheme, and proposes new research to implement, evaluate and improve the security tagging scheme.
The AFRL project used the open source Real-Time Executive for Multiprocessor Systems (RTEMS), a single-user and multi-threaded runtime executive as the base operating system in the security tagged architecture. Therefore, the design of the new security tagging scheme addressed key features of RTEMS that required modification in order to provide enhanced security. The tag checking and propagation rules are designed for both C language level and assembly instruction level programs. A SPARC instruction simulator has been improved to simulate instruction execution as well as tag checking and propagation. To ensure tagging rules were properly designed and that tag propagations were implemented correctly, several test cases were developed. In addition, RTEMS was expanded from a single user system to a multiuser system, and an advanced tagging scheme was designed to support multiple users. Lastly, this dissertation presents a discussion of a formal model of the security policy enforced by the tagged system and proves security properties of the proposed formalization.