Dark Reading is part of the Informa Tech Division of Informa PLC

This site is operated by a business or businesses owned by Informa PLC and all copyright resides with them.Informa PLC's registered office is 5 Howick Place, London SW1P 1WG. Registered in England and Wales. Number 8860726.

Application Security

6/23/2015
11:00 AM
Dark Reading
Dark Reading
Products and Releases
50%
50%

SRI International Releases New Game for DARPA Crowd-Sourced Software Verification Program

Citizen scientists interested in cybersecurity can now play Binary Fission at www.verigames.com

Menlo Park, Calif. – June 23, 2015 —SRI International, in partnership with the University of California, Santa Cruz (UCSC), the Air Force Research Laboratory, and the U.S. Defense Advanced Research Projects Agency (DARPA) Crowd-Sourced Formal Verification (CSFV) program, has created a game where sophisticated gamers can help improve security of the country’s critical software. Binary Fission was designed as a fun and accessible way for “citizen scientists” to help increase the reliability and security of mission critical software by verifying that it is free of cyber vulnerabilities.

From a gaming perspective, the goal of Binary Fission is simple — sort colored atomic particles or “quarks” in as few steps as possible. Players use up to 100 filters to sort the particles into separate pools. As players move their cursor over a particular pool, they are shown in real time how successfully a particular filter would sort the quarks in that pool.

Binary Fission also allows more sophisticated interactions: rather than defining behavior of software elements from scratch, players can mix-and-match pre-made descriptions. The search for such descriptions – technically called "loop invariants" – takes advantage of visual pattern recognition that people are better at than computers.

"We're very excited about the play experience in Binary Fission," said lead game designer Heather Logas of UC Santa Cruz. "Informed by new research about formal software verification and inspired by the citizen science phenomenon, the game is both very playable and also should contribute well to the underlying science problem."

Examples of critical software behavior, along with some pre-made invariants, are used to generate each level in Binary Fission.  The quarks in the game actually represent values of variables inside the critical software, and the sorting filters represent the potential invariants to be explored and applied. By combining filters efficiently, players can help to verify that the software is free of security vulnerabilities. Binary Fission also emphasizes community, an important aspect of successful citizen science projects, through integrated chat, active community management and regular community events.

“The auxiliary Binary Fission feature set is very light, since our goal is to keep players focused on solving problems,” said John Murray, Ph.D., program director in the Computer Science Laboratory at SRI International and principal investigator for the overall project. “However, as a citizen science project, our recruitment policy draws in players who are interested in solving cybersecurity issues.”

Currently, formal software verification is rarely used because relatively few people have the necessary training in verification techniques. In addition, finding loop invariants in software programs has historically been a challenging task requiring extensive training and insight.

“SRI is well versed in formal software verification, with over a quarter of a century spent assuring that mission-critical computer systems are error-free, secure and interoperable. We are pleased to work with our partners in DARPA’s highly innovative, creative and fun program,” said Patrick Lincoln, Ph.D., director of SRI’s Computer Science Laboratory. “We learned a lot of valuable lessons with our first game of this type, Xylem.  For our gaming approach to succeed, we need a more sophisticated game for a more sophisticated audience.  We have leveled up our research, and with more automation, interaction and sophistication, Binary Fission is our best game yet.”

Binary Fission is one of five games that DARPA is releasing under its Crowd-Sourced Formal Verification (CSFV) program. All games, including the first SRI-and-UCSC-created game, Xylem, are freely accessible through the Verigames website.

UCSC and SRI are also collaborating with researchers at CEA, the French Alternative Energies and Atomic Energy Commission (Commissariat à l'énergie atomique et aux énergies alternatives) to develop tools for software analysis and formal verification that feed into Binary Fission.

This material is based upon work supported by the United States Air Force Research Laboratory (AFRL) and the Defense Advanced Research Projects Agency under Contract No. FA8750-12-C-0225. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of AFRL or DARPA.

 

Distribution Statement "A" (Approved for Public Release, Distribution Unlimited)

###

 

About SRI International

SRI International creates world-changing solutions to make people safer, healthier, and more productive. SRI, a research center headquartered in Menlo Park, California, works primarily in advanced technology and systems, biosciences, computing, and education. SRI brings its innovations to the marketplace through technology licensing, spin-off ventures and new product solutions.

 

 

Recommended Reading:

Comment  | 
Print  | 
More Insights
Comments
Newest First  |  Oldest First  |  Threaded View
US Capitol Attack a Wake-up Call for the Integration of Physical & IT Security
Seth Rosenblatt, Contributing Writer,  1/11/2021
More SolarWinds Attack Details Emerge
Kelly Jackson Higgins, Executive Editor at Dark Reading,  1/12/2021
Vulnerability Management Has a Data Problem
Tal Morgenstern, Co-Founder & Chief Product Officer, Vulcan Cyber,  1/14/2021
Register for Dark Reading Newsletters
White Papers
Video
Cartoon
Current Issue
2020: The Year in Security
Download this Tech Digest for a look at the biggest security stories that - so far - have shaped a very strange and stressful year.
Flash Poll
Assessing Cybersecurity Risk in Today's Enterprises
Assessing Cybersecurity Risk in Today's Enterprises
COVID-19 has created a new IT paradigm in the enterprise -- and a new level of cybersecurity risk. This report offers a look at how enterprises are assessing and managing cyber-risk under the new normal.
Twitter Feed
Dark Reading - Bug Report
Bug Report
Enterprise Vulnerabilities
From DHS/US-CERT's National Vulnerability Database
CVE-2020-7343
PUBLISHED: 2021-01-18
Missing Authorization vulnerability in McAfee Agent (MA) for Windows prior to 5.7.1 allows local users to block McAfee product updates by manipulating a directory used by MA for temporary files. The product would continue to function with out-of-date detection files.
CVE-2020-28476
PUBLISHED: 2021-01-18
All versions of package tornado are vulnerable to Web Cache Poisoning by using a vector called parameter cloaking. When the attacker can separate query parameters using a semicolon (;), they can cause a difference in the interpretation of the request between the proxy (running with default configura...
CVE-2020-28473
PUBLISHED: 2021-01-18
The package bottle from 0 and before 0.12.19 are vulnerable to Web Cache Poisoning by using a vector called parameter cloaking. When the attacker can separate query parameters using a semicolon (;), they can cause a difference in the interpretation of the request between the proxy (running with defa...
CVE-2021-25173
PUBLISHED: 2021-01-18
An issue was discovered in Open Design Alliance Drawings SDK before 2021.12. A memory allocation with excessive size vulnerability exists when reading malformed DGN files, which allows attackers to cause a crash, potentially enabling denial of service (crash, exit, or restart).
CVE-2021-25174
PUBLISHED: 2021-01-18
An issue was discovered in Open Design Alliance Drawings SDK before 2021.12. A memory corruption vulnerability exists when reading malformed DGN files. It can allow attackers to cause a crash, potentially enabling denial of service (Crash, Exit, or Restart).