Crowd Sourced Formal Verification-Augmentation (CSFV-A)

reportActive / Technical Report | Accession Number: AD1010444 | Open PDF

Abstract:

Formal verification FV ensures that mission-essential software is free from disruptive errors and security vulnerabilities, but requires human experts that can be quickly overwhelmed by the increasing number, size, and complexity of software systems. DARPAs Crowd Sourced Formal Verification CSFV program built games that recast FV problems into puzzles to make these problems more accessible, increasing the manpower to construct FV proofs. This effort supported the CSFV program by hosting the games on a public website, and analyzed the gameplay for efficiency to provide FV proofs.

Author(s):
Guarino, Sean ; Eusebi, Leonard
Author Organization(s):
Charles River Analytics, Inc. Cambridge United States
Descriptive Note:
Technical Report,01 Mar 2015,31 Dec 2015
Pagination:
0092

Security Markings

DOCUMENT & CONTEXTUAL SUMMARY

Distribution:
Approved For Public Release
Distribution Statement:
Approved For Public Release;

RECORD

Collection: TR
Identifying Numbers
Report Number(s):
AFRL-RI-RS-TR-2016-142
Contract/Grant Number(s):
FA8750-15-C-0074
Task Number(s):
TC
Project Number(s):
CSFV
Monitor Series:
AFRL-RI-RS-TR-2016-142
 Subject Terms
Joint Capability Areas:
JCA_5_Command and Control; JCA_5.3_Planning; JCA_5.5_Direct; JCA_5.5.1_Communicate Intent and Guidance; JCA_5.3.4_Develop Courses of Action; JCA_5.3.5_Analyze Courses of Action; JCA_5.3.3_Develop Strategy; JCA_5.5.2_Task; JCA_5.2_Understand; JCA_5.2.3_Share Knowledge and Situational Awareness; JCA_8_Building Partnerships; JCA_1_Force Support; JCA_5.6.3_Assess Achievement of Objectives; JCA_5.6_Monitor; JCA_6_Net Centric; JCA_8.2_Shape; JCA_1.4_Force Support; JCA_1.2.5_Lessons Learned; JCA_1.2_Force Preparation; JCA_6.4.1_Secure Information Exchange; JCA_8.2.4_Leverage Capacities and Capabilities of Security Establishments
Modernization Areas:
Cyber
Communities of Interest:
Engineered Resilient Systems
Descriptor(s):
Computer program verification, computer programs
Keyword(s):
cs(Crowd Source), Software, fv(Formal Verification), csfv Games, crowd sourcing
Report Date:
2016 Jun 01
Creation Date:
2017 Jan 24