Формальна Верифікація
Формальна верифікація - це процес використання формальних визначень для перевірки відповідності програми певним специфікаціям (технічними характеристиками). Іншими словами, він використовує математику для відповіді на питання: «Чи вдалося нам зробити те, що ми намагалися зробити?»
Для порівняння, наразі програмісти пишуть модульні тести, щоб переконатися у відповідності програми певним характеристикам. Вони тестують програму з максимально можливою кількістю вводів, перевіряючи кожен раз відповідність введення зазначеним специфікаціям. Наприклад, щоб перевірити, чи правильно програма сортує список чисел за зростанням, її буде перевірено за допомогою введення
[2, 3, 1]. Результат повинен видати: [1, 2, 3], в іншому випадку, програма вважатиметься недійсною.Тим не менш, підхід модульного тестування може не врахувати всі можливі дані, що вводяться (або граничні випадки), що може призвести до відмови програми. Вирішення цієї проблеми - формальна верифікація. Формальна верифікація передбачає написання математичних визначень програми. Використовуючи приклад, наведений вище, можна написати визначення: «Для кожного елемента j в списку переконайтеся, що елемент j ≤ j + 1». Це величезний крок вперед в порівнянні з модульними тестами, оскільки правильність програми виявляється математично універсальною.
GADT розшифровується як Узагальнені алгебраїчні типи даних. GADT дозволяють розробникам OCaml описувати відносини між конструкторами даних і типами, в яких вони мешкають. На даний момент мова Michelson використовує GADT (Узагальнені алгебраїчні типи даних) для формальної верифікації типів.
Coq - це інтерактивний засіб доведення теорем. Він заснований на дуже виразній логіці, названій Обчисленням Індуктивних побудови, яка досить потужна, щоб доводити складні математичні теореми, такі як теорема Фейта-Томпсона про непарний порядок, і перевіряти правильність складного програмного забезпечення, такого як CompCert. Більш конкретно, Coq дозволяє:
- визначити функції або предикати, які можна ефективно оцінити;
- викладати математичні теореми і технічні умови ПО;
- інтерактивно розробляти формальні докази цих теорем;
- перевіряти ці докази за допомогою порівняно невеликого «ядра» сертифікації;
- вилучати сертифіковані програми на такі мови, як Objective Caml, Haskell або Scheme.
Mi-Cho-Coq - це формалізація мови смарт-контрактів Майкельсона в Coq. Його можна використовувати для визначення та перевірки смарт-контрактів Tezos, таких як цей контракт з декількома підписами, контракт «менеджера» за замовчуванням і контракт з лімітом витрат гаманця Cortez. Mi-Cho-Coq також служить метою компіляції для компілятора Albert.
Смарт-контракти є програмами, що містять певну суму грошей. Тому дуже важливо, щоб вони були безпомилковими і точними. Модульного тестування недостатньо, щоб охопити всі граничні випадки і помилки, які можуть виникнути.
Складні фінансові контракти включають кроки і процеси, які стосуються довіри сторін-учасниць, а також сторін, зацікавлених в надійності системи, на якій побудований контракт. Неправильно складений контракт може порушити довіру до системи. У гірших випадках ненавмисні програмні збої можуть призвести до втрати грошей, як це сталося з Ethereum.
Завдяки формальній верифікації, програмісти і розробники можуть незаперечно довести відсутність помилок в деяких програмах. Вони можуть зробити це з впевненістю і точністю математика, який бажає довести теорему. Ці вдосконалення застосовуються для забезпечення безпеки в бу дь-яких сферах: від безпілотників до Інтернету.
Last modified 2yr ago