Task 2 Papers
| [1] | Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell. Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. In Security and Privacy 2020: Proceedings of the 41st IEEE Symposium on Security and Privacy (SP), May 2020. [ bib | .pdf | Abstract ] |
| [2] | Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell. ARMv8-A system semantics: instruction fetch in relaxed architectures (extended version). In ESOP 2020: Proceedings of the 29th European Symposium on Programming, April 2020. This is an extended version of the ESOP 2020 paper, with appendices giving additional details. [ bib | .pdf | Abstract ] |
| [3] | J. Woodruff, A. Joannou, H. Xia, A. Fox, R. M. Norton, D. Chisnall, B. Davis, K. Gudka, N. W. Filardo, A. T. Markettos, M. Roe, P. G. Neumann, R. N. M. Watson, and S. W. Moore. Cheri concentrate: Practical compressed capabilities. IEEE Transactions on Computers, 68(10):1455--1469, October 2019. [ bib | DOI | .pdf | Abstract ] |
| [4] | Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter Neumann. An introduction to CHERI. Technical Report UCAM-CL-TR-941, University of Cambridge, Computer Laboratory, September 2019. [ bib | .pdf | Abstract ] |
| [5] | Kyndylan Nienhuis, Alexandre Joannou, Anthony Fox, Michael Roe, Thomas Bauereiss, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell. Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. Technical Report UCAM-CL-TR-940, University of Cambridge, Computer Laboratory, September 2019. [ bib | .pdf | Abstract ] |
| [6] | Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, David Chisnall, Brooks Davis, Nathaniel Wesley Filardo, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert Norton, Alex Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan Xia. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7). Technical Report UCAM-CL-TR-927, University of Cambridge, Computer Laboratory, June 2019. [ bib | .pdf | Abstract ] |
| [7] | Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, and Chung-Kil Hur. Promising-ARM/RISC-V: A simpler and faster operational concurrency model. In PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2019. [ bib | DOI | .pdf | Abstract ] |
| [8] | Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, and Jonathan Woodruff. CheriABI: Enforcing valid pointer provenance and minimizing pointer privilege in the POSIX C run-time environment. Technical Report UCAM-CL-TR-932, University of Cambridge, Computer Laboratory, January 2019. [ bib | .pdf | Abstract ] |
| [9] | Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS. In POPL 2019: Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2019. Proc. ACM Program. Lang. 3, POPL, Article 71. [ bib | DOI | .pdf | Abstract ] |
| [10] | Andrew Waterman and Krste Asanović, editors. The RISC-V Instruction Set Manual Volume I: Unprivileged ISA. December 2018. Document Version 20181221-Public-Review-draft. Contributors: Arvind, Krste Asanović, Rimas Avižienis, Jacob Bachmeyer, Christopher F. Batten, Allen J. Baum, Alex Bradbury, Scott Beamer, Preston Briggs, Christopher Celio, Chuanhua Chang, David Chisnall, Paul Clayton, Palmer Dabbelt, Roger Espasa, Shaked Flur, Stefan Freudenberger, Jan Gray, Michael Hamburg, John Hauser, David Horner, Bruce Hoult, Alexandre Joannou, Olof Johansson, Ben Keller, Yunsup Lee, Paul Loewenstein, Daniel Lustig, Yatin Manerkar, Luc Maranget, Margaret Martonosi, Joseph Myers, Vijayanand Nagarajan, Rishiyur Nikhil, Jonas Oberhauser, Stefan O'Rear, Albert Ou, John Ousterhout, David Patterson, Christopher Pulte, Jose Renau, Colin Schmidt, Peter Sewell, Susmit Sarkar, Michael Taylor, Wesley Terpstra, Matt Thomas, Tommy Thorn, Caroline Trippel, Ray VanDeWalker, Muralidaran Vijayaraghavan, Megan Wachs, Andrew Waterman, Robert Watson, Derek Williams, Andrew Wright, Reinoud Zandijk, and Sizhuo Zhang. [ bib | .pdf ] |
| [11] | Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. In POPL 2018, pages 19:1--19:29, January 2018. [ bib | DOI | http | .pdf | Abstract ] |
| [12] | Alexandre Joannou, Jonathan Woodruff, Robert Kovacsics, Simon W. Moore, Alex Bradbury, Hongyan Xia, Robert N. M. Watson, David Chisnall, Michael Roe, Brooks Davis, Edward Napierala, John Baldwin, Khilan Gudka, Peter G. Neumann, Alfredo Mazzinghi, Alex Richardson, Stacey Son, and A. Theodore Markettos. Efficient tagged memory. In ICCD 2017: IEEE 35th International Conference on Computer Design, November 2017. [ bib | DOI | www: | .pdf | Abstract ] |
| [13] | Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Jonathan Anderson, John Baldwin, David Chisnall, Brooks Davis, Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Robert Norton, Stacey Son, and Hongyan Xia. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 6). Technical Report UCAM-CL-TR-907, University of Cambridge, Computer Laboratory, April 2017. [ bib | .pdf | Abstract ] |
| [14] | Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. Mixed-size concurrency: ARM, POWER, C/C++11, and SC. In POPL 2017: The 44st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, pages 429--442, January 2017. [ bib | DOI | http | .pdf | Abstract ] |
| [15] | Brian Campbell and Ian Stark. Extracting behaviour from an executable instruction set model. In Ruzica Piskac and Muralidhar Talupur, editors, FMCAD 2016: Formal Methods in Computer-Aided Design, pages 33--40, October 2016. Full proceedings http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/proceedings/fmcad-2016-proceedings.pdf. [ bib | .pdf | Abstract ] |
| [16] | Robert N.M. Watson, Robert M. Norton, Jonathan Woodruff, Simon W. Moore, Peter G. Neumann, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Michael Roe, Nirav H. Dave, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Ed Maste, Steven J. Murdoch, Colin Rothwell, Stacey D. Son, and Munraj Vadera. Fast protection-domain crossing in the CHERI capability-system architecture. IEEE Micro, 36(5):38--49, September 2016. [ bib | DOI | http | Abstract ] |
| [17] | M. Naylor, S. W. Moore, and A. Mujumdar. A consistency checker for memory subsystem traces. In FMCAD 2016: Formal Methods in Computer-Aided Design, September 2016. [ bib | DOI | .pdf | Abstract ] |
| [18] | Brian Campbell and Ian Stark. Randomised testing of a microprocessor model using SMT-solver state generation. Sci. Comput. Program., 118:60--76, March 2016. [ bib | DOI | .pdf | Abstract ] |
| [19] | Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. Modelling the ARMv8 architecture, operationally: concurrency and ISA. In POPL 2016: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, FL, USA, pages 608--621, January 2016. [ bib | DOI | http | .pdf | Abstract ] |
| [20] | Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. In MICRO 2015: Proceedings of the 48th International Symposium on Microarchitecture, , Waikiki, HI, USA, pages 635--646, December 2015. [ bib | DOI | http | .pdf | Abstract ] |
| [21] | Robert N. M. Watson, David Chisnall, Brooks Davis, Wojciech Koszek, Simon W. Moore, Steven J. Murdoch, Peter G. Neumann, and Jonathan Woodruff. Capability Hardware Enhanced RISC Instructions: CHERI Programmer's Guide. Technical Report UCAM-CL-TR-877, University of Cambridge, Computer Laboratory, September 2015. [ bib | .pdf | Abstract ] |
| [22] | Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Jonathan Anderson, David Chisnall, Brooks Davis, Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Robert Norton, and Stacey Son. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture. Technical Report UCAM-CL-TR-876, University of Cambridge, Computer Laboratory, September 2015. [ bib | .pdf | Abstract ] |
| [23] | Matthew Naylor and Simon W. Moore. A generic synthesisable test bench. In MEMOCODE 2015: ACM/IEEE International Conference on Formal Methods and Models for Codesign, Austin, TX, USA, pages 128--137, September 2015. [ bib | DOI | http | .pdf | Abstract ] |
| [24] | Robert N. M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan Anderson, David Chisnall, Nirav Dave, Brooks Davis, Khilan Gudka, Ben Laurie, Steven J. Murdoch, Robert Norton, Michael Roe, Stacey Son, and Munraj Vadera. CHERI: A hybrid capability-system architecture for scalable software compartmentalization. In Security and Privacy 2015: Proceedings of the 36th IEEE Symposium on Security and Privacy (“Oakland”), May 2015. [ bib | DOI | .pdf | Abstract ] |
| [25] | S. Flur, K. Gray, G. Kerneis, D. Mulligan, C. Pulte, S. Sarkar, and P. Sewell. Rigorous architectural modelling for production multiprocessors, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference. [ bib | Abstract ] |
| [26] | Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, and John Wickerson. GPU concurrency: Weak behaviours and programming assumptions. In ASPLOS 2015: Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, Istanbul, Turkey, pages 577--591, March 2015. [ bib | DOI | http | Abstract ] |
| [27] | Brian Campbell and Ian Stark. Randomised testing of a microprocessor model using SMT-solver state generation. In Frédéric Lang and Francesco Flammini, editors, FMICS 2014: Formal Methods for Industrial Critical Systems, volume 8718 of Lecture Notes in Computer Science, pages 185--199. Springer, September 2014. [ bib | DOI | .pdf | Abstract ] |
This file was generated by bibtex2html 1.99.