bib-rems.bib

@article{rems-scico15,
  title = {Randomised Testing of a Microprocessor Model Using {SMT}-Solver State Generation},
  author = {Brian Campbell and Ian Stark},
  journal = {Science of Computer Programming},
  year = 2016,
  volume = 118,
  pages = {60--76},
  month = {March},
  issn = {0167-6423},
  doi = {10.1016/j.scico.2015.10.012},
  preprint = {rems/scico2015.pdf}
}

@inproceedings{rems-fmics14,
  title = {Randomised Testing of a Microprocessor Model Using {SMT}-Solver State Generation},
  author = {Brian Campbell and Ian Stark},
  booktitle = {Formal Methods for Industrial Critical Systems ({FMICS} 2014)},
  year = 2014,
  editor = {Fr{\'{e}}d{\'{e}}ric Lang and Francesco Flammini},
  volume = 8718,
  series = {Lecture Notes in Computer Science},
  pages = {185--199},
  publisher = {Springer},
  doi = {10.1007/978-3-319-10702-8_13},
  slides = {rems/fmics-m0-talk.pdf},
  preprint = {rems/fmics2014.pdf},
  preprintnote = {The final publication is available at link.springer.com}
}

@inproceedings{rems-fmcad16,
  title = {Extracting Behaviour from an Executable Instruction Set Model},
  author = {Brian Campbell and Ian Stark},
  booktitle = {Formal Methods in Computer-Aided Design, ({FMCAD} 2016)},
  year = 2016,
  editor = {Ruzica Piskac and Muralidhar Talupur},
  pages = {33--40},
  doi = {10.1109/FMCAD.2016.7886658},
  isbn = {978-0-9835678-6-8},
  slides = {rems/fmcad16-slides.pdf},
  preprint = {rems/fmcad16.pdf},
  preprintnote = {\url{http://www.fmcad.org/FMCAD16}}
}

@article{DBLP:journals/pacmpl/ArmstrongBCRGNM19,
  author = {Alasdair Armstrong and
               Thomas Bauereiss and
               Brian Campbell and
               Alastair Reid and
               Kathryn E. Gray and
               Robert M. Norton and
               Prashanth Mundkur and
               Mark Wassell and
               Jon French and
               Christopher Pulte and
               Shaked Flur and
               Ian Stark and
               Neel Krishnaswami and
               Peter Sewell},
  title = {{ISA} semantics for {ARMv8-A}, {RISC-V}, and {CHERI-MIPS}},
  journal = {Proc. {ACM} Program. Lang.},
  volume = {3},
  number = {{POPL}},
  pages = {71:1--71:31},
  year = {2019},
  xurl = {https://doi.org/10.1145/3290384},
  doi = {10.1145/3290384},
  timestamp = {Thu, 16 Apr 2020 13:51:46 +0200},
  biburl = {https://dblp.org/rec/journals/pacmpl/ArmstrongBCRGNM19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{cheri-formal-SP2020,
  author = {Kyndylan Nienhuis and Alexandre Joannou and Thomas Bauereiss and Anthony Fox and Michael Roe and Brian Campbell and Matthew Naylor and Robert M. Norton and Moore, Simon W.  and Neumann, Peter G.  and Ian Stark and Watson, Robert N. M.  and Peter Sewell},
  title = {Rigorous engineering for hardware security: Formal modelling and proof in the {CHERI} design and implementation process},
  optcrossref = {},
  optkey = {},
  conf = {Security and Privacy 2020},
  booktitle = {Proceedings of the 41st IEEE Symposium on Security and Privacy (SP)},
  year = {2020},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  pages = {1007--1024},
  month = may,
  optaddress = {},
  optorganization = {},
  optpublisher = {},
  optnote = {},
  optannote = {},
  xabstract = {The 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.
},
  pdf = {https://www.cl.cam.ac.uk/users/pes20/cheri-formal.pdf},
  apollourl = {https://www.repository.cam.ac.uk/handle/1810/302580},
  publisherurl = {https://www.computer.org/csdl/proceedings-article/sp/2020/349700b007/1j2Lg3o6fdK},
  doi = {10.1109/SP40000.2020.00055},
  project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
  topic = {cheri},
  cheriformal = {true},
  recent = {true}
}