Lessons learned in game development for crowdsourced software formal verification

Download: PDF.

“Lessons learned in game development for crowdsourced software formal verification” by Drew Dean, Sean Guarino, Leonard Eusebi, Andrew Keplinger, Tim Pavlik, Ronald Watro, Aaron Cammarata, John Murray, Kelly McLaughlin, John Cheng, and Thomas Maddern. In 3GSE: USENIX Summit on Gaming, Games, and Gamification in Security Education, (Washington, DC), Aug. 2015.

Abstract

The history of formal methods and computer security research is long and intertwined. Program logics that were in theory capable of proving security properties of software were developed by the early 1970s. The development of the first security models gave rise to a desire to prove that the models did, in fact, enforce the properties that they claimed to, and that an actual implementation of the model was correct with respect to its specification. Optimism reached its peak in the early to mid-1980s, and the peak of formal methods for security was reached shortly before the publication of the Orange Book, where the certification of a system at class A1 required formal methods. Formal verification of software was considered the gold standard evidence that the software enforced a particular set of properties. Soon afterwards, the costs of formal methods, in both time and money, became all too apparent. Mainstream computer security research shifted focus to analysis of cryptographic protocols, policies around cryptographic key management, and clever fixes for security problems found in contemporary systems.

Download: PDF.

BibTeX entry:

@inproceedings{DeanGEKPWCMMCM2015,
   author = {Drew Dean and Sean Guarino and Leonard Eusebi and Andrew
	Keplinger and Tim Pavlik and Ronald Watro and Aaron Cammarata and
	John Murray and Kelly McLaughlin and John Cheng and Thomas
	Maddern},
   title = {Lessons learned in game development for crowdsourced software
	formal verification},
   booktitle = {3GSE: USENIX Summit on Gaming, Games, and Gamification in
	Security Education},
   address = {Washington, DC},
   month = aug,
   year = {2015}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.