Безопасность Bitcoin и других блокчейнов, таких как Liquid, зависит от алгоритмов цифровых подписей, таких как ECDSA и подписи Шнора. C-библиотека под названием libsecp256k1 предоставляет эти алгоритмы и используется как Bitcoin Core, так и Liquid. Эти алгоритмы используют вычисление, называемое модульным обратным значением, которое является затратной частью процесса.
В статье «Быстрое вычисление gcd с постоянным временем и модульное обращение» Даниэль Дж. Бернштейн и Бо-Йин Ян создали новый алгоритм модульного обращения под названием «safegcd». Этот алгоритм был реализован для libsecp256k1 Петером Деттманом в 2021 году. Blockstream Research формально верифицировала дизайн алгоритма с использованием асистента доказательств Coq, показав, что он правильно вычисляет модульное обратное значение для 256-битных входных данных.
Однако реализация алгоритма safegcd потребовала адаптации математического описания для соответствия языку программирования C, который нативно поддерживает только целые числа до 64 бит. Были добавлены несколько оптимизаций, чтобы сделать реализацию быстрой, в результате чего в libsecp256k1 было создано четыре отдельные реализации алгоритма safegcd.
Чтобы убедиться, что C-код правильно реализует алгоритм safegcd, был использован 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>
