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

TWC：中：微观策略：基于标签的安全监视器框架

• 批准号: 1513854
• 负责人: Benjamin Pierce
• 金额: $ 120万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-09-01 至 2021-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1513854&HistoricalAwards=false
• 关键词: TWC; Medium; Micro; Policies; Framework

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.

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