Projects per year
In this paper we show how more rigorous engineering methods can be applied to the development of a new security-enhanced processor architecture, with its accompanying hardware implementation and software stack. We use formal models of the complete instruction-set architecture (ISA) at the heart of the design and engineering process, both in lightweight ways that support and improve normal engineering practice – as documentation, in emulators used as a test oracle for hardware and for running software, and for test generation – and for formal verification. We formalise key intended security properties of the design, and establish that these hold with mechanised proof. This is for the same complete ISA models (complete enough to boot operating systems), without idealisation.
We do this for CHERI, an architecture with hardware capabilities that supports fine-grained memory protection and scalable secure compartmentalisation, while offering a smooth adoption path for existing software. CHERI is a maturing research architecture, developed since 2010, with work now underway on an Arm industrial prototype to explore its possible adoption in mass-market commercial processors. The rigorous engineering work described here has been an integral part of its development to date, enabling more rapid and confident experimentation, and boosting confidence in the design.
|Title of host publication||2020 IEEE Symposium on Security and Privacy (SP)|
|Place of Publication||San Francisco, CA, USA|
|Publisher||Institute of Electrical and Electronics Engineers (IEEE)|
|Number of pages||18|
|Publication status||Published - 30 Jul 2020|
|Event||41st IEEE Symposium on Security and Privacy - The Hyatt Regency, San Francisco, United States|
Duration: 18 May 2020 → 20 May 2020
Conference number: 41
|Conference||41st IEEE Symposium on Security and Privacy|
|Abbreviated title||SP 2020|
|Period||18/05/20 → 20/05/20|