-
Notifications
You must be signed in to change notification settings - Fork 1
/
references.bib
225 lines (200 loc) · 9.73 KB
/
references.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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
@inproceedings{ironclad,
author = {Hawblitzel, Chris and Howell, Jon and Lorch, Jay and Narayan, Arjun and Parno, Bryan and Zhang, Danfeng and Zill, Brian},
title = {Ironclad Apps: End-to-End Security via Automated Full-System Verification},
booktitle = {USENIX Symposium on Operating Systems Design and Implementation (OSDI)},
year = {2014},
month = {October},
abstract = {
An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app’s behavior. This does more than eliminate implementation vulnerabilities such as buffer overflows, parsing errors, or data leaks; it tells the user exactly how the app will behave at all times. We provide these guarantees via complete, low-level software verification. We then use cryptography and secure hardware to enable secure channels from the verified software to remote users. To achieve such complete verification, we developed a set of new and modified tools, a collection of techniques and engineering disciplines, and a methodology focused on rapid development of verified systems software. We describe our methodology, formal results, and lessons we learned from building a full stack of verified software. That software includes a verified kernel; verified drivers; verified system and crypto libraries including SHA, HMAC, and RSA; and four Ironclad Apps.
},
publisher = {USENIX – Advanced Computing Systems Association},
url = {https://www.microsoft.com/en-us/research/publication/ironclad-apps-end-to-end-security-via-automated-full-system-verification/},
address = {},
pages = {},
journal = {},
volume = {},
chapter = {},
isbn = {},
}
@inproceedings{ironfleet,
author = {Hawblitzel, Chris and Howell, Jon and Kapritsos, Manos and Lorch, Jay and Parno, Bryan and Roberts, Michael Lowell and Setty, Srinath and Zill, Brian},
title = {IronFleet: Proving Practical Distributed Systems Correct},
booktitle = {Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)},
year = {2015},
month = {October},
abstract = {
Distributed systems are notorious for harboring subtle bugs. Verification can, in principle, eliminate these bugs a priori, but verification has historically been difficult to apply at full-program scale, much less distributed-system scale.
We describe a methodology for building practical and provably correct distributed systems based on a unique blend of TLA-style state-machine refinement and Hoare-logic verification. We demonstrate the methodology on a complex implementation of a Paxos-based replicated state machine library and a lease-based sharded key-value store. We prove that each obeys a concise safety specification, as well as desirable liveness requirements. Each implementation achieves performance competitive with a reference system. With our methodology and lessons learned, we aim to raise the standard for distributed systems from "tested" to "correct."
},
publisher = {ACM – Association for Computing Machinery},
url = {https://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/},
address = {},
pages = {},
journal = {},
volume = {},
chapter = {},
isbn = {},
}
@inproceedings{simulation-liveness,
author = {Pradeep Kumar Nalla and
Raj Kumar Gajavelly and
Hari Mony and
Jason Baumgartner and
Robert Kanzelman},
title = {Effective Liveness Verification Using a Transformation-Based Framework},
booktitle = {2014 27th International Conference on {VLSI} Design and 2014 13th
International Conference on Embedded Systems, Mumbai, India, January
5-9, 2014},
pages = {74--79},
year = {2014},
url = {http://dx.doi.org/10.1109/VLSID.2014.20},
doi = {10.1109/VLSID.2014.20},
timestamp = {Tue, 21 Apr 2015 17:24:46 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/vlsid/NallaGMBK14},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{tla-lamport,
author = {Lamport, Leslie},
title = {The Temporal Logic of Actions},
journal = {ACM Trans. Program. Lang. Syst.},
issue_date = {May 1994},
volume = {16},
number = {3},
month = may,
year = {1994},
issn = {0164-0925},
pages = {872--923},
numpages = {52},
url = {http://doi.acm.org/10.1145/177492.177726},
doi = {10.1145/177492.177726},
acmid = {177726},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {concurrent programming, liveness properties, safety properties},
}
@Inbook{Ravi2000,
author="Ravi, Kavita
and Bloem, Roderick
and Somenzi, Fabio",
editor="Hunt, Warren A.
and Johnson, Steven D.",
title="A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles",
bookTitle="Formal Methods in Computer-Aided Design: Third International Conference, FMCAD 2000 Austin, TX, USA, November 1--3, 2000 Proceedings",
year="2000",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="162--179",
isbn="978-3-540-40922-9",
doi="10.1007/3-540-40922-X_10",
url="http://dx.doi.org/10.1007/3-540-40922-X_10"
}
@article{Schuppan2006,
author = {Schuppan, Viktor and Biere, Armin},
title = {Liveness Checking As Safety Checking for Infinite State Spaces},
journal = {Electron. Notes Theor. Comput. Sci.},
issue_date = {February, 2006},
volume = {149},
number = {1},
month = feb,
year = {2006},
issn = {1571-0661},
pages = {79--96},
numpages = {18},
url = {http://dx.doi.org/10.1016/j.entcs.2005.11.018},
doi = {10.1016/j.entcs.2005.11.018},
acmid = {1706711},
publisher = {Elsevier Science Publishers B. V.},
address = {Amsterdam, The Netherlands, The Netherlands},
keywords = {infinite state space, linear temporal logic, liveness, model checking, safety},
}
@incollection{compcert,
author = {Leroy, Xavier and Appel, Andrew W. and Blazy, Sandrine and Stewart, Gordon},
title = {The {CompCert} memory model},
year = {2014},
month = apr,
booktitle = {Program Logics for Certified Compilers},
editor = {Appel, Andrew W.},
publisher = {Cambridge University Press},
url = {http://vst.cs.princeton.edu/}
}
@inproceedings{verve,
author = {Yang, Jean and Hawblitzel, Chris},
title = {Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System},
booktitle = {},
year = {2010},
month = {June},
abstract = {
Typed assembly language (TAL) and Hoare logic can verify the absence of many kinds of errors in low-level code.We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called Verve. Our techniques and tools mechanically verify the safety of every assembly language instruction in the operating system, run-time system, drivers, and applications (in fact, every part of the system software except the boot loader). Verve consists of a “Nucleus” that provides primitive access to hardware and memory, a kernel that builds services on top of the Nucleus, and applications that run on top of the kernel. The Nucleus, written in verified assembly language, implements allocation, garbage collection, multiple stacks, interrupt handling, and device access. The kernel, written in C# and compiled to TAL, builds higher-level services, such as preemptive threads, on top of the Nucleus. A TAL checker verifies the safety of the kernel and applications. A Hoare-style verifier with an automated theorem prover verifies both the safety and correctness of the Nucleus. Verve is, to the best of our knowledge, the first operating system mechanically verified to guarantee both type and memory safety. More generally, Verve’s approach demonstrates a practical way to mix high-level typed code with low-level untyped code in a verifiably safe manner.
},
publisher = {Association for Computing Machinery, Inc.},
url = {https://www.microsoft.com/en-us/research/publication/safe-to-the-last-instruction-automated-verification-of-a-type-safe-operating-system/},
address = {},
pages = {},
journal = {},
volume = {},
chapter = {},
isbn = {},
}
@article{Abadi,
author = {Abadi, Mart\'{\i}n and Lamport, Leslie},
title = {The Existence of Refinement Mappings},
journal = {Theor. Comput. Sci.},
issue_date = {May 31, 1991},
volume = {82},
number = {2},
month = may,
year = {1991},
issn = {0304-3975},
pages = {253--284},
numpages = {32},
url = {http://dx.doi.org/10.1016/0304-3975(91)90224-P},
doi = {10.1016/0304-3975(91)90224-P},
acmid = {114018},
publisher = {Elsevier Science Publishers Ltd.},
address = {Essex, UK},
}
@book{lamport-tla-book,
author = {Lamport, Leslie},
title = {Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers},
booktitle = {Specifying Systems},
year = {2002},
month = {June},
publisher = {Addison-Wesley},
url = {https://www.microsoft.com/en-us/research/publication/specifying-systems-the-tla-language-and-tools-for-hardware-and-software-engineers/},
address = {},
pages = {},
journal = {},
volume = {},
chapter = {},
isbn = {},
}
@article{paxos,
author = {Lamport, Leslie},
title = {The Part-Time Parliament},
booktitle = {},
year = {1998},
month = {May},
publisher = {},
url = {https://www.microsoft.com/en-us/research/publication/part-time-parliament/},
address = {},
pages = {},
journal = {},
volume = {},
chapter = {},
isbn = {},
}
@inproceedings{leino-dafny,
author = {Leino, K. Rustan M.},
title = {Dafny: An Automatic Program Verifier for Functional Correctness},
booktitle = {Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
series = {LPAR'10},
year = {2010},
isbn = {3-642-17510-4, 978-3-642-17510-7},
location = {Dakar, Senegal},
pages = {348--370},
numpages = {23},
url = {http://dl.acm.org/citation.cfm?id=1939141.1939161},
acmid = {1939161},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
}