Cameleer: инструмент дедуктивной проверки для OCaml

От социальных сетей до освоения космоса программное обеспечение является основой, благодаря которой наш мир функционирует. Но откуда мы знаем, что программному обеспечению можно доверять? Доктор Марио Перейра из Школы науки и технологий Нова в Лиссабоне и его сотрудники разработали Cameleer, программный инструмент для формальной проверки написанного на OCaml кода, который устанавливает математическое доказательство того, что система работает в соответствии со спецификациями программиста. Cameleer – это первый инструмент автоматизированной дедуктивной проверки программ, написанных на OCaml.

Мир стал зависимым от программного обеспечения. От его использования в повседневных задачах, таких как социальные сети, до очень важных миссий, таких как исследование космоса, программное обеспечение является основой, которая поддерживает наш мир. Разработка программного обеспечения — деятельность, подверженная ошибкам, не говоря уже о ее подверженности вредоносным атакам. Дефектное программное обеспечение может иметь неприятные и дорогостоящие последствия. Например, в 2015 году произошел сбой во время ежедневного обновления системы в точках продаж 7000 магазинов Starbucks в США и 1000 в Канаде. Сотрудники не могли принимать платежи по картам или регистрировать сдачу, поэтому были вынуждены раздавать клиентам бесплатный кофе и чай. Хотя через несколько часов проблема была решена, сообщается, что в тот день Starbucks потеряла от трех до четырех миллионов долларов. Другой пример произошел в 2008 году, когда открылся новый Терминал 5 Хитроу, а вместе с ним и обещание современной, эффективной и функционирующей системы обработки багажа. Система была протестирована перед открытием с более чем 12 000 единиц багажа и работала отлично. Когда терминал открылся для публики, система не смогла справиться с огромным количеством ежедневно регистрируемого багажа, и всего через десять дней после ее запуска было потеряно около 42 000 сумок и отменено более 500 рейсов.

Так откуда мы знаем, что мы можем доверять программному обеспечению? Один из ответов — тестирование надежности программного обеспечения. Однако такие тесты охватывают лишь часть возможных запусков, которые программа будет запускать на практике. Лучшее решение предполагает включение надежных математических гарантий в процесс разработки программного обеспечения. «Формальные методы» — это область компьютерных наук, которая отстаивает этот подход, используя строгие математические рассуждения и методы моделирования для описания и сертификации частей компьютерной инфраструктуры и обеспечения формальной проверки программного обеспечения. В соответствии с этой практикой д-р Марио Перейра и д-р Антониу Равара из Новой школы науки и технологий в Лиссабоне и их сотрудники разработали инструмент Cameleer, программный инструмент для формальной проверки кода, написанного на OCaml.

Дедуктивная верификация программного обеспечения
Дедуктивная верификация программного обеспечения включает в себя выражение правильности кода в наборе математических утверждений, известных как условия верификации, а затем их доказательство. Перейра объясняет, как это включает в себя логическую спецификацию, прикрепленную к коду. Логическая спецификация — это описание, написанное на математическом языке, свойств, которые программа должна соблюдать в определенные моменты своего выполнения. Наконец, реализован алгоритм генератора условий проверки. Это берет код вместе с его спецификацией и создает условия проверки. Доказательство этих математических утверждений формально устанавливает, что выполнение программы подчиняется логическим свойствам, описанным в ее спецификации. Перейра отмечает, что, несмотря на успехи в дедуктивной верификации и автоматизации доказательств в последние десятилетия, семейству функциональных языков, используемых для построения программ путем применения и составления функций, уделялось мало внимания.

Лучшее решение предполагает включение надежных математических гарантий в процесс разработки программного обеспечения.

OCaml
Одним из таких функциональных языков является OCaml, промышленный язык программирования, разработанный в парижском исследовательском центре Inria. OCaml используется для внедрения программного обеспечения, такого как помощники по проверке, автоматические решатели и компиляторы, в промышленности по всему миру такими организациями, как Facebook, Bloomberg и Issuu. OCaml — мультипарадигмальный язык, поддерживающий функциональное, императивное и объектно-ориентированное программирование. Он имеет надежный механизм сопоставления с образцом, гибкую модульную систему и автоматическое управление памятью, поэтому его можно использовать для написания эффективных модульных программ, поддерживающих безопасность типов (предотвращающих ошибки типов, вызванные несоответствиями между разными типами данных) и работающими с побочные эффекты, такие как мутация памяти.

