Агентство DARPA экспериментирует с созданием игр для верификации надёжности открытого ПО
10 июня 2014 года
Агентство по перспективным оборонным научно-исследовательским разработкам США (DARPA) проводит эксперименты с созданием online-игр, позволяющих привлечь обычных пользователей для верификации надёжности и безопасности открытого ПО. Экспертов для проведения аудита качества кода не хватает, поэтому DARPA рассматривает варианты привлечения к проверке кода обычных пользователей, косвенно используя игровой процесс для организации верификации.
В настоящее время уже подготовлено (Архивная копия от 17 февраля 2020 на Wayback Machine) пять игр (CircuitBot, Flow Jam, Ghost Map, StormBound, Xylem), которые мало отличаются по игровому процессу от типичных логических игр и головоломок. Как правило, задачей игрока является поиск оптимального пути, разбор запутанных комбинаций и организация взаимодействия между игровыми объектами. При этом, проходя множество игровых уровней пользователи невольно участвуют в процессе формальной верификации, подтверждающей надёжность работы тех или иных участков кода, взаимодействие с которыми вовлечено в игровую логику.
Игровые приложения, в которых изначально отражены математические модели исследуемых приложений, транслируют действия пользователя в программные аннотации и генерируют математические доказательства, позволяющие убедиться в отсутствии различных классов дефектов в коде на языках Си и Java. Программа формальной верификации (CSFV, Crowd Sourced Formal Verification) нацелена на подтверждение безопасности серии открытых проектов, используемых в военных и государственных учреждениях, а также в критичных к надёжности областях коммерческого сектора.
Проходящие верификацию открытые проекты не называются явно, но в опубликованном несколько лет назад документе о проведении конкурса на разработку технологии формальной верификации упоминались ядро Linux, BIND и Hadoop. Заявлено (Архивная копия от 22 сентября 2015 на Wayback Machine), что все выявляемые в процессе верификации ошибки оперативно сообщаются основным разработчикам проектов.
Источники
править
Любой участник может оформить статью: добавить иллюстрации, викифицировать, заполнить шаблоны и добавить категории.
Любой редактор может снять этот шаблон после оформления и проверки.
Комментарии
Если вы хотите сообщить о проблеме в статье (например, фактическая ошибка и т. д.), пожалуйста, используйте обычную страницу обсуждения.
Комментарии на этой странице могут не соответствовать политике нейтральной точки зрения, однако, пожалуйста, придерживайтесь темы и попытайтесь избежать брани, оскорбительных или подстрекательных комментариев. Попробуйте написать такие комментарии, которые заставят задуматься, будут проницательными или спорными. Цивилизованная дискуссия и вежливый спор делают страницу комментариев дружелюбным местом. Пожалуйста, подумайте об этом.
Несколько советов по оформлению реплик:
- Новые темы начинайте, пожалуйста, снизу.
- Используйте символ звёздочки «*» в начале строки для начала новой темы. Далее пишите свой текст.
- Для ответа в начале строки укажите на одну звёздочку больше, чем в предыдущей реплике.
- Пожалуйста, подписывайте все свои сообщения, используя четыре тильды (~~~~). При предварительном просмотре и сохранении они будут автоматически заменены на ваше имя и дату.
Обращаем ваше внимание, что комментарии не предназначены для размещения ссылок на внешние ресурсы не по теме статьи, которые могут быть удалены или скрыты любым участником. Тем не менее, на странице комментариев вы можете сообщить о статьях в СМИ, которые ссылаются на эту заметку, а также о её обсуждении на сторонних ресурсах.
