Slashdot Mirror

← Back to Stories (view on slashdot.org)

DARPA Wants You To Verify Software Flaws By Playing Games

Posted by samzenpus on from the play-the-bugs-away dept.

coondoggie writes: Researchers at the Defense Advanced Research Projects Agency (DARPA) think online gamers can perform the tedious software verification work typically done by professional coding experts. They were so impressed with their first crowdsourced flaw-detecting games, they announced an new round of five games this week designed for improved playability as well as increased software verification effectiveness. “These games translated players’ actions into program annotations and assisted formal verification experts in generating mathematical proofs to verify the absence of important classes of flaws in software written in the C and Java programming languages. An initial analysis indicates that non-experts playing CSFV games generated hundreds of thousands of annotations,” DARPA stated.

19 of 31 comments (clear)

  1. War Games by Stuarticus · · Score: 3, Funny

    Set number of players zero.

    --
    If you think someone isn't free to have a different definition of "freedom" you may be a tyrant.
    1. Re:War Games by rooie · · Score: 2

      Shall we play a game?

    2. Re:War Games by GLMDesigns · · Score: 1

      I choose Global Nuclear War

      --
      If you're scared of your govt then you need to further restrict its powers
      Vote 3rd Party in 2016 and beyond
    3. Re:War Games by SmileyByte · · Score: 3, Insightful

      What a strange game. The only winning move is not to play.

      --

      h@hh@hh@...@.&.... "You shall not pass!"
  2. Obligatory /. Coverup Post - Again... by Anonymous Coward · · Score: 2, Interesting

    ./ --

    Run this article, respond appropriately and this protest will be over. You're acticting like a manager/laywer-type person at Oracle. You can do better than this.

    This is "the" scandal in tech right now, and you're actively supressing discusstion --

    http://mobile.slashdot.org/comments.pl?sid=7477721&cid=49793333

    Mod this up like all the other SF posts, please.

    http://arstechnica.com/information-technology/2015/05/sourceforge-grabs-gimp-for-windows-account-wraps-installer-in-bundle-pushing-adware/

    SourceForge grabs GIMP for Windows’ account, wraps installer in bundle-pushing adware

    1. Re:Obligatory /. Coverup Post - Again... by Lodlaiden · · Score: 1

      Thanks for the info. No mod points today.

      --
      Suborbital [spaceflight] is the special olympics of spaceflight. - Rei
  3. Re:Free labor only goes so far.. by BVis · · Score: 1

    Because that would be growing the size of government, and government jobs don't count anyway.

    --
    Never underestimate the power of stupid people in large groups.
  4. I really don't understand it and want to learn by onepoint · · Score: 1

    This is way over my head. I read the link, and got a grasp of the concept.
    but I want to learn more.
    Does anyone have something more detailed I could read and learn with ??
    thanks in advance.

    --
    if you see me, smile and say hello.
    1. Re:I really don't understand it and want to learn by JimWhiteheadUCSC · · Score: 5, Informative

      I'm one of the people involved in creating the Binary Fission game, so I can explain a little bit about what is going on "behind the scenes" in this game.

      In Binary Fission (http://binaryfission.verigames.com/), players use filters to try and make clean separations between piles of blue and gold colored dots ("bits"). It is usually the case that no one filter cleanly separates all of the blue bits from the gold bits, and hence solving a puzzle requires judicious use of filters to subdivide the piles into smaller piles, until you can find filters that do cleanly separate the smaller piles.

      Overall, the science goal of the game is to have players discover "loop invariant" conditions (http://en.wikipedia.org/wiki/Loop_invariant). This is a mathematical expression that describes (an approximation to) the behavior of a loop (for loop, while loop). For example, if a loop increments x by two each time through the loop, then a loop invariant would be x = {initial value of x} + {loop iteration count} * 2. At any point in the execution of the loop, this condition always holds. That is, the condition doesn't vary, and is "invariant".

      Behind the scenes, each of the bits (the dots) really represents a cluster of mappings of variables to values within a single iteration through a loop. One color of bits represents values of variables that are "good" -- they are consistent with the values that variables could have during loop execution. The other color of bits represents values of variables that are "bad" -- they are values that the variables could never have during loop execution.

      The filters represent possible loop invariant conditions. A strong loop invariant condition will perfectly separate the good values from the bad values, and thereby be a precise description of the behavior of the loop. Multiple combinations of filters can be combined together to create an aggregate loop invariant expression.

      One way of putting this is we're looking at finding loop invariants as a kind of classification problem, where we're trying to find the best possible classifier that will separate valid variable values from invalid variable values. The act of applying filters involves the player constructing a classifier.

      Right now, the filters in Binary Fission are candidate loop invariants that are output by the Daikon automated loop invariant finder (http://plse.cs.washington.edu/daikon/). These candidate invariants from Daikon are not usually good enough to describe the entire loop behavior, so the human player is using their unique judgement to augment the best output we get from automated invariant finder tools.

    2. Re:I really don't understand it and want to learn by onepoint · · Score: 1

      What a great Response, had to read it 3 times before I could get a basic grasp...
      What a cool idea all this is, play a game and somehow ( I know you explained it, but still don't grasp it all )
      it helps out solving something.

      Keep up the great Ideas and work

      --
      if you see me, smile and say hello.
  5. Re:Free labor only goes so far.. by Alumoi · · Score: 1

    We've gone beyond that.

    Just claim it's a beta for some big new game. People will pay you to work for them.

    It's already done. But they forget to tell you about the 'beta' part.

  6. Re:How much am I getting paid? by gnupun · · Score: 1

    The same amount you get paid every time you play a video game.

  7. Re:How much am I getting paid? by Lodlaiden · · Score: 1

    (not saying I'm the open source dev kinda guy, but if I was) It'd be a nice change of pace to set down building an open source app to play a game, and have a side effect be that it was able to validate the code I wrote.

    --
    Suborbital [spaceflight] is the special olympics of spaceflight. - Rei
  8. I have no idea what to do in these games by wonkey_monkey · · Score: 2

    I tried Paradox. No idea what's going on. Click, drag, click, something happens. Yay! What?

    I tried dynamakr as well. Even less of a clue. "Left Seek Similar Patterns!" "Enhance Energy!" And then it turns into some weird shoot 'em up. It feels like the game equivalent of a book translated from Swahili to English via Japanese.

    --
    systemd is Roko's Basilisk.
  9. Mathematical Proof by aaronkuchma · · Score: 1

    Let's get players to play tic-tac-toe, and we'll use the unique GameID they generate to annotate a number line to make a mathematical proof that the number line is infinite in the positive direction!

  10. SLASHDOT COVERUP by Scotsman,+True · · Score: 1

    Why did Dice buy Slashdot?

    So they could suppress discussions about their own scandals!

    SHAME ON YOU DICE!

  11. How much do I get paid? by plopez · · Score: 1

    Why should I be free labor. Nobody rides for free....

    --
    putting the 'B' in LGBTQ+
  12. Created an accout, tried to play, most are buggy by hackwrench · · Score: 1

    They need to fix their games so that you can actually play them. I tried some of them and one wouldn't run at all under IE, so I ran it under Chrome and got a little bit farther. That ones Monster Proof. I forget which one threw a dialog box error after getting through the first level and clicking Go to Next Level. Then there was one with text too small. Another had a light grey on dark grey thing for text and a glow around the text.

  13. Thanks for the example by q4Fry · · Score: 2

    I ran through a couple rounds of your game. I'm not trying to knock it, but if I may ask an ignorant question: If a computer can determine the value of structures created by a human, couldn't the computer generate structures and evaluate them much, much faster than a human (or even as many humans as you can muster to play the game)?