-
Notifications
You must be signed in to change notification settings - Fork 3
/
cheri.bib
139 lines (129 loc) · 10.5 KB
/
cheri.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
@inproceedings{ChisnallCPDP11,
author = {Chisnall, David and Rothwell, Colin and Watson, Robert N. M. and Woodruff, Jonathan and Vadera, Munraj and Moore, Simon W. and Roe, Michael and Davis, Brooks and Neumann, Peter G.},
location = {Istanbul, Turkey},
publisher = {ACM},
url = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201503-asplos2015-cheri-cmachine.pdf},
booktitle = {Proceedings of the {{Twentieth International Conference}} on {{Architectural Support}} for {{Programming Languages}} and {{Operating Systems}}},
date = {2015-03},
doi = {10.1145/2694344.2694367},
isbn = {978-1-4503-2835-7},
keywords = {bounds checking,C language,capabilities,compilers,memory protection,memory safety,processor design,security},
pages = {117--130},
series = {{{ASPLOS}} '15},
shorttitle = {Beyond the {{PDP}}-11},
title = {Beyond the {{PDP}}-11: {{Architectural}} Support for a Memory-Safe {{C}} Abstract Machine},
}
@inproceedings{davis2019:cheriabi,
author = {Davis, Brooks and Watson, Robert N. M. and Richardson, Alexander and Neumann, Peter G. and Moore, Simon W. and Baldwin, John and Chisnall, David and Clarke, Jessica and Filardo, Nathaniel Wesley and Gudka, Khilan and Joannou, Alexandre and Laurie, Ben and Markettos, A. Theodore and Maste, J. Edward and Mazzinghi, Alfredo and Napierala, Edward Tomasz and Norton, Robert M. and Roe, Michael and Sewell, Peter and Son, Stacey and Woodruff, Jonathan},
location = {Providence, RI, USA},
publisher = {ACM},
url = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201904-asplos-cheriabi.pdf},
booktitle = {Proceedings of the {{Twenty}}-{{Fourth International Conference}} on {{Architectural Support}} for {{Programming Languages}} and {{Operating Systems}}},
date = {2019},
doi = {10.1145/3297858.3304042},
eventtitle = {{{ASPLOS}} 2019},
isbn = {978-1-4503-6240-5},
keywords = {cheri,hardware,operating systems,security},
pages = {379--393},
series = {{{ASPLOS}} '19},
shorttitle = {{{CheriABI}}},
title = {{{CheriABI}}: {{Enforcing Valid Pointer Provenance}} and {{Minimizing Pointer Privilege}} in the {{POSIX C Run}}-Time {{Environment}}},
}
@report{UCAM-CL-TR-932,
author = {Davis, Brooks and Watson, Robert N. M. and Richardson, Alexander and Neumann, Peter G. and Moore, Simon W. and Baldwin, John and Chisnall, David and Clarke, Jessica and Filardo, Nathaniel Wesley and Gudka, Khilan and Joannou, Alexandre and Laurie, Ben and Markettos, A. Theodore and Maste, J. Edward and Mazzinghi, Alfredo and Napierala, Edward Tomasz and Norton, Robert M. and Roe, Michael and Sewell, Peter and Son, Stacey and Woodruff, Jonathan},
institution = {University of Cambridge, Computer Laboratory},
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-932.pdf},
date = {2019-04},
langid = {english},
number = {UCAM-CL-TR-932},
shorttitle = {{{CheriABI}}},
title = {{{CheriABI}}: {{Enforcing}} Valid Pointer Provenance and Minimizing Pointer Privilege in the {{POSIX C}} Run-Time Environment},
type = {Technical Report},
}
@inproceedings{filardo:cornucopia,
author = {Filardo, Nathaniel and Gutstein, Brett F. and Woodruff, Jonathan and Ainsworth, Sam and Paul-Trifu, Lucian and Davis, Brooks and Xia, Hongyan and Napierala, Edward and Richardson, Alexander and Baldwin, John and Chisnall, David and Clarke, Jessica and Gudka, Khilan and Joannou, Alexandre and Markettos, Theo and Mazzinghi, Alfredo and Norton, Robert M. and Roe, Michael and Sewell, Peter and Son, Stacey and Jones, Timothy M. and Moore, Simon W. and Neumann, Peter G. and Watson, Robert},
location = {Los Alamitos, CA, USA},
publisher = {IEEE Computer Society},
url = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2020oakland-cornucopia.pdf},
booktitle = {2020 {{IEEE}} Symposium on Security and Privacy ({{SP}})},
date = {2020-05},
doi = {10.1109/SP40000.2020.00098},
langid = {english},
pages = {1507--1524},
shorttitle = {Cornucopia},
title = {Cornucopia: {{Temporal Safety}} for {{CHERI Heaps}}},
}
@inproceedings{cerberus-popl2019,
author = {Memarian, Kayvan and Gomes, Victor B. F. and Davis, Brooks and Kell, Stephen and Richardson, Alexander and Watson, Robert N. M. and Sewell, Peter},
location = {Cascais, Portugal},
url = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201901-popl-cerberus.pdf},
booktitle = {Proceedings of the {{ACM}} on {{Programming Languages}}},
date = {2019-01},
doi = {10.1145/3290380},
keywords = {C},
pages = {67:1--67:32},
title = {Exploring {{C Semantics}} and {{Pointer Provenance}}},
}
@inproceedings{cheri-formal-SP2020,
abstract = {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.},
author = {Nienhuis, Kyndylan and Joannou, Alexandre and Bauereiss, Thomas and Fox, Anthony and Roe, Michael and Campbell, Brian and Naylor, Matthew and Norton, Robert M. and Moore, Simon W. and Neumann, Peter G. and Stark, Ian and Watson, Robert N. M. and Sewell, Peter},
location = {Los Alamitos, CA, USA},
publisher = {IEEE Computer Society},
url = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/202005oakland-cheri-formal.pdf},
booktitle = {2020 {{IEEE}} Symposium on Security and Privacy ({{SP}})},
date = {2020-05},
doi = {10.1109/SP40000.2020.00055},
file = {https://www.cl.cam.ac.uk/users/pes20/cheri-formal.pdf},
pages = {1007--1024},
title = {Rigorous engineering for hardware security: Formal modelling and proof in the {CHERI} design and implementation process},
}
@report{UCAM-CL-TR-941,
author = {Watson, Robert N. M. and Moore, Simon W. and Sewell, Peter and Neumann, Peter G.},
institution = {University of Cambridge, Computer Laboratory},
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-941.pdf},
date = {2019},
langid = {english},
number = {UCAM-CL-TR-941},
title = {An {{Introduction}} to {{CHERI}}},
type = {Technical Report},
}
@report{UCAM-CL-TR-927,
author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff, Jonathan and Roe, Michael and Almatary, Hesham and Anderson, Jonathan and Baldwin, John and Chisnall, David and Davis, Brooks and Filardo, Nathaniel Wesley and Joannou, Alexandre and Laurie, Ben and Markettos, A. Theodore and Moore, Simon W. and Murdoch, Steven J. and Nienhuis, Kyndylan and Norton, Robert and Richardson, Alex and Rugg, Peter and Sewell, Peter and Son, Stacey and Xia, Hongyan},
institution = {University of Cambridge, Computer Laboratory},
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-927.pdf},
date = {2019-06},
langid = {english},
number = {UCAM-CL-TR-927},
shorttitle = {Capability {{Hardware Enhanced RISC Instructions}}},
title = {Capability {{Hardware Enhanced RISC Instructions}}: {{CHERI Instruction}}-{{Set Architecture}} ({{Version}} 7)},
type = {Technical Report},
}
@article{Woodruff2019,
author = {Woodruff, Jonathan and Joannou, Alexandre and Xia, Hongyan and Fox, Anthony and Norton, Robert and Baureiss, Thomas and Chisnall, David and Davis, Brooks and Gudka, Khilan and Filardo, Nathaniel Wesley and Markettos, A. Theodore and Roe, Michael and Neumann, Peter G. and Watson, Robert N. M. and Moore, Simon W.},
url = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2019tc-cheri-concentrate.pdf},
date = {2019-10},
doi = {10.1109/TC.2019.2914037},
issn = {0018-9340, 1557-9956, 2326-3814},
journaltitle = {IEEE Transactions on Computers},
langid = {english},
number = {10},
pages = {1455--1469},
shorttitle = {{{CHERI Concentrate}}},
title = {{{CHERI Concentrate}}: {{Practical Compressed Capabilities}}},
volume = {68},
}
@inproceedings{Xia_CHERIvokeCharacterisingPointer_2019,
author = {Xia, Hongyan and Woodruff, Jonathan and Ainsworth, Sam and Filardo, Nathaniel W. and Roe, Michael and Richardson, Alexander and Rugg, Peter and Neumann, Peter G. and Moore, Simon W. and Watson, Robert N. M. and Jones, Timothy M.},
location = {Columbus, OH, USA},
publisher = {ACM},
url = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201910micro-cheri-temporal-safety.pdf},
booktitle = {Proceedings of the 52nd {{Annual IEEE}}/{{ACM International Symposium}} on {{Microarchitecture}}},
date = {2019},
doi = {10.1145/3352460.3358288},
isbn = {978-1-4503-6938-1},
keywords = {architecture,security,temporal safety,use-after-free},
pages = {545--557},
series = {{{MICRO}} '52},
shorttitle = {{{CHERIvoke}}},
title = {{{CHERIvoke}}: {{Characterising Pointer Revocation}} Using {{CHERI Capabilities}} for {{Temporal Memory Safety}}},
}