Формальная Верификация

Введение

Формальная верификация - это процесс использования формальных определений для проверки соответствия программы определенным спецификациям (техническим характеристикам). Другими словами, он использует математику для ответа на вопрос: «Удалось ли нам сделать то, что мы пытались сделать?»

Для сравнения, в настоящее время программисты пишут модульные тесты, чтобы убедиться в соответствии программы определенным характеристикам. Они тестируют программу с максимально возможным количеством вводов, проверяя каждый раз соответствие ввода указанным спецификациям. Например, чтобы проверить, правильно ли программа сортирует список чисел по возрастанию, она будет проверена с помощью ввода [2, 3, 1]. Результат должен выдать: [1, 2, 3], в противном случае, программа будет считаться недействительной.

Тем не менее, подход модульного тестирования может не учесть все возможные вводимые данные (или пограничные случаи), что может привести к отказу программы. Решение этой проблемы - формальная верификация. Формальная верификация предполагает написание математических определений программы. Используя тот же пример, что и выше, можно написать определение: «Для каждого элемента j в списке убедитесь, что элемент j ≤ j+1». Это огромный шаг вперед по сравнению с модульными тестами, поскольку правильность программы оказывается математически универсальной.

Michelson с GADT

GADT расшифровывается как Обобщенные алгебраические типы данных. GADT позволяют разработчикам OCaml описывать отношения между конструкторами данных и типами, в которых они обитают. В настоящее время язык Michelson использует GADT (Обобщенные алгебраические типы данных) для формальной верификации типов.

Michelson с Coq

Coq - это интерактивное средство доказательства теорем. Он основан на очень выразительной логике, называемой Исчислением Индуктивных Построений, которая достаточно мощна, чтобы доказывать сложные математические теоремы, такие как теорема Фейта-Томпсона о нечетном порядке, и проверять правильность сложного программного обеспечения, такого как CompCert. Более конкретно, Coq позволяет:

• определить функции или предикаты, которые можно эффективно оценить;

• излагать математические теоремы и технические условия ПО;

• интерактивно разрабатывать формальные доказательства этих теорем;

• проверять эти доказательства с помощью сравнительно небольшого «ядра» сертификации;

• извлекать сертифицированные программы на такие языки, как Objective Caml, Haskell или Scheme.

Mi-Cho-Coq - это формализация языка смарт-контрактов Майкельсона в Coq. Его можно использовать для определения и проверки смарт-контрактов Tezos, таких как этот контракт с несколькими подписями, контракт «менеджера» по умолчанию и контракт с лимитом расходов кошелька Cortez. Mi-Cho-Coq также служит целью компиляции для компилятора Albert.

Почему это важно для финансовых контрактов?

Смарт-контракты являются программами, содержащими определенную сумму денег. Поэтому очень важно, чтобы они были безошибочными и точными. Модульного тестирования недостаточно, чтобы охватить все пограничные случаи и ошибки, которые могут возникнуть.

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

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

Материалы разработаны TQ Tezos переведены на русский язык Tezos Ukraine