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.
CT-M: Realizing Verifiable Security Properties on Untrusted Computing Platforms