Show simple item record

dc.contributor.authorNienhuis, K
dc.contributor.authorJoannou, A
dc.contributor.authorBauereiss, T
dc.contributor.authorFox, A
dc.contributor.authorRoe, M
dc.contributor.authorCampbell, B
dc.contributor.authorNaylor, M
dc.contributor.authorNorton, RM
dc.contributor.authorMoore, SW
dc.contributor.authorNeumann, PG
dc.contributor.authorStark, I
dc.contributor.authorWatson, RNM
dc.contributor.authorSewell, P
dc.date.accessioned2020-02-22T00:31:22Z
dc.date.available2020-02-22T00:31:22Z
dc.date.issued2020
dc.identifier.isbn9781728134970
dc.identifier.issn1081-6011
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/302580
dc.description.abstractThe root causes of many security vulnerabilities include a pernicious combination of two problems, often regarded as inescapable aspects of computing. First, the protection mechanisms provided by the mainstream processor architecture and C/C++ language abstractions, dating back to the 1970s and before, provide only coarse-grain virtual-memory-based protection. Second, mainstream system engineering relies almost exclusively on test-and-debug methods, with (at best) prose specifications. These methods have historically sufficed commercially for much of the computer industry, but they fail to prevent large numbers of exploitable bugs, and the security problems that this causes are becoming ever more acute. 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 \emph{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.
dc.description.sponsorshipThis work was supported by EPSRC programme grant EP/K008528/1 (REMS: Rigorous Engineering for Mainstream Systems). This work was supported by a Gates studentship (Nienhuis). This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement 789108, ELVER). This work was supported by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (CTSRD), HR0011-18-C-0016 (ECATS), and FA8650-18-C-7809 (CIFV).
dc.publisherIEEE
dc.rightsAll rights reserved
dc.titleRigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process
dc.typeConference Object
prism.endingPage1020
prism.publicationDate2020
prism.publicationNameProceedings - IEEE Symposium on Security and Privacy
prism.startingPage1003
prism.volume2020-May
dc.identifier.doi10.17863/CAM.49648
dcterms.dateAccepted2020-01-30
rioxxterms.versionofrecord10.1109/SP40000.2020.00055
rioxxterms.versionAM
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.licenseref.startdate2020-05-01
dc.contributor.orcidMoore, Simon [0000-0002-2806-495X]
dc.contributor.orcidSewell, Peter [0000-0001-9352-1013]
rioxxterms.typeConference Paper/Proceeding/Abstract
pubs.funder-project-idEngineering and Physical Sciences Research Council (EP/K008528/1)
pubs.funder-project-idEuropean Research Council (789108)
pubs.conference-name2020 IEEE Symposium on Security and Privacy (SP)
pubs.conference-start-date2020-05-18
cam.orpheus.successThu Nov 05 11:55:57 GMT 2020 - Embargo updated
pubs.conference-finish-date2020-05-21
rioxxterms.freetoread.startdate2021-05-01


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record