Просматривать миллионы строк кода в поисках ошибки или уязвимости — сложный и неблагодарный труд. Но агентство по перспективным исследовательским проектам США (DARPA) решило привлечь к делу волонтёров, специально для которых весь процесс превратили в игру.
Новая краудсорсинговая инициатива DARPA Formal Verification предполагает использование труда добровольцев для обнаружения уязвимостей в коде ПО. Для этого агентство создало пять онлайновых игр и одну для iPad.
Вот как они работают: игры сделаны таким образом, что когда пользователь разгадывает загадку для того, чтобы перейти на следующий уровень, они, по-настоящему, генерируют аннотации к программному коду и выводят математические доказательства, которые могут доказать наличие или отсутствие ошибки в ПО, написанном на C или Java.
DARPA финансировала разработку этих игр. Если подвести итог, главное в них — разрешить действительно сложные математические проблемы в лёгкой игровой форме. Результаты, полученные с помощью них, помогут исследователям агентства обнаружить уязвимости в строчках кода, которым нужно пристальное внимание.