Lessons Learned in Game Development for Crowdsourced Software Formal Verification

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.