CSFV
A framework of crowdsourcing tools for formal software verification
Crowd-sourced Formal Verification (CSFV) Integration
As developers for the Department of Defense (DoD) construct large software components and systems consisting of millions of lines of code, this software should go through formal verification (FV) to ensure that mission-essential software is free from disruptive errors and security vulnerabilities. Unfortunately there is a shortage of highly specialized FV experts to support this undertaking. DARPA’s Crowd-Sourced Formal Verification (CSFV) program has been building games that break down and recast FV problems as discrete puzzles that are more accessible to a broad population, increasing the manpower to construct FV proofs.
Much progress has already been made on this effort, but there remains a need to develop games that can not only address FV problems, but also be more engaging to encourage participation. DARPA required a team to maintain and extend the CSFV program website that provides access to these games, perform additional game analytics, and investigate alternative incentives for crowd-sourced software verification participation.
The Charles River Analytics Solution
Scientists and software engineers at Charles River Analytics have been part of the CSFV project since its inception. We developed a resource allocation model that used market-based optimization to manage the delivery of verification tasks to individual participants in the crowdsourcing system. Next, we applied computational analytics and expert evaluations to determine how CSFV games could be improved to increase participation. We also integrated the superset of CSFV games for release on Verigames. In addition, we have been continuing analytical efforts investigating the strategy of game experts and identifying usability and tutorial issues. We have also been managing alternative crowdsourcing mechanisms, including Mechanical Turk, sponsored contests, and broadcast bug hunts, to determine impacts on CSFV game play statistics and to optimize future CSFV efforts.
The Benefit
CSFV is an exciting application of “citizen science” and has demonstrated clear successes with expert game players who have helped to further formal verification proofs. Charles River played a key role as the system integrator on the CSFV program, maintaining the verigames website in collaboration with TopCoder, and analyzing the games to support user experience and performance improvements. We also enabled a successful Phase 2 deployment and test of Mechanical Turk as a non-gaming solution, showing that it provides an effective means to lower costs of overall verification
Contact us to learn more about CSFV and our other capabilities.
The project is sponsored by the Defense Advanced Research Projects Agency (DARPA) and the United States Air Force under contract number FA8750-15-C-0074.
