Вступ

Безпека Bitcoin та інших блокчейнів, таких як Liquid, залежить від використання алгоритмів цифрових підписів, таких як ECDSA та підписи Шнора. Бібліотека C під назвою libsecp256k1, названа на честь elliptic curve, на якій працює бібліотека, використовується як Bitcoin Core, так і Liquid для надання цих алгоритмів цифрових підписів. Ці алгоритми використовують математичне обчислення, зване модульним оберненням, яке є відносно дорогим компонентом обчислення.

У 'Швидка обчислення gcd з постійним часом та модульне обернення', Деніел Дж. Бернштейн та Бо-Їн Янг розробляють новий алгоритм модульного обернення. У 2021 році цей алгоритм, відомий як 'safegcd', був реалізований для libsecp256k1 Пітером Деттманом. Як частина процесу перевірки цього нового алгоритму, Blockstream Research став першим, хто завершив формальну перевірку дизайну алгоритму, використовуючи асистента доведення Coq, щоб формально перевірити, що алгоритм дійсно завершується з правильним результатом модульного обернення для 256-бітних вхідних даних.

Розрив між алгоритмом і реалізацією

Зусилля з формалізації у 2021 році лише продемонстрували, що алгоритм, розроблений Бернштейном і Янгом, працює правильно. Однак використання цього алгоритму в libsecp256k1 вимагає реалізації математичного опису алгоритму safegcd у мові програмування C. Наприклад, математичний опис алгоритму виконує множення матриць векторів, які можуть бути настільки широкими, як 256-бітні знакові цілі числа, однак мова програмування C надасть цілі числа лише до 64 біт (або 128 біт із деякими розширеннями мови).

Реалізація алгоритму safegcd вимагає програмування множення матриць та інших обчислень за допомогою 64-бітних цілих чисел C. Крім того, було додано багато інших оптимізацій, щоб зробити реалізацію швидкою. В кінці кінців, існує чотири окремі реалізації алгоритму safegcd в libsecp256k1: два алгоритми постійного часу для генерації підписів, один оптимізований для 32-бітних систем та один оптимізований для 64-бітних систем, і два алгоритми змінного часу для перевірки підписів, знову один для 32-бітних систем і один для 64-бітних систем.

Verifiable C

Для того, щоб перевірити, що код C правильно реалізує алгоритм safegcd, всі деталі реалізації повинні бути перевірені. Ми використовуємо Verifiable C, частину Verified Software Toolchain для міркувань про код C, використовуючи теорему провідника Coq.

Перевірка відбувається шляхом визначення преумов і постумов, використовуючи логіку відокремлення для кожної функції, що підлягає перевірці. Логіка відокремлення є логікою, спеціалізованою для міркувань про підпрограми, виділення пам’яті, одночасність та інше.

Коли кожній функції надається специфікація, перевірка відбувається з початку з преумови функції, і встановлюється новий інваріант після кожної інструкції в тілі функції, поки нарешті не буде встановлено постумову в кінці тіла функції або в кінці кожної інструкції повернення. Більшість зусиль з формалізації витрачається «між» рядками коду, використовуючи інваріанти для перекладу сирих операцій кожного виразу C у більш високорівневі твердження про те, що представляють собою оброблювані структури даних математично. Наприклад, те, що мова C вважає масивом 64-бітних цілих чисел, може бути насправді представленням 256-бітного цілого числа.

Кінцевий результат - формальне доведення, перевірене асистентом доведення Coq, що реалізація алгоритму модульного обернення safegcd з використанням змінної часу 64-бітної бібліотеки libsecp256k1 є функціонально правильною.

Обмеження перевірки

Є деякі обмеження на доказ функціональної коректності. Логіка відокремлення, що використовується в Verifiable C, реалізує те, що відоме як часткова коректність. Це означає, що вона лише доводить, що код C повертається з правильним результатом, якщо він повертається, але не доводить саму термінацію. Ми пом'якшуємо це обмеження, використовуючи наше попереднє доведення Coq щодо меж алгоритму safegcd, щоб довести, що значення лічильника циклу основного циклу насправді ніколи не перевищує 11 ітерацій.

Ще одне питання полягає в тому, що сама мова C не має формальної специфікації. Натомість проект Verifiable C використовує проект компілятора CompCert для надання формальної специфікації мови C. Це гарантує, що коли перевірена програма на C компілюється за допомогою компілятора CompCert, отриманий асемблерний код відповідатиме своїй специфікації (за умови вищезгаданої обмеженості). Однак це не гарантує, що код, згенерований GCC, clang або будь-яким іншим компілятором, обов'язково працюватиме. Наприклад, компілятори C можуть мати різні порядки оцінювання аргументів у виклику функції. І навіть якщо мова C мала б формальну специфікацію, будь-який компілятор, який не є формально перевіреним, може все ще неправильно компілювати програми. Це дійсно відбувається на практиці.

Останнє, Verifiable C не підтримує передачу структур, повернення структур або присвоєння структур. Хоча в libsecp256k1 структури завжди передаються за посиланням (що дозволено в Verifiable C), є кілька випадків, коли використовується присвоєння структур. Для доведення коректності модульного оберненого значення було 3 присвоєння, які потрібно було замінити на спеціалізований виклик функції, що виконує присвоєння структур по полях.

Резюме

Blockstream Research формально перевірив коректність функції модульного обернення libsecp256k1. Ця робота надає подальші докази того, що перевірка коду C є можливою на практиці. Використання загального асистента доведення дозволяє нам перевірити програмне забезпечення, побудоване на складних математичних аргументах.

Нічого не заважає іншим функціям, реалізованим у libsecp256k1, також бути перевіреними. Таким чином, можливе для libsecp256k1 отримати найвищі можливі гарантії коректності програмного забезпечення.

Це гостьовий пост Рассела О’Коннора та Ендрю Поелстри. Висловлені думки є цілком їхніми власними і не обов'язково відображають думки BTC Inc або Bitcoin Magazine.

Джерело: Bitcoin Magazine

Пост 'Формально перевірена реалізація Safegcd' вперше з'явився на Crypto Breaking News.