Система Maude: Логика переписывания для формальной верификации и анализа.

Введение

Система Maude — это реализация логики переписывания. Она схожа в общем подходе с реализацией OBJ3 уравнительной логики, разработанной Джозефом Гогеном, но основана на логике переписывания, а не на упорядоченной уравнительной логике, и делает сильный акцент на мощном метапрограммировании, основанном на рефлексии. Maude является свободным программным обеспечением, и в сети доступны обучающие материалы. Изначально она была разработана в SRI International, но сейчас разрабатывается совместными усилиями различных исследователей.

Введение

Maude решает задачи, отличные от тех, что решают обычные императивные языки, такие как C, Java или Perl. Это формальный инструмент для рассуждений, который может помочь нам проверить, соответствует ли система ожидаемому поведению, и указать причину несоответствия, если оно есть. Иными словами, Maude позволяет нам формально определить смысл понятий в очень абстрактной форме (не заботясь о том, как структура представлена внутри и т.д.), но при этом описывать, что считается равным в рамках нашей теории (уравнения) и какие изменения состояний возможны (правила переписывания). Модули Maude (теории переписывания) состоят из языка терминов, а также наборов уравнений и правил переписывания. Термины в теории переписывания строятся с использованием операторов (функций, принимающих ноль или более аргументов определенного типа и возвращающих термин определенного типа). Операторы, принимающие ноль аргументов, считаются константами, и язык терминов строится на основе этих простых конструкций. Maude позволяет пользователю указывать, являются ли операторы инфиксными, постфиксными или префиксными (по умолчанию), используя подчеркивания в качестве заполнителей для входных терминов. Уравнения восстановления предполагаются коллинеарными и завершающимися. Правила переписывания не имеют этого ограничения. При "выполнении" Maude переписывает термины в соответствии с уравнениями и правилами переписывания. Maude переписывает термины в соответствии с уравнениями, когда находится соответствие между переписываемым (или восстанавливаемым) закрытым термином и левой частью уравнения из нашего набора уравнений. Соответствие в данном контексте – это подстановка переменных в левой части уравнения, в результате которой она становится идентичной переписываемому/восстанавливаемому термину. Уравнения и правила переписывания могут быть также условными, то есть для их применения к термину необходимо выполнение определенных критериев (помимо простого соответствия левой части правила переписывания). Правила применяются системой Maude в "случайном" порядке, что означает, что нельзя гарантировать, какое правило будет применено раньше другого и так далее. Если к термину может быть применено уравнение, оно всегда будет применено раньше любого правила переписывания. Встроенный механизм поиска в Maude может находить нежелательные состояния и доказывать, что они недостижимы. Maude предоставляет возможность контролировать, какие правила следует применять на каждом шаге, используя метапрограммирование благодаря рефлексивным свойствам логики переписывания.

Maude sets out to solve a different set of problems than ordinary imperative languages like C, Java or Perl. It is a formal reasoning tool, which can help us verify that things are "as they should", and show us why they are not if this is the case. In other words, Maude lets us define formally what we mean by some concept in a very abstract manner (not concerning ourselves with how the structure is internally represented and so on), but we can describe what is thought to be the equal concerning our theory (equations) and what state changes it can go through (rewrite rules). Maude modules (rewrite theories) consist of a term language plus sets of equations and rewrite rules. Terms in a rewrite theory are constructed using operators (functions taking 0 or more arguments of some sort, which return a term of a specific sort). Operators taking 0 arguments are considered constants, and one constructs their term language by these simple constructs. Maude lets the user specify whether or not operators are infix, postfix or prefix (default), this is done using underscores as place fillers for the input terms. Reduction equations are assumed to be confluent and terminating. Rewrite rules do not have this restriction. When Maude "executes", it rewrites terms according to the equations and rewrite rules. Maude rewrites terms according to the equations whenever there is a match between the closed terms that one tries to rewrite (or reduce) and the left hand side of an equation in our equation set. A match in this context is a substitution of the variables in the left hand side of an equation which leaves it identical to the term that one tries to rewrite/reduce. Equations and rewrite rules can also be conditional rules, which means they have to fulfill some criteria to be applied to the term (other than just matching the left hand side of the rewrite rule). The rules are applied at "random" by the Maude system, meaning that you can not be sure that one rule is applied before another rule and so on. If an equation can be applied to the term, it will always be applied before any rewrite rule. Maude's built in search can look for unwanted states and show that no such states can be reached. Maude has the ability to control what rule applications should be attempted at each step using meta programming, due to the reflective property or rewriting logic.

Использование

Мод использовался для проверки безопасности протоколов и критически важного кода. Система Maude выявила уязвимости в криптографических протоколах, просто описывая возможности системы и обнаруживая нежелательные ситуации (состояния или термы, которые не должны возникать). Таким образом, можно показать, что протокол содержит ошибки, не связанные с ошибками программирования, а с ситуациями, которые сложно предсказать, просто следуя по "счастливому пути", как это обычно делают разработчики.