Войти
OpenNet

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

1719
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
Материал размещён правообладателем в открытом доступе
  • В новости упоминаются
Страны
Компании
Проекты
Хотите оставить комментарий? Зарегистрируйтесь и/или Войдите и общайтесь!
ПОДПИСКА НА НОВОСТИ
Ежедневная рассылка новостей ВПК на электронный почтовый ящик
  • Разделы новостей
  • Обсуждаемое
    Обновить
  • 09.05 13:19
  • 1
Трамп заявил, что «хорошим стимулом» для РФ прекратить войну на Украине может стать участие в ЧМ по футболу 2026
  • 09.05 12:57
  • 193
Конкурента российского Су-75 из Южной Кореи впервые представили на выставке
  • 09.05 11:53
  • 1
Поляки выбирают: президент «здравого смысла» или личный враг Путина
  • 09.05 04:34
  • 8790
Без кнута и пряника. Россия лишила Америку привычных рычагов влияния
  • 09.05 04:18
  • 7
Индия при ударах по Пакистану использовала ракеты SCALP, авиационные бомбы Hammer, барражирующие боеприпасы - СМИ
  • 09.05 04:13
  • 30
Российские системы ПВО: первый опыт реального боевого применения
  • 08.05 19:24
  • 27
МС-21 готовится к первому полету
  • 08.05 19:13
  • 41
Командующий ВВС США в Европе о роли авиации в боевых действиях на Украине
  • 08.05 18:48
  • 2
Путин подписал договор о всеобъемлющем стратегическом партнерстве РФ и Ирана
  • 08.05 17:32
  • 146
Без пилота охота: вертолеты будут охранять небо России от дронов
  • 08.05 11:00
  • 1
Вэнс: США считают, что РФ просит по Украине слишком много, но хочет мира
  • 08.05 08:12
  • 101
«Не в пользу российской машины»: 38-й НИИИ БТ МО завершил испытания трофейной американской БМП Bradley M2A2 ODS SA
  • 08.05 00:32
  • 1
Это наша Победа
  • 07.05 21:30
  • 0
Ответ на "Латвийские настроения. Часть 1"
  • 07.05 19:32
  • 1
Неприемлемый ущерб: теория, практика и индивидуальность