Verified Security for the Morello Capability-enhanced Prototype Arm Architecture
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture
复制标题
Morello 功能增强原型 Arm 架构的安全性经过验证
DOI：
10.1007/978-3-030-99336-8_7
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Peter Sewell
中科院分区：
文献类型：
--
作者：
Thomas Bauereiß;Brian Campbell;Thomas Sewell;A. Armstrong;Lawrence Esswood;I. Stark;Graeme Barnes;R. Watson;Peter Sewell
，Abstract.内存安全漏洞仍然是我们关键基础设施安全漏洞的主要来源。CHERI项目建议通过硬件支持的功能扩展传统架构，以实现细粒度的内存保护和可扩展的分区，允许历史上内存不安全的C和C++进行调整，以确定性地减轻大类漏洞，同时只需要对现有系统软件源进行微小的更改。Arm目前正在设计和构建Morello，这是一个支持CHERI的原型架构、处理器、SoC和电路板，扩展了高性能Neoverse N1，以实现对CHERI的工业评估，并为潜在的大众市场采用铺平道路。然而，对于这样一个主要的新的面向安全的架构功能，重要的是要建立高度的信心，它确实提供了预期的保护，而这是传统的工程技术无法做到的。在本文中，我们从一开始就将Morello架构置于坚实的数学基础上。我们定义了Morello旨在提供的基本安全属性，可达能力单调性，并证明架构定义萨蒂斯它。该证明在Isabelle/HOL中机械化，并适用于Morello配置集架构（伊萨）的专用Arm规范到Isabelle的翻译。主要的挑战是处理生产架构的复杂性和规模：62，000行规格，转换为210，000行Isabelle。我们通过一个狭窄的抽象来分解证明，这个抽象捕捉了任意CHERI ISA的基本属性，更广泛的CHERI和Morello团队，他们的工作使Morello成为现实。这项工作是由英国工业战略挑战基金（ISCF）的数字安全设计（DSbD）计划，提供DSbDtech启用的数字平台（补助金105694），EPSRC计划补助金EP/K 008528/1 REMS，ERC AdG 789108 ELVER，Arm iCASE奖，EPSRC IAA KTF基金，艾萨克·牛顿信托基金，英国高等教育创新基金（HEIF），Thales E-Security，微软研究院剑桥、Arm、谷歌、谷歌DeepMind、惠普企业和盖茨剑桥信托基金。批准公开发行;发行不受限制。这项工作得到了国防高级研究计划局（DARPA）和研究实验室（AFRL）的支持，合同编号为FA 8750 -10-C-0237（“CTSRD”）、FA 8750 -11-C-0249（“MRC 2”）、HR 0011 -18-C-0016（“ECATS”）和FA 8650 -18-C-7809（“CIFV”），是DARPA CRASH、MRC、SSITH研究项目。本报告所载的观点、意见和/或发现均为作者的观点、意见和/或发现，不应被解释为代表美国国务院或美国政府的官方观点或政策。
, Abstract. Memory safety bugs continue to be a major source of security vulnerabilities in our critical infrastructure. The CHERI project has proposed extending conventional architectures with hardware-supported capabilities to enable fine-grained memory protection and scalable compartmentalisation, allowing historically memory-unsafe C and C++ to be adapted to deterministically mitigate large classes of vulnerabilities, while requiring only minor changes to existing system software sources. Arm is currently designing and building Morello, a CHERI-enabled prototype architecture, processor, SoC, and board, extending the high-per-formance Neoverse N1, to enable industrial evaluation of CHERI and pave the way for potential mass-market adoption. However, for such a major new security-oriented architecture feature, it is important to establish high confidence that it does provide the intended protections, and that cannot be done with conventional engineering techniques. In this paper we put the Morello architecture on a solid mathematical footing from the outset. We define the fundamental security property that Morello aims to provide, reachable capability monotonicity, and prove that the architecture definition satisfies it. This proof is mechanised in Isabelle/HOL, and applies to a translation of the official Arm specification of the Morello instruction-set architecture (ISA) into Isabelle. The main challenge is handling the complexity and scale of a production architecture: 62,000 lines of specification, translated to 210,000 lines of Isabelle. We do so by factoring the proof via a narrow abstraction capturing essential properties of arbitrary CHERI ISAs, the wider CHERI and Morello teams, for their work to make Morello a reality. This work was by the UK Industrial Strategy Challenge Fund (ISCF) the Digital Security by Design (DSbD) Programme, to deliver a DSbDtech enabled digital platform (grant 105694), EPSRC programme grant EP/K008528/1 REMS, ERC AdG 789108 ELVER, Arm iCASE awards, EPSRC IAA KTF funds, the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), Thales E-Security, Microsoft Research Cambridge, Arm, Google, Google DeepMind, HP Enterprise, and the Gates Cambridge Trust. Approved for public release; distribution is unlimited. This work was supported by the Defense Advanced Research Projects Agency (DARPA) and the Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”), FA8750-11-C-0249 (“MRC2”), HR0011-18-C-0016 (“ECATS”), and FA8650-18-C-7809 (“CIFV”), as part of the DARPA CRASH, MRC, and SSITH research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies of the Department of or the U.S. Government.
CHERI Concentrate：实用的压缩功能
影响因子：
3.7
作者：
Woodruff J
通讯作者：
Woodruff J
影响因子：
1.8
作者：
Armstrong, Alasdair;Bauereiss, Thomas;Sewell, Peter
通讯作者：
Sewell, Peter
Isla：集成完整的 ISA 语义和公理并发模型（扩展版本）
影响因子：
0.8
作者：
Armstrong A
通讯作者：
Armstrong A