|
Current cybersecurity practice is inadequate to defend against the security threats faced by society. Unlike physical systems, present-day computers lack supervising safety interlocks to help prevent catastrophic failures. Worse, many exploitable vulnerabilities arise from the violation of well-understood safety and security policies that are not enforced due to perceived high performance costs. This project aims to demonstrate how language design and formal verification can leverage emerging hardware capabilities to engineer practical systems with strong security and safety guarantees. The ultimate goal is to strengthen the security foundation upon which today's information-based society is built, thereby improving national security by providing capabilities to protect critical infrastructure from misuse and cyber-attack, as well as protecting individual privacy and reducing opportunities for cyber-muggings.
A rich set of micro-policies - instruction-level security monitoring mechanisms based on fine-grained metadata tags - can be described as instances of a common dynamic monitoring framework, formalized and reasoned about with unified verification tools, and efficiently implemented using programmable metadata-propagation hardware. Specific project contributions include (1) a linguistic framework for defining and combining micro-policies, with a verified compiler and a framework for carrying out machine-checked proofs of key security properties; (2) architectural extensions and microarchitectural optimizations for micro-policy enforcement in hardware with low performance overhead and acceptable resource costs; and (3) applications of the micro-policy language, proof framework, and hardware support to implement, verify, and evaluate a number of concrete micro-policies on realistic application workloads.
|
TWC: Medium: Micro-Policies: A Framework for Tag-Based Security Monitors