-
Notifications
You must be signed in to change notification settings - Fork 9
/
model-checking.bib
210 lines (163 loc) · 7.54 KB
/
model-checking.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
@InProceedings{GanapathySJRB2005,
author = "Vinod Ganapathy and Sanjit A. Seshia and Somesh Jha and Thomas W. Reps and Randal E. Bryant",
title = "Automatic discovery of {API}-level exploits",
crossref = "ICSE2005",
pages = "312--321",
abstract =
"We argue that finding vulnerabilities in software components is different
from finding exploits against them. Exploits that compromise security often
use several low-level details of the component, such as layouts of stack
frames. Existing software analysis tools, while effective at identifying
vulnerabilities, fail to model low-level details, and are hence unsuitable
for exploit-finding.
\par
We study the issues involved in exploit-finding by considering application
programming interface (API) level exploits. A software component is
vulnerable to an API-level exploit if its security can be compromised by
invoking a sequence of API operations allowed by the component. We present
a framework to model low-level details of APIs, and develop an automatic
technique based on bounded, infinite-state model checking to discover
API-level exploits.
\par
We present two instantiations of this framework. We show that format-string
exploits can be modeled as API-level exploits, and demonstrate our
technique by finding exploits against vulnerabilities in widely-used
software. We also use the framework to model a cryptographic-key management
API (the IBM CCA) and demonstrate a tool that identifies a previously known
exploit.",
}
@InProceedings{HenzingerJMS2003,
author = "Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar
and Gregoire Sutre",
title = "Software Verification with {Blast}",
crossref = "SPIN2003",
pages = "235--239",
abstract =
"Blast is a model checker for C programs based on an algorithm called lazy
abstraction. Specifications are given as temporal safety monitors written
in C syntax. Blast starts with a very coarse predicate abstraction of the
input program and automatically refines the abstraction, on-the-fly and
on-demand, until either a bug is found or the specification is
proved. Then, Blast provides either an error trace or a succinct proof
certificate. Blast has been applied successfully to Linux and Windows
device drivers with tens of thousands of lines of C code."
}
@Article{BallLR2011,
author = "Ball, Thomas and Levin, Vladimir and Rajamani, Sriram K.",
title = "A decade of software model checking with {SLAM}",
journal = CACM,
year = 2011,
volume = 54,
number = 7,
pages = "68--76",
month = jul,
}
@InProceedings{BallR2002,
author = "Thomas Ball and Sriram K. Rajamani",
title = "The {SLAM} project: Debugging system software via static analysis",
crossref = "POPL2002",
pages = "1--3",
note = "Invited talk",
abstract =
"The goal of the SLAM project is to check whether or not a program obeys
``API usage rules'' that specify what it means to be a good client of an
API. The SLAM toolkit statically analyzes a C program to determine whether
or not it violates given usage rules. The toolkit has two unique aspects:
it does not require the programmer to annotate the source program
(invariants are inferred); it minimizes noise (false error messages)
through a process known as ``counterexample-driven refinement''. SLAM
exploits and extends results from program analysis, model checking and
automated deduction. We have successfully applied the SLAM toolkit to
Windows XP device drivers, to both validate behavior and find defects in
their usage of kernel APIs."
}
@InProceedings{BallBKL2010,
author = "Ball, Thomas and Bounimova, Ella and Kumar, Rahul and Levin, Vladimir",
title = "{SLAM2}: Static driver verification with under 4\% false alarms",
crossref = "FMCAD2010",
pages = "35--42",
}
@Article{AndersonH2002,
author = "Henrik Reif Anderson and Henrik Hulgaard",
title = "Boolean expression diagrams",
journal = IandC,
year = 2002,
volume = 179,
number = 2,
pages = "194--212"
}
@InProceedings{EnglerM2004,
author = "Dawson R. Engler and Madanlal Musuvathi",
title = "Static analysis versus software model checking for bug finding",
booktitle = "VMCAI",
pages = "191--210",
year = 2004,
address = "Venice",
month = jan # "~11--13,"
}
@inproceedings{964017,
author = {Roberto Giacobazzi and Isabella Mastroeni},
title = {Abstract non-interference: parameterizing non-interference by abstract interpretation},
booktitle = {POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
year = {2004},
isbn = {1-58113-729-X},
pages = {186--197},
address = {Venice, Italy},
doi = {https://doi.acm.org/10.1145/964001.964017},
}
@inproceedings{940107,
author = { Robby and Matthew B. Dwyer and John Hatcliff},
title = {Bogor: an extensible and highly-modular software model checking framework},
booktitle = {ESEC/FSE-11: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering},
year = {2003},
isbn = {1-58113-743-5},
pages = {267--276},
address = {Helsinki, Finland},
doi = {https://doi.acm.org/10.1145/940071.940107},
}
@article{ClarkeGL1994,
author = {Clarke, Edmund M. and Grumberg, Orna and Long, David E.},
title = {Model checking and abstraction},
journal = TOPLAS,
volume = 16,
number = 5,
year = 1994,
pages = {1512--1542},
}
@InProceedings{BersaniBGKP2016,
author = "Bersani, Marcello M. and Bianculli, Domenico and Ghezzi, Carlo and Krsti\'{c}, Sr\&\#273;an and Pietro, Pierluigi San",
title = "Efficient large-scale trace checking using {MapReduce}",
crossref = "ICSE2016",
pages = "888--898",
}
@InProceedings{RizziED2016,
author = "Rizzi, Eric F. and Elbaum, Sebastian and Dwyer, Matthew B.",
title = "On the techniques we create, the tools we build, and their misalignments: A study of {KLEE}",
crossref = "ICSE2016",
pages = "132--143",
}
@Article{JacksonD96,
author = "Jackson, Daniel and Damon, Craig A.",
title = "Elements of style: Analyzing a software design feature with a counterexample detector",
journal = TSE,
year = 1996,
volume = 22,
number = 7,
pages = "484-495",
}
% LocalWords: GanapathySJRB Vinod Ganapathy Sanjit Seshia Somesh Jha jul
% LocalWords: API CCA InProceedings booktitle NEEDpages addr printf XP doi
% LocalWords: printf's unmodeled seteuid execl HenzingerJMS Henzinger isbn
% LocalWords: Ranjit Jhala Rupak Majumdar Gregoire Sutre BallR Sriram ORNA
% LocalWords: Rajamani AndersonH Henrik Reif Hulgaard IandC BDDs BDD Rahul
% LocalWords: BED's BEDs EnglerM Engler Madanlal Musuvathi VMCAI jan SLAM2
% LocalWords: GanapathySJRB2005 ICSE2005 ICSE2005addr ICSE2005date Bogor
% LocalWords: HenzingerJMS2003 SPIN2003 SPIN2003addr SPIN2003date SIGACT
% LocalWords: BallLR2011 BallR2002 POPL2002 POPL2002addr POPL2002date
% LocalWords: BallBKL2010 Bounimova FMCAD2010 numpages FMCAD2010date OTP
% LocalWords: FMCAD2010addr AndersonH2002 EnglerM2004 unfreed Giacobazzi
% LocalWords: inproceedings Mastroeni Hatcliff Broadcom GRUMBERG VEITH
% LocalWords: Karthik Nagaraj Salman Pervez Braud MacePC MacePC's Akka
% LocalWords: ness ClarkeGL1994 Grumberg Orna Godefroid MicroX Bersani
% LocalWords: BersaniBGKP2016 Bianculli Ghezzi Krsti Pierluigi MapReduce
% LocalWords: ICSE2016 ICSE2016date ICSE2016addr timesteps pointwise