当前,计算机体系结构的安全问题给我们带来了巨大的风险和挑战。本文在介绍现有方法的基础上,探讨计算机尤其是硬件工作者需要探索的方向。
关键词:计算机系统安全
当前,计算机体系结构的安全问题给我们带来了巨大的风险和挑战。本文在介绍现有方法的基础上,探讨计算机尤其是硬件工作者需要探索的方向。
许多现存的商业操作系统存在广泛的漏洞。MITRE常见软件安全漏洞存储库(CVEs:http://cve.mitre.org)目前已披露超过11万个公开的漏洞,这还未包含已经解决的漏洞以及未来可能发现或者未曝光的漏洞。此外,每天还会有约50个新的漏洞被曝出。一方面,从业人员的修补速度完全跟不上漏洞出现的速度;另一方面,芯片修补可能需要数年的时间成本以及数十亿美元的经济成本。因此,补丁式的防御会使攻防均衡的天平逐渐向对攻击方有利的方向倾斜。
最近的研究,诸如seL4微内核[9]、CertiKOS虚拟机层次结构[7]以及CompCert验证编译器[11]等,已经在操作系统内核正确性的形式化证明方面做出了重大贡献。它们的证明依赖于可信的架构抽象模型——硬件/软件接口,以及最近发展的模型[1, 6]。虽然上述技术尚未普及,但它们为证明系统免受大量攻击提供了可能。
最近出现的漏洞都说明我们的防御理念存在落后之处。换句话说,是对处理器的底层了解不够深入。主要表现有三个方面。首先,处理器硬件(通常已经过大量验证)长期以来被认为能为软件提供坚实的基础,但其上出现的越来越多的漏洞充分驳斥了这一观点。其次,日益复杂的系统以及多供应商的硬件构成方式意味着人们不能局限于单处理器架构的思考,我们需要以全面的角度来了解这种形势下的处理器的复杂性。最后一点也是最为严重的问题:这些新型攻击突破了传统的架构抽象。传统的抽象仅描述了硬件实现允许的功能性行为,这种灵活的设计对性能优化至关重要,但攻击利用的恰恰是性能差异化所带来的细微信息流。如缓存和推测执行,这些微架构创新在过去几十年里为我们提供了更快的运算能力,却导致了侧信道攻击(side-channels)。
理想情况下,安全应当是自下而上构建的。那么我们应当如何构建硬件的安全基础来解决安全问题呢?
多年来,许多从业人员认为硬件安全仅意味着保证物理层的安全。例如,功耗/电磁侧信道和故障注入通过操纵芯片的物理特性实现来提取加密密钥。但物理层的防护并不完备,新一轮的攻击意味着还有更多不同而有效的媒介可以利用。
物理层安全社区的失败表明了实现(implementation)是至关重要的。在实现过程中,开发人员首先利用硬件定义语言(HDL)实现库逻辑单元之间的连接,然后完成逻辑单元布局、布线以及芯片层设计。这一过程自HDL源、编译器,到单元晶体管定义、布线、功耗、热学,电磁学、掺杂剂浓度和晶格的任何层次的微小失误都可能导致潜在的可被利用的故障。与审查恶意软件的二进制代码不同,许多细微的物理特性难以被检测到。因此,系统更容易受到设计错误和供应链攻击的影响。
最近的研究已经表明侧信道攻击正具有越来越大的危害。传统的物理层侧信道攻击本质上是对信号噪声的处理,攻击者在追踪到足够的功耗使用记录后,就能够通过强大的数据分析能力提取密钥。相比之下,架构层的侧信道攻击具有更高的带宽和更好的信噪比。
从面向系统的角度来看,上述问题表明整体往往会比其各组成部分的总和更糟糕。不同组件构成的系统以及多重的供应商使得各部件实际获得的授权要比实现其目的所需的资源更多,这给了攻击者无限可能。例如,谷歌ProjectZero团队完成了对iPhone内部Broadcom Wi-Fi芯片的攻击,攻击者从恶意的Wi-Fi数据包跳转,并在Wi-Fi芯片上安装恶意代码,从而在应用处理器上攻陷iOS[4]。使用Wi-Fi芯片作为跳板使得攻击更为有效,而且这种组合性的攻击行为极难被识别[5]。组合性攻击具备极大的灵活性,可以使用意外的连接构造新型侧信道,例如,通过共享I2C总线和以太网控制器发送网络数据包的内存DIMM[16]。
硬件工程师经常讨论在物理实现过程加入“寄生”(非设计布置)电阻或者电容,实际上它们对于信号和功耗吸收并没有那么理想。当下,带有“寄生”组件的计算机有很多,这些组件具备意想不到的计算能力,例如x86页面故障处理器[2]可以转换为DMA控制器[15]。这对于全面理解计算发生的位置提出了挑战,例如什么是软件而不是硬件。
全系统的保护策略是至关重要的(参见Bellovin[3])。物理层攻击带给我们的另一个启示就是,多层次的保护策略使其威胁性大为降低。例如,利用激光故障注入从银行卡中提取密钥并没有意义,攻击者还需要利用它来窃取金钱。然而,银行的安防系统如交易限制、欺诈检测会拦截这一行为。此外,该密钥仅涉及一个账户而非全部用户,加上权限分级,限制了攻击行为的收益,使其在经济上不可行。
另一种可行的方法是提供更为丰富的上下文信息,以允许硬件理解和实施安全属性。目前有团队正在设计、开发和形式化分析CHERI硬件指令集架构[20],以及CHERI操作系统和应用程序的安全性。CHERI ISA使硬件能够提供指针出处保护,对虚拟内存进行任意粒度的访问控制以及抽象系统对象,并能实现粗、细粒度的分区。上述措施可以提供增强的隔离和可控的共享,允许可信和不可信的软件(包括未修改的遗留代码)安全地共存。由于硬件具有对指针和分区等软件概念的认知,因此可以起到保护作用,并且我们可以确保这种保护的有效性,例如,对架构抽象和对特定安全属性的增强进行形式化证明。我们相信CHERI系统架构具有提供前所未有的全系统可信的巨大潜力,包括防御某些未知的侧信道攻击[19]。
上述类型的架构保证可以使当前不安全的语言(例如C / C ++)更安全地实现,并且可以在安全硬件的基础上提供安全可证的操作系统内核。类似的设计可以应用于其他领域,例如片上系统的易受攻击的组件之间。
设计这样的系统需要更全面的视野,更注重硬件、操作系统和应用程序之间紧密的相互作用。此外还需要设计师更多地了解其上层和下层的运作机制。更好的架构模型可以更鲁棒地验证安全属性,跨项目地分摊验证成本,这对于抵御攻击极其有利。但此类验证必须具有包容性,即能测试系统的所有方面,包括实现定义行为的边界。
更好的验证可以保护系统免受基于其抽象模型中存在的新漏洞的影响,但不能防御那些涉及未建模场景的漏洞。一个值得继续探索的问题是,架构规范和完整的硬件实现之间是否存在理想的抽象,可以帮助我们充分推断潜在的泄露,而不会太过复杂难以处理。
传统的、紧密层约束的自由设计理念已经不适合处理安全问题。硬件/软件系统安全架构设计师需要更好地了解其上层和下层的运作机制,确定这些层次组合的相互作用所带来的影响。管理系统整体的复杂性必须获取可能与安全性分析相关的全部信息,尤其是关于全新类别漏洞的信息。防御的战役才刚刚开始。
A.西多·马克托斯(A. Theodore Markettos) 剑桥大学计算机科学与技术系高级研究员。theo.markettos@cl.cam.ac.uk
罗伯特·N.M.沃森(Robert N.M. Watson) 剑桥大学计算机科学与技术系高级讲师。robert.watson@cl.cam.ac.uk
西蒙·W.摩尔(Simon W. Moore) 剑桥大学计算机科学与技术系计算机工程教授。simon.moore@cl.cam.ac.uk
其他作者:彼得·休厄尔(Peter Sewell),彼得·G.诺伊曼(Peter G. Neumann)
苑风凯
CCF专业会员。中国科学院信息工程研究所助理研究员。主要研究方向为计算机安全体系结构。
yuanfengkai@iie.ac.cn
侯锐
CCF专业会员、体系结构专委会委员。中国科学院信息工程研究所研究员,信息安全国家重点实验室副主任。主要研究方向为计算机体系结构、处理器芯片设计与安全、数据中心服务器架构、AI安全。
hourui@iie.ac.cn
[1]Armstrong, A. et al. ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS. In Proceedings of the Principles of Programming Languages Conference (POPL) 2019.
[2]Bangert, J. et al. The page-fault weird machine: Lessons in instruction-less computation. In Proceedings of the USENIX Workshop on Offensive Technologies (WOOT), 2013.
[3]Bellovin, S.M. and Neumann, P.G. The big picture: A systems-oriented view of trustworthiness. Commun.ACM 61, 11 (Nov. 2018), 24–26.
[4]Beniamini, G. Over The Air: Exploiting Broadcom’s Wi-Fi Stack; https://bit.ly/2oA6GJL
[5]Gerber, S. et al. Not your parents’ physical address space. In Proceedings of the Hot Topics in Operating Systems Conference (HotOS-XV) 2015.
[6]Goel, S., Hunt, W.A. Jr., and Kaufmann, M. Engineering a formal, executable x86 ISA simulator for software verification. Provably Correct Systems (ProCoS), 2017.
[7]Google Project Zero, 2018; https://bit.ly/2CAQzTMGu, R. et al. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. OSDI 2016, 653–669; See also https://bit.ly/2Uzj9sI for ongoing work.
[8]Islam, S. et al. SPOILER: Speculative Load Hazards Boost Rowhammer and Cache Attacks, arXiv e-prints (Mar. 1, 2019); https://bit.ly/2TxWdhk
[9]Klein, G. et al. Comprehensive formal verification of an OS microkernel. ACM Trans. Computer Systems 2014; See also https://bit.ly/2UPKgEY for ongoing work.
[10]Kocher, P. et al. Spectre attacks: Exploiting speculative execution. ArXiv e-prints (Jan. 2018); https://bit.ly/2lUpJLk
[11]Leroy, X. A formally verified compiler back-end. Journalof Automated Reasoning 43, 4 (2009), 363–446.
[12]Lipp, M. et al. Meltdown, 2018; https://bit.ly/2E6myYl
[13]Markettos, A.T. Making sense of the Supermicro motherboard attack; https://bit.ly/2PqOnld
[14]Markettos, A.T. et al. Thunderclap: Exploring vulnerabilities in operating system IOMMU protection via DMA from untrustworthy peripherals. In Proceedings of the Network and Distributed Systems Security Symposium (NDSS), (Feb. 2019).
[15]Rushanan, M. and Checkoway, S. Run-DMA. In Proceedings of the WOOT 2015 Conference. (2015).
[16]Sutherland, G. Secrets of the motherboard ([sh*t] my chipset says). In Proceedings of the 44CON 2017,(Sept. 2017).
[17]Van Bulck, J. et al. Foreshadow: Extracting the keys to the Intel SGX kingdom with transient out-of-order execution. USENIX Security (Aug. 15–17, 2018); https://bit.ly/2DusEDT
[18]Watson, R.N.M. et al. Capability Hardware Enhanced RISC Instructions (CHERI): Notes on the Meltdown and Spectre Attacks. Technical Report UCAMCL-TR-916, University of Cambridge, Computer Laboratory (Feb. 2018); https://bit.ly/2DuVDrr
[19]Watson, R.N.M. et al. Capability Hardware Enhanced RISC Instructions (CHERI): CHERI Instruction-set Architecture, Version 7, Technical Report UCAMCL-TR-927, University of Cambridge, Computer Laboratory (Apr. 2019); https://bit.ly/2XzPgKU
[20]Weisse, O. et al. Foreshadow-NG: Breaking the virtual memory abstraction with transient out-of-order execution (Aug. 2018); https://bit.ly/2VZLD0h
* 本文译自Communications of theACM, “Through Computer Architecture, Darkly”, 2019,62(6): 25~27。
(本期译文责任编委:李超)
CCF推荐
【精品文章】
点击“阅读原文”,前往CCF数图相关栏目。