SCorCH: Secure Code for 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.