`

СПЕЦИАЛЬНЫЕ
ПАРТНЕРЫ
ПРОЕКТА

Архив номеров

Как изменилось финансирование ИТ-направления в вашей организации?

Best CIO

Определение наиболее профессиональных ИТ-управленцев, лидеров и экспертов в своих отраслях

Человек года

Кто внес наибольший вклад в развитие украинского ИТ-рынка.

Продукт года

Награды «Продукт года» еженедельника «Компьютерное обозрение» за наиболее выдающиеся ИТ-товары

 

Виталий Кобальчинский

Формальные методы знаменуют начало эры невзламываемого ПО

+11
голос

Метод, который позволяет разрабатывать программы, самой внутренней логикой защищённые от ошибок, называется формальная верификация. Каждая строка такой программы неизбежно следует из предшествующих, подобно строгому математическому доказательству теоремы.

Летом прошлого года этот стиль программирования, восходящий ещё к работам Дийкстры (Edsger Dijkstra) 40-летней давности, прошёл первую проверку боем. Команда хакеров «Red Team» на полигоне  Boeing в штате Аризона в течение шести недель пыталась через Wi-Fi получить контроль над системой управления полетом военного дрона Little Bird, аналога пилотируемой модели, используемой для армейских спецопераций.

Поначалу, взломать защиту оказалось не сложнее, чем у обычного беспроводного маршрутизатора, но затем инженеры, занятые в проекте High-Assurance Cyber Military Systems (HACMS) агентства DARPA заменили ключевые элементы программного обеспечения Little Bird кодом, написанным с применением формальной верификации. Несмотря на степень доступа к компьютерной сети дрона, о какой не могли бы и мечтать настоящие киберпреступники, «белым хакерам» так и не удалось добиться успеха.

«Вы пишете математическую формулу, которая определяет поведение программы, и используете некоторый инструмент, проверяющий правильность этого утверждения», – объясняет Брайан Парно (Bryan Parno), занимающийся вопросами формальной верификации и безопасности в Microsoft Research.

Долгое время осуществить что-нибудь подобное представлялось если не невозможным, то непрактичным, однако прогресс в так называемых «формальных методах» создал предпосылки для исследований прикладных аспектов формальной верификации. Сегодня совершенствованием этой технологии занимаются в рамках хорошо финансируемых академических программ с участием военных учреждений и крупных технологических компаний, таких как Microsoft и Amazon.

Год спустя после аризонского эксперимента DARPA продвигает инструменты и методики из проекта HACMS в другие области военных технологий, такие как спутники и грузовые транспорты с автономным управлением для конвоев.

За последнее десятилетие исследователи уже создали множество доказанно безопасных компонентов, включая ядра операционной системы, и родственный HACMS проект DeepSpec, если он увенчается успехом, должен связать эти компоненты вместе, получив полностью верифицированную комплексную систему, такую как, например, веб-сервер. DeepSpec получил грант в 10 млн долл. от Национального научного фонда США.

Программные инженеры в Microsoft Research также работают над двумя амбициозными проектами формальной верификации. Задача одного из них, под названием Everest, состоит в создании верифицированной версии HTTPS, второго – в разработке верифицированных спецификаций сложных кибер-физических систем, таких как дроны.

+11
голос

Напечатать Отправить другу

Читайте также

 
 
IDC
Реклама

  •  Home  •  Рынок  •  ИТ-директор  •  CloudComputing  •  Hard  •  Soft  •  Сети  •  Безопасность  •  Наука  •  IoT