High-assurance systems are used in areas critical to human life and welfare, such as avionic, military, financial, and medical systems. Because of the high cost of failure, e.g., financial disaster or loss of life, these systems have stringent requirements about both secrecy (guarantees that private information cannot be made public) and integrity (guarantees that un trusted information cannot corrupt trusted systems). In order to meet these requirements, the underlying computer hardware on which these systems are run must itself be verifiably secure using the same criteria. In addition, the hardware must also be efficient, able to run the systems with sufficiently high performance to be practical.
The goal of this research is to create computer hardware for high-assurance systems that is verifiably secure (that is, provably meets the requirements for secrecy and integrity) while remaining highly efficient. The unique approach taken is to leverage techniques from the programming languages community (e.g., advanced type systems) to create a new hardware description language called Caisson that enables hardware designers to quickly and easily create hardware systems that are provably secure by construction. If a system is designed using Caisson, then it is necessarily secure. Caisson will be used to explore the space of secure hardware designs in order to develop systems that are efficient as well as secure. On a broad scale, the fruits of this research will be a large step towards a safer digital domain, safeguarding the integrity of our financial system, the privacy of our medical records, and the safety of our transportation infrastructure.
