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.