Несмотря на то, что эти факторы делают код OCaml подходящим для формальной проверки, дедуктивная проверка редко используется с программами OCaml, объясняет Перейра. Более того, до проекта Cameleer не существовало инструмента автоматической проверки, который мог бы напрямую работать с кодом, написанным на OCaml. До сих пор программистам OCaml, решившим использовать автоматизацию проверки, приходилось изучать язык, поддерживающий проверку, писать на нем программы, а затем выполнять извлечение кода. Альтернативой было использование инструментов, которые требовали ручной проверки.

GOSPEL
Язык спецификаций — это формальный язык, используемый во время разработки программного обеспечения, который обеспечивает точную спецификацию на разных уровнях. Требуется провести формальную верификацию программного обеспечения. Язык спецификации определяет семантику и структуру программной системы и используется во время формальной проверки для предоставления математического доказательства того, что система работает в соответствии с предыдущими спецификациями.

Вместе с доктором Артуром Шаргеро, доктором Жаном-Кристофом Филлиатром и доктором Клаудио Бело Лоуренсо (Charguéraud et al, 2019) Перейра разработал язык спецификаций для OCaml под названием GOSPEL — Generic Ocaml SPEcification Language. С тех пор GOSPEL превратился в зрелый проект, который в настоящее время разрабатывается большим консорциумом исследователей, в который входят Клеман Паскутто, Николя Осборн, доктор Франсуа Потье и доктор Армаэль Гено. GOSPEL предназначен для облегчения проверки структур данных и алгоритмов. Он имеет формальную семантику, которая определяется путем перевода в логику разделения, форму рассуждений о программах. GOSPEL предлагает высокоуровневый краткий синтаксис, доступный для программистов, не знакомых с логикой разделения. Хотя GOSPEL был разработан для спецификации кода OCaml, он также предназначен как общий инструмент для проверки и тестирования с функциями, которые можно применять к другим языкам программирования.

Cameleer — это мощная, удобная и в основном автоматизированная система проверки для сообщества OCaml.

Cameleer
Исследователи разработали Cameleer, первый инструмент автоматизированной дедуктивной проверки программ, написанных на OCaml. Они выбрали GOSPEL в качестве языка спецификации, чтобы иметь возможность назначать удобочитаемую, строгую поведенческую спецификацию для кода OCaml. Cameleer фокусируется на автоматизации проверки и использует программу OCaml с аннотациями GOSPEL в качестве входных данных. Он переводит это в WhyML. WhyML — это язык программирования и спецификаций для Why3, платформы для дедуктивной проверки программного обеспечения и, в частности, автоматизированного доказательства. Генератор условий проверки Why3 создает набор условий проверки, которые отправляются различным решателям, где выполняются формальные доказательства.

Перейра и его коллеги решили разработать инструмент проверки Cameleer, чтобы принимать в качестве входных данных программы, написанные непосредственно на OCaml, а не на специальном языке проверки. Это означает, что пользователю не нужно переписывать весь исходный код OCaml исключительно для проведения формальной проверки. На протяжении всего процесса проверки пользователю нужно только написать код OCaml и спецификацию GOSPEL. Cameleer был разработан таким образом, что другие элементы генерируются автоматически; впоследствии пользователю не нужно беспокоиться о программе, созданной в WhyML. Пользователь участвует только на начальном этапе определения и на последнем этапе процесса, где он помогает Why3 закрыть доказательство.

Чтобы оценить производительность и удобство использования Cameleer, исследователи составили тестовый набор тематических исследований, состоящий из более чем 1000 строк кода OCaml. К ним относятся реализации из существующих библиотек, такие как числовые программы, сортировка и поиск, логические алгоритмы, сканирование массивов, реализации более высокого порядка и несколько исторических алгоритмов. Все они были успешно проверены с помощью инструмента Cameleer. Перейра добавляет, что только эта коллекция тематических исследований вносит свой вклад в создание всеобъемлющей совокупности проверенных кодовых баз OCaml.

