loading...
Model Checking An Entire Linux Distribution for Security Violations
Tucson, Arizona December 05-December 09
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSAC.2005.3921st Annual Computer Security Applica ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Benjamin Schwarz, Hao Chen, David Wagner, Jeremy Lin, Wei Tu, Geoff Morrison, Jacob West, "Model Checking An Entire Linux Distribution for Security Violations," Computer Security Applications Conference, Annual, pp. 13-22, 21st Annual Computer Security Applications Conference (ACSAC'05), 2005.
 
 
BibTex
x
 
@article{ 10.1109/CSAC.2005.39,
author = {Benjamin Schwarz and Hao Chen and David Wagner and Jeremy Lin and Wei Tu and Geoff Morrison and Jacob West},
title = {Model Checking An Entire Linux Distribution for Security Violations},
journal ={Computer Security Applications Conference, Annual},
volume = {0},
year = {2005},
issn = {1063-9527},
pages = {13-22},
doi = {http://doi.ieeecomputersociety.org/10.1109/CSAC.2005.39},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Security Applications Conference, Annual
TI - Model Checking An Entire Linux Distribution for Security Violations
SN - 1063-9527
SP13
EP22
A1 - Benjamin Schwarz,
A1 - Hao Chen,
A1 - David Wagner,
A1 - Jeremy Lin,
A1 - Wei Tu,
A1 - Geoff Morrison,
A1 - Jacob West,
PY - 2005
KW - null
VL - 0
JA - Computer Security Applications Conference, Annual
ER -
 
Benjamin Schwarz, University of California, Berkeley
Hao Chen, University of California, Berkeley
David Wagner, University of California, Berkeley
Jeremy Lin, University of California, Berkeley
Wei Tu, University of California, Berkeley
Geoff Morrison, University of California, Berkeley
Jacob West, University of California, Berkeley
Software model checking has become a popular tool for verifying programs? behavior. Recent results suggest that it is viable for finding and eradicating security bugs quickly. However, even state-of-the-art model checkers are limited in use when they report an overwhelming number of false positives, or when their lengthy running time dwarfs other software development processes. In this paper we report our experiences with software model checking for security properties on an extremely large scale-an entire Linux distribution consisting of 839 packages and 60 million lines of code. To date, we have discovered 108 exploitable bugs. Our results indicate that model checking can be both a feasible and integral part of the software development process.
Citation:
Benjamin Schwarz, Hao Chen, David Wagner, Jeremy Lin, Wei Tu, Geoff Morrison, Jacob West, "Model Checking An Entire Linux Distribution for Security Violations," acsac, pp.13-22, 21st Annual Computer Security Applications Conference (ACSAC'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.


Suggestions