.jpg)
В DARPA, похоже, нашли способ упростить процесс поиска уязвимостей в программном обеспечении для Пентагона: в агентстве создали сайт с набором компьютерных игр-головоломок, решая которые, вы на самом деле решаете задачи формальной верификации кода. Как объясняют в DARPA, определенные виды брешей, например, переполнение буфера и уязвимости, вызывающие подъем уровня привилегий, «особенно хорошо проецируются на головоломки».
В одной из игр, например, вы исследуете тропический остров, каталогизируя встречающиеся вам по пути неизвестные растения (которые в реальности являются воплощениями фрагментов кода). В другой нужно комплектовать команды роботов для выполнения некоторой миссии, а в третьей задача — оптимизировать топологию кабельной сети таким образом, чтобы обеспечить максимальную пропускную способность.
Как объясняют в DARPA, нынешний набор игр обеспечивает поиск брешей в реальных программах с открытым кодом на Си и Java, применяемых в госструктурах и коммерческих компаниях. Основная работа по формальной верификации выполняется автоматически, а в головоломки для «игровой» проверки преобразуют участки кода, отмеченные автоматизированными средствами в качестве ненадежных. Если в процессе игры вы помогли обнаружить ошибку, о ней уведомляют разработчиков.
