Micro-Policies: A Framework for Tag-Based Security Monitors

Опубликовано 22 июня 2016, 2:43

Current cybersecurity practice is inadequate to defend against the threats faced by society. A host of vulnerabilities arise from the violation of known—but not enforced—safety and security policies, including both high-level programming models and critical invariants of low-level programs. Unlike safety-critical physical systems (cars, airplanes, chemical processing plants), present-day computers lack supervising safety interlocks to help prevent catastrophic failures. We argue that 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 computer systems. We describe work originating in the DARPA CRASH/SAFE project (www.crash-safe.org) to (1) introduce an architecture for ISA-level micro-policy enforcement; (2) develop a linguistic framework for formally defining micro-policies; (3) identify and implement a diverse collection of useful micro-policies; (4) 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 (5) microarchitecture to provide hardware support with low performance overhead and acceptable resource costs. Thus, emerging hardware capabilities and advances in formal specification and verification combine to enable engineering systems with strong security and safety properties.