SCorCH: Secure Code for Capability Hardware

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

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.