Programmable Hardware Support for Ubiquitous Micro-Policy Enforcement
Presented as part of the 2014 HCSS conference.
Abstract:
A host of security vulnerabilities arise from the violation of known, but in-practice unenforceable, safety and security policies, including high-level programming models and critical invariants of low-level programs. The onus is on every programmer to ensure that the entire system — every line of code — is free from vulnerabilities and exploitable errors, and remains that way as each feature is added and bug patched. Unlike safety-critical physical systems (cars, airplanes, chemical processing plants) that guard against life-threatening failures using redundant fail-safe mechanisms, present-day computer systems lack supervising safety interlock mechanisms to help prevent catastrophic failures that arise from violation of known safety and security policies.
This talk will demonstrate how a rich and valuable set of low-level micro-policies can be enforced at the hardware instruction-set level to provide such safety interlocks with modest performance impact. The enforcement of these micro-policies provides more secure and robust macro-scale behavior for our computer systems.
Specifically, we describe work developed in the context of the DARPA CRASH/SAFE project,1 and plans for follow-on efforts, to (i) introduce an architecture for ISA-level micro-policy enforcement; (ii) develop a linguistic framework for formally defining micro-policies; (iii) identify and implement a diverse collection of useful micro-policies; (iv) verify, through a combination of rigorous testing and formal proof, that combinations of hardware and software handlers correctly implement the desired policies and that the policies imply specific high-level safety and security properties; and (v) elaborate a microarchitecture to provide hardware support with low performance overhead and acceptable resource costs. We demonstrate how emerging hardware capabilities and advances in formal specification and verification can be combined to make it tractable to engineer systems with strong security and safety properties. We combine ideas from programming languages, verification, language-based security, hardware design, and microarchitectural optimization to provide a clean model for capturing policies and efficient mechanisms for implementing them.
Our proposed talk directly addresses the Requirements and Specifications topic of HCSS by emphasizing the formal specification and verification of our generic hardware and software mechanisms as well as specific micro-policies. Furthermore, it addresses the Designed-In Security theme, de- scribing how to support ubiquitous policy enforcement at the lowest levels of the hardware/software stack. Our ubiquitous enforcement guarantees that key security behavior is enforced even when the code contains errors and vulnerabilities. Since the policies are separate from the code, their enforcement is guaranteed as the code evolves during its lifetime.
---
1http://www.crash-safe.org
Presenter Bio:
Benjamin Pierce is Henry Salvatori Professor of Computer and Information Science at the University of Pennsylvania and a Fellow of the ACM. His research centers on programming languages, static type systems, language-based security, computer-assisted proof, concurrent and distributed programming, and synchronization technologies. His books include the widely used graduate texts Types and Programming Languages and Software Foundations. He serves as co-Editor in Chief of the Journal of Functional Programming, as Managing Editor for Logical Methods in Computer Science, and as editorial board member of Mathematical Structures in Computer Science and Formal Aspects of Computing. He is also the lead designer of the popular Unison file synchronizer.