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

目前的网络安全实践不足以抵御社会面临的安全威胁。与物理系统不同，现代计算机缺乏监督安全联锁来帮助防止灾难性故障。更糟糕的是，许多可利用的漏洞是由于违反了众所周知的安全和安全策略而产生的，这些安全和安全策略由于感知到的高性能成本而没有实施。该项目旨在展示语言设计和形式验证如何利用新兴的硬件功能来设计具有强大安全性和安全保证的实用系统。 最终目标是加强当今信息社会赖以建立的安全基础，从而通过提供保护关键基础设施免遭滥用和网络攻击的能力，改善国家安全，以及保护个人隐私和减少网络抢劫的机会。一组丰富的微观策略-基于细粒度元数据标签的防御级安全监控机制-可以被描述为通用动态监控框架的实例，使用统一的验证工具进行形式化和推理，并使用可编程元数据传播硬件有效地实现。具体的项目贡献包括：（1）一个用于定义和组合微策略的语言框架，以及一个经过验证的编译器和一个用于对关键安全属性进行机器检查证明的框架;（2）用于在硬件中执行微策略的体系结构扩展和微体系结构优化，性能开销低，资源成本可接受;以及（3）微策略语言、证明框架和硬件支持的应用，以在实际应用工作负载上实现、验证和评估多个具体的微策略。

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.