SCorCH: Secure Code for Capability Hardware

计算机和智能手机现在被用于日常生活的各个领域，从商业到教育再到娱乐。从个人到国家层面，我们已经变得依赖软件系统，如果这些系统出现故障或其安全受到威胁，我们将面临重大损失。防止这种情况的唯一方法是确保软件没有固有的弱点，这要求我们使用数学的力量来确保软件既安全又安全。随着软件系统变得越来越复杂，故障的可能性也越来越大。传统的测试方法变得不可扩展，并且对软件系统的安全性提供的保证较弱。同样，我们的软件系统也越来越多地受到一些人的攻击，这些人试图利用我们对技术的依赖来达到他们自己的邪恶目的。这些所谓的网络攻击正变得更加复杂，积极寻求颠覆现有的检测方法。只有消除潜在的弱点，我们才能真正保护自己。因此，正确处理安全和安全的概念，必须着眼于软件系统的基本属性，并对其进行一般性的推理。然而，软件系统并不是孤立的，它们与其他软件一起运行在硬件上，任何软件的安全和保障都依赖于这种背景。理想情况下，从分号到硅码，我们都有安全保障。ARM和剑桥大学最近的一项努力，为安全系统引入了一种新的模式：能力硬件。最重要的一组安全漏洞源于不应允许访问或操作该内存的进程访问或操作该内存。能力硬件背后的想法是通过特殊的所谓能力在硬件级别提供安全保证，这是一种特殊类型的内存，它知道谁被允许使用它做什么。其结果应该是更加安全和健壮的软件系统。然而，现在我们在硬件层面上有了更多的安全性，关键是我们确保在软件层面上正确地利用这一点。这个项目旨在将软件验证方面的实质性先进成果转移到这个新功能硬件的设置中。一般而言，我们将扩展现有工具，并创建能够对运行在功能硬件上的工业相关软件系统的安全性和安全性进行推理的新工具。将把重点放在实现高度的技术准备上，确保当国际社会准备接受能力硬件时，已经有一套成熟的工具能够核实其上软件的安全性和保障。

Computers and smart phones are now used in all areas of everyday life, from business to education to entertainment. From the individual to the national level, we have become reliant on software systems and risk substantial loss if these systems fail or have their security compromised. The only way to protect against this is to ensure that the software has no inherent weakness, and this requires that we use the power of mathematics to ensure that the software is both safe and secure.As software systems grow more complex the potential for failure grows. Traditional testing approaches become unscalable and give weaker assurances about the safety of software systems. Similarly, our software systems are increasingly subject to attacks from those who seek to exploit our dependence on technology for their own nefarious purposes. These so-called cyber attacks are becoming more elaborate, actively seeking to subvert existing methods of detection. Only by removing the underlying vulnerabilities we can truly protect ourselves. Therefore, to properly handle notions of safety and security we must focus on fundamental properties of software systems and reason about them generally.However, software systems are not isolated, they run on hardware alongside other software and the safety and security of any software is dependent on this context. Ideally, we have safety and security `all the way down' from semicolons to silicon. A recent effort, let by ARM and the University of Cambridge, has introduced a new model for safe and secure systems: Capability Hardware. The most significant set of security vulnerabilities stem from memory being accessed or manipulated by a process that should not be allowed to access or manipulate that memory. The idea behind Capability Hardware is to provide security guarantees at the hardware level with special so-called capabilities, a special kind of memory that knows who is allowed to do what with it. The result should be much more secure and robust software systems. However, now that we have more security at the hardware level, it is key that we ensure that this is correctly utilised at the software level.This project aims to transport the substantial advanced in software verification to the setting of this new capability hardware. In general, we will extend existing tools and create new tools able to reason about the safety and security of industrially relevant software systems running on Capability Hardware. There will be a significant focus on achieving high technological readiness, ensuring that when the international community is ready to embrace Capability Hardware there already exists a mature set of tools able to verify the safety and security of the software sitting on top of it.