This project is motivated by the fundamental question of whether it is possible to achieve verifiable end-to-end security properties by adding suitable security mechanisms on top of commercially available applications executing on an untrusted computing platform. A concrete example of such a scenario is provided by a user interacting with a bank's web server using a web browser running SSL. An important end-to-end security property in this context is protecting the confidentiality and integrity of the exchanged information and the user's password from malware and insider attacks on the local machine or the bank's server, as well as an active adversary trying to compromise the network communication. The untrusted computing platform here is the user's machine, which is running a commodity OS such as Windows or Linux and applications such as Internet Explorer or Firefox.
We believe that this goal can be achieved if one takes the approach of (1) minimizing the liability of security-property proof based on differentiated application services, and well-defined, useful properties of security-sensitive code, and (2) supporting the identified and proved properties by a security architecture that is compatible with commercially available platforms. Our system architecture includes novel components (e.g. trusted paths to local and remote security sensitive code) and integrates existing technologies (e.g., hypervisors, isolated execution environments) in a way that minimizes the size of both system and security-sensitive application code, thus enabling formal verification.
The project will provide extensive educational opportunities for undergraduate and graduate students; research results will be integrated into courses at CMU and disseminated via technical publications, student internships, the CyLab Industrial Partners program, and the CMU Women@SCS roadshow program.
To be useful in practice, security primitives must be available on commodity computers with demonstrable assurance and be understandable by ordinary users with minimum effort. The working hypothesis of this project was that traditional trusted systems comprising a reference monitor and layered operating system services that are formally verified, while useful for a few niche application areas, will continue to fail these criteria for commodity computers. In particular, commodity operating systems will continue to be untrustworthy; i.e., they will lack demonstrable properties and support only low-assurance services. Hence, this project was motivated by the fundamental question of whether it is possible to achieve verifiable security properties by adding suitable security mechanisms to unmodified commodity systems and untrusted applications. This project represents a fundamental shift in the design of systems with demonstrable security properties. For nearly four decades, most researchers assumed that all security properties must be implemented layer-by-layer from the ground up, starting with a reference monitor. The reference monitor identifies all system subjects and objects, is isolated from external attacks, is always invoked for every subject reference to any object, and hence enforces a system's security policy. The reference monitor is supposed to be small and simple enough to enable correctness verification via formal proofs and hence provides high assurance of correct implementation of security properties. Furthermore, most researchers assumed that full operating system layering is also essential for verifiable security properties of applications. In contrast with these long-standing assumptions, this project showed that it is possible to add non-virtualizing, micro-hypervisors to unmodified, untrustworthy commodity (i.e., low-assurance) operating systems. These micro-hypervisors enable the creation of isolated execution environments for application modules with verifiable security properties. In contrast with traditional hypervisors, our micro-hypervisors (e.g., TrustVisor, XMHF) do not virtualize hardware; e.g., they do not include scheduling or multiplexing operations. Hence, they are much simpler than all virtualizing hypervisors/VMMs, other recent micro-hypervisor designs, and past security kernels. As a consequence, we are able to verify micro-hypervisor security properties, and compose them with the higher level properties of isolated application modules. In addition, we are able to show that our micro-hypervisors can support higher level security primitives in a verifiable manner; i.e., trusted path to/from isolated application modules, and application level micro-kernels that implement verifiable services for isolated application modules. As a result, trustworthy software components can be supported for security-sensitive applications running on top of unmodified commodity operating systems. Hence, restructuring commodity operating systems to implement native security kernels and fully layered services becomes unnecesary for most security-sensitive applications. In addition, we investigated various mechanisms for the trusted boot of micro-hypervisor software, and the establishment of both hardware-based and software-based root of trust. Finally, we explored the use of micro-hypervisors to support security properties of network protocols. The impact of this project reached beyond numerous publications in leading security conferences. For example, our reseach helped produce a micro-hypervisor development framework, called the XMHF, which is now available as open-source code. Our micro-hypervisor designs have been used by industry research efforts, including at Northrop Grumman, Lockheed Martin, and Intel. Our software root of trust technology is also being used in other research projects; e.g., DARPA VET and General Motors Co. Our research on the foundations of trust in networks of humans and computers is the basis for an upcoming DARPA ISAT. From an educational perspective, this project helped us develop several modules for graduate courses, including one on architectures for secure systems and another on formal verification of hypervisor properties. The project findings also contributed to the development of a multi-year capacity-building program designed to increase the skills of faculty in minority (e.g., HBCU) institutions, and to a summer school on trustworthy computing attended by over a hundred graduate students and expert speakers from academia, industry, and government between 2009 and 2011. From a human resource development perspective, our project supported six PhD students who have graduated or will graduate soon, and three post-doctoral researchers, all of whom are now working in leading US research laboratories (e.g., Microsoft, Google) or universities (e.g., Stanford, CMU).