Расширяя границы проверки программного обеспечения
Перейра описывает, как исследователи, работающие над проектом Cameleer, продолжают расширять границы формальной проверки программного обеспечения. Они разрабатывают принципы и инструменты для применения дедуктивной верификации к коду, написанному на OCaml. На сегодняшний день они создали надежный инструмент, который может обрабатывать код OCaml и автоматически проверять, соответствует ли он спецификации, написанной в GOSPEL. Их работа продолжается над созданием «мощной, удобной и в основном автоматизированной системы проверки для сообщества OCaml», что делает проверку более доступной для программистов, использующих OCaml, в том числе для тех, кто не является экспертом по проверке. О следующих шагах в своем исследовании Перейра говорит: «Наша конечная цель — превратить Cameleer в инструмент проверки, который может одновременно использовать лучшие функции различных сред промежуточной проверки».

Личный ответ

Как вы думаете, почему кто-то до сих пор не разработал инструмент автоматической проверки, который может работать непосредственно с кодом, написанным на OCaml?

Во-первых, позвольте мне заявить о существовании CFML, замечательного инструмента проверки, который может работать с кодом OCaml. Однако CFML требует высокой степени взаимодействия с человеком, чего можно ожидать только от экспертов по формальным методам, а не от обычных программистов.

Возвращаясь к вопросу, литература включает множество инструментов автоматической проверки, но нацеленных на императивные языки, такие как C/C++, Java и так далее. Я искренне верю, что это связано с тем фактом, что промышленность (и, в частности, критическая промышленность) гораздо больше использовала императивные (иногда низкоуровневые) языки, поскольку они изображали функциональные языки как «слишком академические» или «не соответствующие требованиям». job» (с точки зрения эффективности, гибкости, ремонтопригодности и т. д.). Теперь правда в том, что функциональные языки выросли из небольших исследовательских проектов в полноценные основные языки, следовательно, набирают обороты в промышленности. Поэтому сейчас самое подходящее время для того, чтобы инвестировать в формальную проверку функциональных программ, так как я верю, что все больше и больше программистов захотят использовать функциональные языки и формальные методы в своей повседневной работе.

Ссылки

Перейра М., Равара А. (2021) Cameleer: инструмент дедуктивной проверки для OCaml. В: Silva, A, Leino, KRM, (eds) Computer Aided Verification. CAV 2021. Lecture Notes in Computer Science, vol 12760. Springer, Cham. doi.org/10.1007/978–3–030–81688–9_31

Шаргеро, А., Филлиатр, Дж., Лоуренсу, К., Перейра, М., (2019) ЕВАНГЕЛИЕ — Предоставление OCaml языка формальных спецификаций. In: McIver, A, ter Beek, M, (eds) FM 2019, 23-й международный симпозиум по формальным методам, Порту, Португалия, октябрь 2019 г.

Перейра, М. (2018) Инструменты и методы проверки модульного кода с отслеживанием состояния. Тезисы, Парижский университет Сакле (COMUE).

Основы исследования

Д-р Марио Перейра является младшим научным сотрудником в Новой школе науки и технологий в Лиссабоне с 2020 года. В марте 2022 года он был назначен ассистентом профессора на постоянной основе. Он работает в Лаборатории компьютерных наук и информатики NOVA (NOVA LINCS) Лиссабонского университета NOVA. Доктор Перейра защитил докторскую диссертацию в 2018 году под руководством Жана-Кристофа Фийатра в Университете Париж-Сакле. Он является экспертом в области дедуктивной проверки программного обеспечения и функционального программирования, а также архитектором и ведущим разработчиком инструмента Cameleer. Он также является активным членом команд разработки Why3 и GOSPEL.

Цели исследования

Доктор Перейра и его сотрудники разработали инструмент Cameleer, программное обеспечение для формальной проверки кода, написанного на OCaml.

Финансирование

  • H2020-ЕС.1.3.2. Развитие совершенства посредством трансграничной и межотраслевой мобильности
  • Индивидуальные стипендии MSCA-IF-2019 (идентификатор соглашения о гранте: 897873)
  • ВОКАЛ ANR-15-CE25–008

Соавторы

О разработке Cameleer:

  • Антонио Равара (ctp.di.fct.unl.pt/~aravara)
  • Симао Мелу де Соуза (www.di.ubi.pt/~desousa)
  • Тьяго Соарес (ученик)
  • Даниэль Кастаньо (студент)
  • Карлос Пинто (студент)

О развитии ЕВАНГЕЛИЯ: