Мусаб А. Алтурки и Брэндон Мур

Формальная проверка программ, например проверка смарт-контрактов в системах блокчейна или проверка полетных контроллеров самолетов во встроенных устройствах, является мощным методом обеспечения правильности и повышения надежности систем. В этом контексте вопрос Зачем использовать «К, а не Coq?» кажется, довольно часто возникает при обсуждении K с коллегами, которые могут быть не знакомы с K, но слышали о Coq или использовали его раньше. В этой серии статей мы попытаемся выделить некоторые важные отличия K и Coq как формальных верификационных фреймворков для языков на рабочем примере. Мы надеемся объяснить читателю, почему мы считаем, что K больше подходит в этом контексте. Прежде чем мы продолжим, мы хотели бы отметить, что у нас есть большой опыт работы с Coq как в качестве пользователей, так и в качестве разработчиков библиотек/фреймворков.

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

K и Coq при проверке во время выполнения

И Coq, и K очень эффективны в качестве сред проверки языка, и мы в Runtime Verification регулярно используем их для предоставления наших услуг формального моделирования и проверки.

Примеры недавних разработок на основе K включают семантику виртуальной машины Ethereum KEVM и сгенерированный интерпретатор и дедуктивный верификатор, объединенные в набор инструментов Firefly, полное определение языка блокчейна IELE, конкретную модель Ethereum 2.0. Спецификация Beacon Chain» и KWasm: формальная исполняемая семантика Web Assembly, среди прочего.

Некоторые недавние разработки на основе Coq (не обязательно для проверки на основе языка) в Runtime Verification включают моделирование протокола Algorand и проверку его безопасности, а также моделирование и проверку механизма окончательности Ethereum в Casper. Мы также разработали независимую от языка структуру проверки программ в Coq, которую мы используем здесь для нашего рабочего примера, описанного в этом посте, который более подробно объясняется здесь.

Рабочий пример

Поскольку наша цель здесь — выделить некоторые из основных отличий при использовании K по сравнению с Coq для проверки программы, мы используем очень простой, но содержательный пример, которым является программа SUM ниже, написанная на императивном C-подобном языке, который мы называем IMP:

Важным свойством SUM, которое мы хотели бы проверить, является то, что после завершения переменная sum может иметь значение только (n + 1) n / 2 (которое представляет собой сумму целых значений от 1 до n) для любого неотрицательного числа. целое число n. Мы используем этот проверочный пример, чтобы проиллюстрировать, как K и Coq сравниваются и противопоставляются как языковые фреймворки, и даем читателю представление о рабочем процессе, связанном с этим процессом для каждого фреймворка.

Полная спецификация этого примера как на K, так и на Coq, а также скрипты проверки доступны здесь.

То, что нам нужно

Независимо от того, какую платформу мы выбираем для использования, для проверки правильности программ обычно необходимы следующие три артефакта:

  • Формальная модель L синтаксиса и семантики языка программирования, программы которого вы хотите проанализировать. Модель должна быть формальной, чтобы синтаксис и семантика были четко определены и недвусмысленны, и чтобы она позволяла формальные рассуждения. Более того, она должна быть на таком уровне абстракции, чтобы было достаточно легко рассуждать о том, насколько верна модель предполагаемой семантике языка. По сути, с этого момента L будет считаться IMP, и единственный способ ссылаться на значение конструкций IMP — через L.
  • Формальное представление P в этой модели анализируемой программы. Обычно это модель структуры программы в виде абстрактного синтаксического дерева (AST) или кодировка программы на каком-либо языке. При наличии вспомогательных инструментов (а именно, лексеров и парсеров, которые могут генерировать соответствующую спецификацию) это может быть и сам текст программы.
  • Спецификация S свойства, по которому должна быть проверена программа. В зависимости от модели и базовой формальной логики для проверки это могут быть, например, одна или несколько формул темпоральной логики, утверждения логики достижимости, предусловия и постусловия в тройках Хоара или формулы логики первого порядка или другие логические формализмы.

Итак, для SUM это означает, что нам потребуется:

  • Формальная модель семантики языка IMP, точно определяющая, что означают конструкции языка, такие как while и присваивание = (независимо от того, где они используются в программах).
  • Точная спецификация структуры программы SUM.
  • Формализация свойства, согласно которому вычисляемое значение действительно является суммой целых чисел от 1 до n.

Языковые фреймворки и обычные средства проверки программ

Полезно различать фреймворк, такой как Coq и K, и обычный верификатор программы. Обычные верификаторы программ созданы для конкретных языков программирования, таких как VCC для C, Verisol для Solidity и т. д., что означает, что семантика выбранного языка L зашита в самом инструменте. Более того, обычные верификаторы программ обычно также предоставляют специфичные для языка механизмы для извлечения структуры программы P из самой программы, а также спецификации S из удобных для пользователя синтаксических сахарных аннотаций к программе. Это делает верификатор программы более простым в использовании и более удобным для пользователя, но достигается за счет того, что инструмент по существу ограничен конкретным языком программирования (версией) и формализмом свойств, для которых он был создан. Любые изменения в языке программирования, например переход от одной версии к другой, или формализм свойств, например добавление новой логической конструкции или конструкции утверждения, требуют, чтобы весь инструмент проверки программы был обновлен его разработчиками или сопровождающими, если все еще доступен, а пользователи инструмента ждут, пока это будет сделано, а затем переключаются на принципиально новый инструмент.

Языковые фреймворки принципиально отличаются тем, что сами инструменты реализуются независимо от языков, к которым они применяются. Такое разделение ответственности позволяет разрабатывать и развивать инструменты независимо друг от друга, в то же время выделяя семантику языка как самостоятельный формальный артефакт, ценный сам по себе (см., например, EVM Jellopaper, который в настоящее время выступает в качестве канонической спецификации Ethereum). язык виртуальной машины). Плата за это — потенциально менее дружелюбная формальная нотация.

Таким образом, общий рабочий процесс проверки программы в языковой среде состоит в основном из следующих шагов:

  1. Формально определите структуру языка (синтаксис) и используйте его для определения структуры программы P.
  2. Определите формальную семантику языка и используйте разработанную языковую модель L (синтаксис и семантику) для изучения поведения программы.
  3. Задайте свойство S и убедитесь, что свойство S выполняется для P в L, или покажите, что оно не выполняется.

Это первая часть поста из трех частей. В оставшейся части первой части мы покажем, как формальные модели синтаксиса IMP и программы SUM могут быть построены в K и Coq (первый шаг описанного выше рабочего процесса). Определение семантики IMP и тестирование выполнения SUM (второй шаг) объясняется в Части 2. Третий шаг — задание и проверка свойства правильности — описан в Части 3.

Определение синтаксиса IMP

Первым шагом в определении формальной модели L языка является определение его синтаксических структур. Ниже мы определяем синтаксис языка IMP.

Определение синтаксиса в K

В основе K лежит логика Matching Logic, но он включает в себя несколько функций, специально разработанных для определения языков. Во-первых, синтаксис языка программирования может быть представлен в стандартном и широко распространенном формате BNF вместе со структурными и семантическими аннотациями, такими как аннотации ассоциативности и порядка вычисления. Например, арифметические выражения IMP определяются с использованием приведенных ниже правил производства:

Правила определяют синтаксическую категорию для арифметических выражений (вводится с помощью ключевого слова syntax). Терминал задается в виде строки в двойных кавычках, а нетерминал задается именем, начинающимся с заглавной буквы. Int и Id — нетерминалы для целых чисел и идентификаторов соответственно.

Используется несколько аннотаций: > обозначает приоритет среди операторов, left для левоассоциативного бинарного оператора и strict для указания порядка вычисления. Аннотация bracket означает, что круглые скобки ( ) используются только для группировки выражений и не должны создавать для них выделенные узлы в дереве синтаксического анализа (подробнее см. Учебник K). Обратите внимание, что Coq не нуждается в подобных аннотациях, поскольку Coq не занимается синтаксическим анализом.

Логические выражения BExp, такие как реляционные выражения, и программные операторы Stmt, такие как условные конструкции и циклические конструкции, определяются с использованием аналогичных правил производства.

Наконец, Pgm — это синтаксическая категория программ в IMP, и каждая синтаксически допустимая программа IMP, такая как SUM выше, имеет Pgm в качестве сортировки в этой спецификации ( Ids — это список идентификаторов):

Таким образом, программа в IMP состоит из последовательности объявлений переменных, за которыми следует оператор программы.

Полный K-модуль, определяющий синтаксис языка IMP, можно найти здесь.

Определение синтаксиса в Coq

В основе Coq лежит Исчисление индуктивных построений. Следовательно, для определения IMP наиболее естественным подходом является определение синтаксиса IMP с использованием индуктивно определенных типов данных и его семантики с использованием индуктивно определенных функций и отношений.

Например, синтаксис арифметических выражений в IMP может быть определен в Coq с помощью следующего объявления индуктивного типа, введенного с ключевым словом Inductive ( string и Z — строковые и целочисленные типы в Coq):

Как правило, каждая языковая конструкция, с помощью которой может быть построено арифметическое выражение в IMP, например. переменных, захватывается конструктором в типе AExp, который указывает типы его аргументов. Например, переменная создается конструктором var, применяемым к строке (имени переменной), а постоянное значение создается конструктором con, применяемым к целому числу. Используя это определение, выражение x + 2, например, представляется термом в Coq типа AExp, имеющим форму plus (var "x") (con 2).

Синтаксис логических выражений и инструкций в IMP определяется аналогичным образом с индуктивными типами BExp и Stmt соответственно. Например, конструктор оператора цикла while while : BExp -> Stmt -> Stmt принимает два аргумента: условие в виде логического выражения и тело цикла в виде оператора.

IMP-программа типа Pgm создается с помощью pgm, которая принимает в качестве аргументов список строк (объявляемых переменных) и оператор программы:

Полное определение Coq синтаксиса IMP (абстрактного) можно найти здесь.

Обратите внимание, что это кодирование программ IMP в термины в Coq соответствует построению деревьев синтаксического анализа программ. Однако этот процесс кодирования обязательно выполняется вручную, поскольку Coq не предоставляет функций, специфичных для анализа программ в терминах индуктивных типов (таких как ассоциативность или аннотации приоритета оператора в K). Кроме того, эти термины Coq (деревья синтаксического анализа) являются чисто синтаксическими. На данном этапе они не имеют семантической информации, связанной с ними. Например, в Coq нет облегчения в стиле K для указания строгости операторов или других стратегий оценки.

Спецификация SUM в K и Coq

Стиль BNF K для определения синтаксиса IMP и используемых аннотаций позволяет анализировать текст программы в абстрактном синтаксическом дереве (AST), которое однозначно определяет структуру программы. Таким образом, тяжелая работа по определению структуры программы автоматически выполняется синтаксическим анализатором K для IMP, созданным на основе спецификации синтаксиса BNF. Это означает, что сам текст программы может использоваться непосредственно для выполнения, проверки или любым другим инструментом K. Ниже мы даем имя sum_pgm параметрическое в n тексту программы:

Обратите внимание, что приведенное выше правило K, введенное с ключевым словом rule, определяет значение термина sum_pgm, применяемого к целочисленному значению. Например, sum_pgm 100 — это программа SUM с переменной n, инициализированной значением 100.

Однако в Coq программные тексты, такие как приведенная выше SUM, не могут быть использованы напрямую, и их необходимо разобрать на соответствующие термины, допустимые в модели Coq. Для небольших языков и программ, таких как IMP и SUM, эта задача синтаксического анализа довольно проста, но для более сложных языков и больших программ этот процесс обычно требует разработки внешних синтаксических анализаторов и генераторов спецификаций Coq, что может быть нетривиальной задачей.

В нашей модели Coq программа SUM имеет следующее представление в виде терма типа Pgm, который мы называем sum_pgm, как указано выше:

Конструкторы seq и assign обозначают соответственно операторы последовательности и присваивания в IMP (полное определение см. здесь).

Далее: семантика…

Теперь, когда у нас есть формальное определение синтаксиса IMP и формальное представление SUM, следующим шагом будет формальное определение семантики IMP и тестирование выполнения SUM с использованием этой семантики. Это описано далее в Части 2 этого поста.

Первоначально опубликовано на https://runtimeverification.com 12 декабря 2019 г.

Получайте лучшие предложения программного обеспечения прямо в свой почтовый ящик