Безпека Bitcoin та інших блокчейнів, таких як Liquid, залежить від алгоритмів цифрових підписів, таких як ECDSA та підписи Шнорра. Бібліотека C під назвою libsecp256k1 надає ці алгоритми і використовується як Bitcoin Core, так і Liquid. Ці алгоритми використовують обчислення, яке називається модульним оберненням, що є витратною частиною процесу.
У статті "Швидкий обчислення gcd з постійним часом та модульне обернення" Даніель Дж. Бернштейн та Бо-Ін Ян створили новий алгоритм модульного обернення, званий "safegcd". Цей алгоритм був реалізований для libsecp256k1 Петером Деттманом у 2021 році. Blockstream Research формально підтвердив дизайн алгоритму за допомогою асистента доказів Coq, показавши, що він правильно обчислює модульне обернене значення для 256-бітних вхідних даних.
Однак реалізація алгоритму safegcd вимагала адаптації математичного опису для того, щоб вписатися в мову програмування C, яка нативно підтримує лише цілі числа до 64 біт. Було додано кілька оптимізацій, щоб зробити реалізацію швидкою, в результаті чого було створено чотири окремі реалізації алгоритму safegcd в libsecp256k1.
Щоб забезпечити правильну реалізацію алгоритму safegcd в коді C, було використано Verifiable C, частину Verified Software Toolchain, разом з теоремним доводчиком Coq. Це передбачало специфікацію попередніх і постійних умов для кожної функції, що підлягає перевірці, за допомогою логіки розділення. Процес перевірки почався з попередньої умови функції та встановлював новий інваріант після кожного виразу в тілі функції, поки не була досягнута постійна умова в кінці тіла функції або у виразах повернення.
Більшість зусиль щодо формалізації було витрачено на переклад сирих операцій кожного виразу C на вищі рівні тверджень про те, що представляють собою маніпульовані структури даних з математичної точки зору. Перевірка призвела до формального доказу, перевіреного асистентом доказів Coq, що 64-бітна реалізація алгоритму модульного оберненого значення safegcd в libsecp256k1 є функціонально правильною.
Однак існують певні обмеження на доказ функціональної правильності. Логіка розділення, яка використовується в Verifiable C, лише доводить часткову правильність, що означає, що вона лише показує, що код C повертає правильний результат, якщо він повертається, але не доводить саму термінацію. Для вирішення цього було використано попереднє доказ Coq меж алгоритму safegcd, щоб довести, що значення лічильника циклу основного циклу ніколи не перевищує 11 ітерацій.
Ще одним обмеженням є те, що сама мова C не має формальної специфікації. Замість цього проект Verifiable C використовує проект компілятора CompCert для надання формальної специфікації мови C. Це гарантує, що коли перевірена програма C компілюється за допомогою компілятора CompCert, отриманий асемблерний код відповідатиме своїй специфікації, але це не гарантує, що код, згенерований іншими компіляторами, обов'язково працюватиме.
Крім того, Verifiable C не підтримує передачу, повернення або присвоєння структур. У libsecp256k1 структури завжди передаються за допомогою вказівника, що дозволено в Verifiable C, але є кілька випадків, коли використовується присвоєння структур. Підсумовуючи, Blockstream Research формально підтвердив правильність функції модульного оберненого значення libsecp256k1, надаючи додаткові докази того, що перевірка коду C можлива на практиці.
Ця робота також підкреслює, що решту функцій, реалізованих у libsecp256k1, також можна перевірити, що дозволяє бібліотеці досягти найвищих можливих гарантій правильності програмного забезпечення.
Джерело
<p>Пост Як цифрові підписи роблять Bitcoin безпечним! вперше з'явився на CoinBuzzFeed.</p>
