Войти
OpenNet

Агентство DARPA экспериментирует с созданием игр для верификации надёжности открытого ПО

1730
0
+1
CircuitBot
Компьютерная игра CircuitBot.
Источник изображения: www.verigames.com

Агентство по перспективным оборонным научно-исследовательским разработкам США (DARPA) проводит эксперименты с созданием online-игр, позволяющих привлечь обычных пользователей для верификации надёжности и безопасности открытого ПО. Экспертов для проведения аудита качества кода не хватает, поэтому DARPA рассматривает варианты привлечения к проверке кода обычных пользователей, косвенно используя игровой процесс для организации верификации.


В настоящее время уже подготовлено пять игр (CircuitBot, Flow Jam, Ghost Map, StormBound, Xylem), которые мало отличаются по игровому процессу от типичных логических игр и головоломок. Как правило, задачей игрока является поиск оптимального пути, разбор запутанных комбинаций и организация взаимодействия между игровыми объектами. При этом, проходя множество игровых уровней пользователи невольно участвуют в процессе формальной верификации, подтверждающей надёжность работы тех или иных участков кода, взаимодействие с которыми вовлечено в игровую логику.


Игровые приложения, в которых изначально отражены математические модели исследуемых приложений, транслируют действия пользователя в программные аннотации и генерируют математические доказательства, позволяющие убедиться в отсутствии различных классов дефектов в коде на языках Си и Java. Программа формальной верификации (CSFV, Crowd Sourced Formal Verification) нацелена на подтверждение безопасности серии открытых проектов, используемых в военных и государственных учреждениях, а также в критичных к надёжности областях коммерческого сектора.


Проходящие верификацию открытые проекты не называются явно, но в опубликованном несколько лет назад документе о проведении конкурса на разработку технологии формальной верификации упоминались ядро Linux, BIND и Hadoop. Заявлено, что все выявляемые в процессе верификации ошибки оперативно сообщаются основным разработчикам проектов.


Права на данный материал принадлежат OpenNet
Материал размещён правообладателем в открытом доступе
  • В новости упоминаются
Страны
Компании
Проекты
Хотите оставить комментарий? Зарегистрируйтесь и/или Войдите и общайтесь!
ПОДПИСКА НА НОВОСТИ
Ежедневная рассылка новостей ВПК на электронный почтовый ящик
  • Разделы новостей
  • Обсуждаемое
    Обновить
  • 01.06 00:59
  • 1
Ответ на "Ковальчук: москитный флот для РФ имел бы преимущества перед большими кораблями"
  • 31.05 21:39
  • 9025
Без кнута и пряника. Россия лишила Америку привычных рычагов влияния
  • 31.05 21:07
  • 6
SCMP: Эксперты предполагают, что секретный китайский истребитель J-36 не предназначен для ведения воздушного боя
  • 31.05 20:29
  • 1
У России есть стратегический резерв для отражения атак украинских БПЛА
  • 31.05 20:07
  • 1
Запущенная с "Иноходца" ракета Х-БПЛА (ТКБ-1030) сожгла бронемашину ВСУ
  • 31.05 20:01
  • 1
На Западе у российского ударного «Охотника» обнаружили «неожиданную проблему»
  • 31.05 13:18
  • 67
Какое оружие может оказаться эффективным против боевых беспилотников
  • 31.05 06:44
  • 102
Будущее за тяжелыми "противоснарядными" БМП весом в 55 тонн
  • 31.05 05:38
  • 0
Ответ на "Полковник раскрыл особенности ударивших по Украине российских «Калибров»"
  • 31.05 02:21
  • 1
Шойгу: вооружение РФ прошло испытание боем и крайне востребовано в мире
  • 30.05 21:09
  • 0
Еще одна "не самая новая" статья о флоте (о ЧФ)
  • 30.05 18:54
  • 0
По поводу "У России есть стратегический резерв для отражения атак украинских БПЛА"
  • 30.05 16:42
  • 32
Российский сверхзвуковой пассажирский самолет — преемник Ту-144 — будет летать со скоростью 2500 км/ч на расстояние свыше 8500 км
  • 30.05 13:19
  • 1
Медведев: в воинские части с начала года прибыли почти 175 тыс. военнослужащих
  • 30.05 06:35
  • 11
Зачем и без того мощной авиационной ракете «ядерная» модернизация?