Werner Dietl
wdietl@uwaterloo.ca, Room EIT 4007
Lessons Learned in Game Development for Crowdsourced Software Formal Verification
Download: PDF.
“Lessons Learned in Game Development for Crowdsourced Software Formal Verification” by D. Dean, S. Guarino, L. Eusebi, A. Keplinger, T. Pavlik, R. Watro, A. Cammarata, J. Murray, K. McLaughlin, J. Cheng, and T. Maddern. In USENIX Summit on Gaming, Games, and Gamification in Security Education (3GSE), 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{csfv-lessons-3gse2015, author = {D. Dean and S. Guarino and L. Eusebi and A. Keplinger and T. Pavlik and R. Watro and A. Cammarata and J. Murray and K. McLaughlin and J. Cheng and T. Maddern}, title = {Lessons Learned in Game Development for Crowdsourced Software Formal Verification}, booktitle = {USENIX Summit on Gaming, Games, and Gamification in Security Education (3GSE)}, month = aug, }
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author’s copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
(This webpage was created with bibtex2web.)