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

Вступ

Формальна верифікація - це процес використання формальних визначень для перевірки відповідності програми певним специфікаціям (технічними характеристиками). Іншими словами, він використовує математику для відповіді на питання: «Чи вдалося нам зробити те, що ми намагалися зробити?»

Для порівняння, наразі програмісти пишуть модульні тести, щоб переконатися у відповідності програми певним характеристикам. Вони тестують програму з максимально можливою кількістю вводів, перевіряючи кожен раз відповідність введення зазначеним специфікаціям. Наприклад, щоб перевірити, чи правильно програма сортує список чисел за зростанням, її буде перевірено за допомогою введення [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