Fiat Crypto

Что такое Fiat Crypto?

Fiat Crypto, также называемый Fiat-Crypto или Fiat Cryptography, — это система с открытым исходным кодом для создания эффективного и формально верифицированного кода криптографических арифметических операций.

Она предназначена для преобразования математических описаний высокого уровня в низкоуровневые реализации, сопровождаемые машинно проверяемыми доказательствами корректности.

Проект сосредоточен главным образом на арифметических операциях, применяемых в криптографии на эллиптических кривых, цифровых подписях, обмене ключами, аутентификации и других криптографических системах.

Программное обеспечение для криптовалют в значительной степени зависит от таких операций: транзакции в блокчейне авторизуются цифровыми подписями и проверяются с помощью математических операций над конечными полями.

Fiat Crypto — это не криптовалюта, токен, блокчейн, стейблкоин, кошелек, торговая платформа или цифровой актив, обеспеченный фиатной валютой.

В названии слово «fiat» используется в смысле, связанном с языками программирования: речь идет о создании программного обеспечения на основе спецификаций, а не о деньгах, выпускаемых государством.

В официальном репозитории Fiat-Crypto проект описывается как система для синтеза кода криптографических примитивов, корректность которого обеспечивается самой конструкцией.

Проект разработан в рамках исследований группы по языкам программирования и верификации Массачусетского технологического института.

Его главная цель — снизить риск малозаметных арифметических ошибок в криптографическом программном обеспечении, критически важном для безопасности.

Почему криптографические арифметические операции сложны?

Многие криптографические алгоритмы легко записать в виде математических уравнений, но сложно эффективно реализовать на реальных процессорах.

Математическая спецификация может оперировать целыми числами размером в сотни бит.

Обычные процессоры работают с гораздо меньшими значениями фиксированного размера, например 32- или 64-битными машинными словами.

Разработчикам приходится разбивать большие числа на несколько частей меньшего размера и тщательно учитывать переносы, займы, результаты умножения и приведение по модулю.

Одна ошибка при переносе или пропущенное приведение могут привести к некорректной подписи, отклонению действительной транзакции, принятию недопустимого значения или раскрытию секретной информации.

Самые быстрые реализации часто записывают в виде длинных последовательностей низкоуровневых арифметических операций.

Человеку бывает сложно понять и полностью протестировать такие процедуры.

Традиционное тестирование может показать, что код работает для выбранных входных данных.

Но оно не доказывает, что реализация работает для всех возможных допустимых входных данных.

Fiat Crypto решает эту проблему: система создает код на основе математических спецификаций и одновременно формирует машинно проверяемые доказательства того, что сгенерированные арифметические операции соответствуют этим спецификациям.

Что означает «корректность обеспечивается конструкцией»?

Это означает, что корректность заложена в процесс создания программного обеспечения.

Разработчик начинает с математического описания требуемой операции.

Система преобразует это описание с помощью последовательности доказанных этапов компиляции и оптимизации.

Каждый верифицированный этап сохраняет смысл исходной операции.

Таким образом, итоговая арифметическая процедура связана с высокоуровневой спецификацией формальными доказательствами.

Этот подход отличается от ручного написания оптимизированного кода с последующей попыткой доказать его корректность.

Он также позволяет сократить объем повторяющейся работы по доказательству при добавлении поддержки нового простого модуля или разрядности машинного слова.

В исследовательской статье Simple High-Level Code for Cryptographic Arithmetic описано, как проект использует короткие программы высокого уровня и машинно проверяемые доказательства функциональной корректности.

Что такое формальная верификация?

Формальная верификация использует математическую логику, чтобы доказать соответствие программного обеспечения точно сформулированным свойствам.

Система проверки доказательств проверяет каждое доказательство по небольшому набору доверенных логических правил.

Fiat Crypto использует Coq для создания спецификаций, доказательств, компонентов компилятора и процесса генерации кода.

Coq позволяет разработчикам определять математические объекты, писать программы, формулировать теоремы и создавать доказательства, которые система проверяет автоматически.

Успешное доказательство не ограничивается выполнением набора тестовых примеров.

Оно подтверждает доказанное свойство для всех входных данных, охватываемых формальной спецификацией и ее допущениями.

Формальная верификация не доказывает все мыслимые свойства полноценного приложения для криптовалют.

Она доказывает конкретные утверждения, которые разработчики определили в рамках верифицированной модели.

Как работает Fiat Crypto?

Fiat Crypto начинает работу с высокоуровневого описания модульной арифметики.

Разработчик задает такие параметры, как простой модуль, разрядность машинного слова, структура limbs, стратегия реализации и требуемые для генерации операции.

Система представляет арифметику в Coq.

Затем она применяет верифицированные преобразования, которые упрощают выражения, вычисляют безопасные числовые границы, удаляют ненужные операции и постепенно переводят программу к арифметике над машинными словами.

Преобразованная программа становится линейным внутренним представлением, похожим на C.

Затем бэкенд преобразует это представление в целевой язык программирования или другой верифицированный промежуточный язык.

Сгенерированные функции могут выполнять сложение, вычитание, умножение, возведение в квадрат, перенос, условный выбор и преобразование байтов.

После необходимой проверки, интеграции, компиляции и тестирования полученный код можно включить в более крупную криптографическую библиотеку.

Что такое модульная арифметика?

При модульной арифметике числа, отличающиеся на кратное модуля, считаются эквивалентными.

Простой пример — часы: 13:00 и 1:00 обозначают одно и то же положение на 12-часовом циферблате.

В криптографии используют модульную арифметику с гораздо большими модулями, часто с большими простыми числами.

Предположим, что вычисления выполняются по модулю 17.

Число 20 эквивалентно 3, поскольку при вычитании 17 остается 3.

Это можно записать так:

.

В системах на эллиптических кривых многократно выполняются сложение, вычитание, умножение, возведение в квадрат и нахождение обратного элемента по модулю большого простого числа.

Fiat Crypto адаптирует эти операции для выбранного модуля.

Что такое конечное поле?

Конечное поле — это конечное множество значений с определенными операциями сложения, вычитания, умножения и деления.

В криптографических системах обычно используются поля, основанные на целых числах по модулю большого простого числа.

Значения находятся в диапазоне от нуля до числа, на единицу меньшего простого модуля.

У каждого ненулевого значения есть мультипликативный обратный элемент в этом поле.

Точки эллиптической кривой задаются координатами, арифметические операции над которыми выполняются в конечном поле.

Поэтому системы цифровых подписей и согласования ключей зависят от корректных операций в конечном поле.

Fiat Crypto помогает прежде всего генерировать низкоуровневые процедуры для выполнения такой арифметики.

Что такое limb?

Limb — это одна часть большого целого числа, размер которой соответствует машинному слову.

Элемент конечного поля размером 256 бит может быть представлен четырьмя 64-битными limbs.

В другой реализации могут использоваться пять limbs примерно по 51 бит каждый.

Если оставить в каждом limb неиспользуемые биты, в них можно разместить переносы и промежуточные результаты.

Оптимальная структура limbs зависит от модуля, процессора, инструкций умножения, способа приведения и требуемой производительности.

Неправильно выбранные границы могут привести к тому, что промежуточный результат выйдет за диапазон машинного типа.

Fiat Crypto вычисляет и доказывает границы арифметических значений по мере их прохождения через сгенерированную процедуру.

Что такое приведение по модулю?

Приведение по модулю преобразует большое промежуточное число в эквивалентное значение, входящее в требуемый модульный диапазон.

При умножении двух 256-битных значений может получиться промежуточное значение размером до 512 бит.

Реализация должна привести его по выбранному простому модулю.

Обычная операция деления может выполняться медленно и не обеспечивать подходящего поведения по времени.

Поэтому в криптографических реализациях используют специальные методы приведения, учитывающие структуру модуля.

Fiat Crypto поддерживает несколько стратегий реализации для создания эффективного кода приведения.

Поддерживаемые стратегии арифметики

Насыщенная арифметика Солинаса

В насыщенном представлении limbs занимают большую часть или весь доступный диапазон машинного слова.

Арифметика Солинаса использует преимущества простых чисел, которые можно представить через степени двойки и небольшое количество дополнительных слагаемых.

Такая структура позволяет выполнять приведение быстрее, чем обычное деление.

Ненасыщенная арифметика Солинаса

В ненасыщенном представлении верхние биты каждого limb остаются свободными.

Дополнительное пространство позволяет выполнять несколько арифметических операций до полного переноса или приведения.

В арифметике поля Curve25519 на 64-битных машинах часто используются пять limbs примерно по 51 бит.

Поразрядная арифметика Монтгомери

Арифметика Монтгомери представляет значения в специальной форме, которая позволяет выполнять модульное умножение без обычного деления на модуль.

При поразрядном приведении Монтгомери результат обрабатывается частями размером с машинное слово.

Этот подход может применяться к произвольным нечетным модулям, для которых не подходит удобная форма Солинаса.

Умножение Деттмана

Умножение в стиле Деттмана — это метод реализации эффективной арифметики для некоторых представлений простых полей.

Он организует умножение и приведение с учетом структуры модуля и limbs.

Приведение Солинаса

При приведении Солинаса используются специальные соотношения между степенями двойки и выбранным простым числом.

С помощью этих соотношений старшие части промежуточного числа можно перенести в младшие разряды.

Преобразование основания

Преобразование основания меняет способ распределения значения поля между limbs.

Оно может потребоваться, если две части криптографической системы используют разные внутренние представления.

В текущем репозитории описание этих стратегий приведено в едином интерфейсе генерации кода

.

Какие операции может генерировать Fiat Crypto?

Fiat Crypto может генерировать процедуры модульного сложения и вычитания.

Система также может генерировать процедуры умножения и возведения в квадрат.

Она может создавать функции переноса и приведения, которые переводят значения в допустимый диапазон.

Также можно сгенерировать функции отрицания и умножения на выбранные константы.

Система может создавать функции условного выбора, предназначенные для обхода обычных ветвлений, зависящих от секретных значений.

Кроме того, она может генерировать функции преобразования между внутренними limbs и стандартизированными последовательностями байтов.

Точный набор доступных функций зависит от выбранной стратегии и параметров командной строки.

Для полноценной реализации подписи или обмена ключами, помимо этих операций над полем, потребуются дополнительные операции над группами, хеширование, генерация nonce, проверка протокола и логика приложения.

Какие простые числа для криптографии поддерживает Fiat Crypto?

Fiat Crypto предназначен для генерации арифметических операций для различных простых модулей, а не только для одной фиксированной кривой.

В официальном репозитории есть примеры генерации для простого числа

, используемого в криптографии семейства Curve25519.

В нем также представлены примеры для простого числа поля NIST P-256.

Кроме того, кодовая база содержит поддержку и доказательства, связанные с полем secp256k1, применяемым в основных блокчейн-системах цифровых подписей.

Примеры генерации Bedrock2 включают простое число

, используемое для аутентификации Poly1305.

Поддержка простого числа поля сама по себе не обеспечивает полноценную реализацию каждого протокола, использующего это поле.

Разработчикам по-прежнему необходимо интегрировать сгенерированную арифметику с корректно реализованными операциями над точками, подписями, хешами, сериализацией, проверкой данных и управлением ключами.

Почему secp256k1 важна для Fiat Crypto?

secp256k1 — это эллиптическая кривая, используемая в нескольких крупных протоколах криптовалют.

Кошельки используют приватные ключи secp256k1 для создания подписей, которыми авторизуются транзакции в блокчейне.

Узлы проверяют эти подписи, прежде чем признать транзакции действительными.

Вычисления координат этой кривой выполняются по конкретному 256-битному простому модулю.

Ошибка в арифметике этого поля может привести к некорректным точкам, подписям или результатам проверки.

Поддержка Fiat Crypto арифметики, связанной с secp256k1, делает проект актуальным для исследований реализации блокчейнов и разработки кошельков с высокими гарантиями безопасности.

Связанный с проектом исследовательский проект CryptOpt также связал верифицированный промежуточный код Fiat Cryptography с генерацией оптимизированного ассемблерного кода, в том числе для арифметики secp256k1.

Fiat Crypto и криптография на эллиптических кривых

В криптографии на эллиптических кривых используются точки, удовлетворяющие алгебраическому уравнению над конечным полем.

Публичные ключи получают умножением точки кривой на секретный скаляр.

При создании и проверке подписей выполняются многочисленные сложения и удвоения точек, умножения на скаляр и операции над полем.

Fiat Crypto предоставляет верифицированную основу для некоторых арифметических операций, лежащих в основе этих алгоритмов более высокого уровня.

В репозитории также содержатся доказательства и определения для представлений кривых Эдвардса, Монтгомери и Вейерштрасса.

Корректность арифметики поля сама по себе не доказывает безопасность всего протокола на эллиптической кривой.

Корректными также должны быть кривая, проверка точек, обработка скаляров, генерация nonce, построение подписи и окружающее программное обеспечение.

Какие языки программирования поддерживает Fiat Crypto?

В текущем репозитории поддерживается основной бэкенд C.

Также поддерживается путь Bedrock2/C с более широким охватом доказательств, связывающих внутреннее синтаксическое дерево с Bedrock2.

К бэкендам, которые поддерживаются сообществом или внешними разработчиками, относятся Go, Rust и Zig.

Бэкенд JSON обозначен как экспериментальный.

В репозитории указано, что бэкенд Java больше не поддерживается и имеет известные проблемы.

Статус бэкендов может меняться, поэтому перед выбором сгенерированного кода разработчикам следует проверить актуальную таблицу статусов бэкендов.

Проект прямо указывает, что не предоставляет одинаковых гарантий качества для всех бэкендов.

Как создается компилятор?

Верифицированные определения и преобразования записаны на Coq.

Fiat Crypto может извлекать исполняемый код компилятора в OCaml или Haskell.

Полученная программа командной строки принимает параметры, описывающие реализацию арифметики.

Сгенерированный исходный код выводится в стандартный поток вывода.

Благодаря такому подходу генерация кода возможна без загрузки полной системы доказательств при каждом запросе.

Разработка доказательств подтверждает свойства преобразований, на основе которых извлекается исполняемый компилятор.

Для сборки полного репозитория по-прежнему нужны описанные зависимости Coq, OCaml, системы сборки и пакетов.

Что доказывает Fiat Crypto?

Fiat Crypto предназначен для доказательства функциональной корректности сгенерированной арифметики относительно ее формальных спецификаций.

Функциональная корректность означает, что сгенерированная операция вычисляет математически ожидаемый результат для входных данных, удовлетворяющих документированным предварительным условиям.

Система также анализирует числовые диапазоны, чтобы промежуточные значения помещались в выбранные машинные целочисленные типы.

Верифицированные этапы переписывания и компиляции должны сохранять смысл выражений.

Точная граница сквозного доказательства зависит от бэкенда и способа интеграции.

В репозитории указано, что бэкенд Bedrock2 включает доказательство, связывающее абстрактное синтаксическое дерево Bedrock2 с внутренним абстрактным синтаксическим деревом.

Для других бэкендов, преобразующих код в текст на языках программирования, такой же охват доказательств пока не обеспечен.

Это различие важно при оценке утверждений о полной верификации сгенерированного исходного кода.

Чего Fiat Crypto не доказывает?

Fiat Crypto не доказывает безопасность каждого связанного кошелька, узла блокчейна, смарт-контракта или приложения.

Система не доказывает автоматически устойчивость криптографического протокола ко всем математическим атакам.

Она не подтверждает, что приватный ключ создан с достаточным уровнем случайности.

Она не мешает разработчику передать недопустимые параметры или неправильно использовать сгенерированные функции.

Она не гарантирует, что каждый компилятор, компоновщик, операционная система, процессор или аппаратное устройство сохранит все предполагаемые свойства.

Для большинства выходных бэкендов нет полностью доказанного преобразования внутреннего представления в окончательный текст исходного кода.

В репозитории также отмечено, что поведение целочисленных выражений обычного компилятора C остается частью доверенной или отдельно проверяемой среды.

Поэтому формальную верификацию следует понимать как весомую гарантию с четко определенными границами, а не как универсальную гарантию.

Гарантирует ли Fiat Crypto выполнение кода за постоянное время?

Криптографическому коду часто необходимо избегать потока управления и шаблонов доступа к памяти, зависящих от секретных значений.

Такой подход к программированию обычно называют написанием кода с постоянным временем выполнения.

Сгенерированная линейная арифметика и примитивы условного выбора могут помочь создавать реализации с постоянным временем выполнения.

Однако фактическое время выполнения зависит от сгенерированного бэкенда, компилятора, целевого процессора, окружающего кода и микроархитектуры.

Доказательство функциональной корректности автоматически не становится полноценным доказательством устойчивости ко всем атакам по времени выполнения, кэшу, энергопотреблению, электромагнитному излучению, спекулятивному выполнению или внедрению ошибок.

Разработчикам необходимо проверить гарантии выбранного конвейера и провести соответствующее тестирование и анализ побочных каналов.

Fiat Crypto и криптографический код, написанный вручную

Криптографический код, написанный вручную опытным специалистом, может быть чрезвычайно быстрым.

Но в нем также могут быть ошибки, которые трудно выявить при обычной проверке.

Для ручной реализации часто требуется отдельная работа для каждого простого числа, разрядности, процессора и представления арифметики.

Fiat Crypto автоматизирует значительную часть такой специализации на основе универсальной математической модели.

Если предположения или целевые платформы меняются, сгенерированный код может быть проще создать заново.

Производительность по-прежнему нужно измерять на целевой платформе.

В некоторых специализированных средах тщательно написанный ассемблерный код может работать быстрее обычного сгенерированного кода C.

Такие проекты, как CryptOpt, исследуют возможности применения верифицированной основы Fiat Crypto для создания высокооптимизированного ассемблерного кода.

Fiat Crypto и традиционное тестирование

При тестировании фактические результаты сравнивают с ожидаемыми для конечного набора примеров.

Формальная верификация доказывает заданное свойство для полного диапазона входных данных, охватываемого теоремой.

Тестирование остается полезным: оно позволяет обнаружить проблемы интеграции, сборки, платформы, сериализации и производительности, которые не охватываются формальным доказательством.

В репозитории Fiat Crypto сгенерированный код C тестируется с помощью проверенного набора криптографических тестов.

Код на Rust проверяется отдельным набором тестов криптографической библиотеки.

Таким образом, формальные доказательства и практическое тестирование дополняют, а не заменяют друг друга.

Fiat Crypto и фиатная валюта

Фиатная валюта — это выпускаемые государством деньги, например доллары, евро или иены.

Fiat Crypto — это проект в области верификации программного обеспечения и генерации кода.

Проект не выпускает деньги и не привязывает токен к национальной валюте.

Он не обеспечивает банковские или карточные платежи, депозиты в фиатной валюте или покупку криптовалют.

По запросу «fiat crypto» можно найти информацию о конвертации государственных валют в криптовалюту.

Этот финансовый смысл не связан с программным проектом Fiat-Crypto.

Fiat Crypto и конвертация фиатной валюты в криптовалюту

Конвертация фиатной валюты в криптовалюту — это обмен выпускаемых государством денег на криптовалюту или цифровой актив.

Сервис для покупки криптовалюты за фиат может обрабатывать банковский перевод, оплату картой, проверку личности, обмен валюты и отправку средств в блокчейне.

Fiat Crypto, напротив, генерирует реализации криптографических арифметических операций.

Проект не предоставляет сервис для ввода или вывода средств между фиатом и криптовалютой.

Это различие важно: названия похожи, но относятся к совершенно разным направлениям криптоиндустрии.

Fiat Crypto и преобразование Fiat–Shamir

Преобразование Fiat–Shamir переводит некоторые интерактивные протоколы доказательств в неинтерактивные доказательства или подписи.

Оно названо в честь криптографов Амоса Фиата и Ади Шамира.

Fiat Crypto — отдельный проект в области формальных методов, предназначенный для синтеза кода криптографических арифметических операций.

Обе темы относятся к криптографии, но решают разные задачи.

Fiat–Shamir касается взаимодействия в рамках протокола и формирования вызова.

Fiat Crypto посвящен верифицированной реализации низкоуровневых математических операций.

Fiat Crypto и криптографическая библиотека

Полноценная криптографическая библиотека предоставляет готовые API для подписей, шифрования, хеширования, обмена ключами, сертификатов и других протоколов.

Fiat Crypto — прежде всего генератор и система доказательств для арифметических компонентов.

Его результаты можно интегрировать в более широкую библиотеку.

Такая библиотека по-прежнему отвечает за логику протокола, публичные интерфейсы, управление памятью, генерацию случайных значений, проверку входных данных, обработку ошибок и безопасное хранение ключей.

Не следует считать одну сгенерированную процедуру умножения полноценной реализацией цифровой подписи.

Fiat Crypto и компилятор общего назначения

Компилятор общего назначения обрабатывает программы, выполняющие широкий спектр вычислений.

Fiat Crypto — специализированная система для криптографической арифметики.

Благодаря узкой специализации система использует математические знания о простых полях, limbs, переносах и приведении по модулю.

Она может специализировать код с учетом деталей, которые универсальный компилятор может не вывести из обычного исходного кода.

После этого сгенерированный код C или на другом языке все еще можно компилировать с помощью компилятора общего назначения.

Таким образом, полный доверенный процесс включает как конвейер генерации Fiat Crypto, так и последующую цепочку сборки.

Почему Fiat Crypto важен для безопасности блокчейна

Блокчейн-протоколы передают контроль над ценными активами криптографическим ключам.

Ошибка в арифметике поля может подорвать безопасность цифровых подписей, даже если экономические правила блокчейна заданы корректно.

Узлы могут получать из сети недоверенные публичные ключи, подписи, доказательства и данные транзакций.

Поэтому криптографические реализации должны корректно обрабатывать все допустимые крайние случаи.

Для арифметических процедур с огромным пространством входных данных формальные методы позволяют получить более весомые доказательства, чем обычное тестирование.

Fiat Crypto также упрощает создание согласованных реализаций для процессоров разной разрядности и простых полей.

Это помогает снизить зависимость от небольшого числа экспертов, которым приходится вручную переписывать сложный арифметический код.

Чем Fiat Crypto может быть полезен криптокошелькам

Кошельки используют криптографические арифметические операции для создания публичных ключей и подписей.

Мобильному кошельку может потребоваться безопасный и эффективный код для 32- или 64-битных процессоров.

Аппаратный кошелек может иметь строгие ограничения по памяти, времени выполнения и возможностям процессора.

Сгенерированные процедуры для конечных полей могут стать верифицированной основой для операций с ключами и подписями.

Разработчику кошелька все равно необходимо проверять публичные ключи, защищать секретные ключи, безопасно генерировать nonce и предотвращать утечки по побочным каналам.

Ошибки пользовательского интерфейса и разбора транзакций также остаются за пределами доказательств арифметической корректности.

Чем Fiat Crypto может быть полезен узлам блокчейна

Узлы блокчейна могут проверять тысячи подписей или криптографических доказательств.

Производительность важна: неэффективная проверка может снизить пропускную способность транзакций и повысить требования к оборудованию.

Корректность не менее важна, поскольку все узлы должны приходить к одинаковому результату проверки.

Редкое расхождение в арифметических вычислениях может привести к сбою консенсуса, если одни реализации принимают транзакцию, а другие ее отклоняют.

Верифицированная арифметика позволяет уменьшить вероятность одного из источников расхождений между реализациями.

Узлам по-прежнему необходимы тесты консенсуса, спецификации протокола, защита сети, безопасность баз данных и полная проверка реализации.

Чем Fiat Crypto может быть полезен системам с доказательствами с нулевым разглашением

Системы доказательств с нулевым разглашением выполняют большое количество арифметических операций над конечными полями.

Для создания и проверки доказательств могут использоваться разные простые поля.

Некорректные операции над полем могут привести к недействительным доказательствам, ошибочному отклонению или серьезным проблемам безопасности.

Генератор кода, который адаптирует арифметику к модулю системы доказательств, может повысить переносимость и уровень гарантий.

Fiat Crypto не генерирует автоматически полноценную систему создания доказательств с нулевым разглашением.

Полиномиальные коммитменты, построение транскрипта, уравнения доказательства, логика схемы и криптографические допущения требуют отдельных реализаций и доказательств.

Как безопасно использовать Fiat Crypto

Разработчикам следует начать с официального репозитория и изучить актуальную документацию по сборке и бэкендам.

Необходимо выбрать подходящую для модуля и целевой архитектуры поддерживаемую стратегию арифметики.

Сгенерированный код следует проверить, скомпилировать с поддерживаемыми настройками и протестировать на независимых контрольных примерах.

Границы доказательств проекта и ограничения бэкенда следует задокументировать в рамках проверки безопасности использующего их приложения.

Разработчикам следует тестировать некорректные входные данные, граничные значения, максимальные переносы, нулевые значения и неканонические кодировки.

Побочные каналы следует оценивать на фактическом сочетании компилятора и оборудования.

Обновления генератора, системы доказательств, компилятора или бэкенда должны запускать новый цикл тестирования и проверки.

При подготовке продукта к эксплуатации нельзя считать слова «формально верифицирован» основанием для отказа от аудита интеграции.

Преимущества Fiat Crypto

Fiat Crypto предоставляет машинно проверяемые доказательства функциональной корректности важных арифметических преобразований.

Система может генерировать реализации для разных простых модулей и разрядностей машинного слова.

Она сокращает объем повторяющейся ручной работы при создании оптимизированной арифметики конечных полей.

В высокоуровневых спецификациях проще разобраться, чем в тысячах написанных вручную низкоуровневых операций.

Проект имеет открытый исходный код и доступен для независимого анализа.

Он обеспечивает воспроизводимую генерацию кода вместо зависимости от копируемых файлов арифметических процедур с неясным происхождением.

Сгенерированные процедуры используются в широко распространенном криптографическом программном обеспечении и обширных наборах тестов.

Ограничения Fiat Crypto

Fiat Crypto охватывает только часть полноценного стека криптографического программного обеспечения.

Гарантии доказательств различаются в зависимости от бэкенда.

Для сборки и изменения разработки доказательств нужны специальные знания Coq, формальных методов, компиляторов и криптографической арифметики.

Сгенерированный исходный код все равно проходит через обычные компиляторы и инструменты платформы.

Функциональная корректность автоматически не доказывает устойчивость ко всем побочным каналам.

Производительность может различаться в зависимости от процессора и компилятора.

Неподдерживаемые параметры или неактуальные бэкенды могут создавать дополнительные риски.

Формально корректная реализация небезопасного криптографического решения все равно остается небезопасной.

Распространенные заблуждения о Fiat Crypto

Fiat Crypto — это не криптовалюта.

Проект не связан с выпускаемыми государством фиатными деньгами.

Он не конвертирует наличные деньги в цифровые активы.

Он не является преобразованием Fiat–Shamir.

Он не создает автоматически полноценные приложения для блокчейна.

Он не доказывает безопасность каждой программы, использующей его результаты.

Он не отменяет необходимости в тестировании и проверке кода.

Он не обеспечивает одинаковые гарантии доказательств для всех поддерживаемых языковых бэкендов.

Он не делает безопасными слабые ключи, небезопасные протоколы или уязвимые интерфейсы кошельков.

Часто задаваемые вопросы

Что такое Fiat Crypto?

Fiat Crypto — это проект с открытым исходным кодом, который создает эффективный код криптографических арифметических операций на основе высокоуровневых спецификаций и машинно проверяемых доказательств корректности.

Является ли Fiat Crypto криптовалютой?

Нет. Это проект по верификации программного обеспечения и генерации кода, а не цифровой актив.

Связан ли Fiat Crypto с фиатными деньгами?

Нет, проект не выпускает, не обрабатывает и не конвертирует государственные валюты.

Fiat Crypto и Fiat Cryptography — это одно и то же?

Да, Fiat-Crypto и Fiat Cryptography — распространенные названия одного проекта и исследовательской работы.

Кто разработал Fiat Crypto?

Проект возник на основе исследований в области формальной верификации и криптографических реализаций, связанных с группой MIT по языкам программирования и верификации, а также внешними участниками.

Какую систему доказательств использует Fiat Crypto?

Coq используется для определения спецификаций, реализации преобразований и проверки доказательств корректности.

Какой код генерирует Fiat Crypto?

В основном он генерирует низкоуровневые процедуры модульной арифметики для криптографических конечных полей.

Генерирует ли Fiat Crypto код C?

Да, C — одна из основных поддерживаемых целевых платформ проекта.

Поддерживает ли Fiat Crypto Rust?

В репозитории есть внешне поддерживаемый бэкенд Rust с тестированием сгенерированного кода.

Поддерживает ли Fiat Crypto Go?

Да, в репозитории указан внешне поддерживаемый бэкенд Go.

Поддерживает ли Fiat Crypto Zig?

Да, Zig указан как внешне поддерживаемый бэкенд, сгенерированный код которого используется в тестировании.

Рекомендуется ли бэкенд Java?

В текущем репозитории указано, что бэкенд Java больше не поддерживается и имеет известные проблемы.

Что такое конечное поле?

Конечное поле — это конечное множество значений с арифметическими операциями, используемыми во многих криптографических алгоритмах.

Что такое limb?

Limb — это одна часть большого криптографического целого числа размером с машинное слово.

Что такое приведение по модулю?

Приведение по модулю преобразует результат арифметической операции в эквивалентное значение относительно выбранного модуля.

Что такое арифметика Монтгомери?

Арифметика Монтгомери использует специальное представление чисел для эффективного модульного умножения без обычного деления на модуль.

Что такое арифметика Солинаса?

Арифметика Солинаса использует простые модули, структура которых позволяет эффективно выполнять приведение с помощью степеней двойки и небольших констант.

Поддерживает ли Fiat Crypto арифметику Curve25519?

Да, в официальном репозитории есть примеры генерации для простого числа, используемого в криптографии семейства Curve25519.

Поддерживает ли Fiat Crypto secp256k1?

В проекте есть работа над полем и эллиптической кривой secp256k1, актуальная для блокчейн-реализаций цифровых подписей.

Создает ли Fiat Crypto цифровые подписи?

Система генерирует арифметические компоненты, которые можно использовать в реализациях подписей, но сама по себе не является полноценным приложением для создания подписей.

Доказывает ли Fiat Crypto безопасность схемы подписи?

Нет. Функциональная корректность арифметики — не то же самое, что доказательство полной математической безопасности схемы подписи.

Предотвращает ли Fiat Crypto арифметическое переполнение?

Верифицированный конвейер анализирует границы значений и выбирает целочисленные типы, которые должны вмещать охватываемые спецификациями промежуточные значения.

Гарантирует ли Fiat Crypto постоянное время выполнения кода?

Архитектура системы поддерживает криптографическую арифметику с фиксированным потоком управления, но общая защита от атак по побочным каналам зависит от бэкенда, компилятора, процессора и окружающего приложения.

Может ли тестирование заменить доказательства Fiat Crypto?

Нет. Тестирование и формальные доказательства обеспечивают разные виды гарантий; наибольшую пользу они приносят вместе.

Может ли формальная верификация заменить аудит безопасности?

Нет. В рамках аудита также необходимо проверять логику протокола, интеграцию, случайность, безопасность памяти, обработку ключей, побочные каналы и поведение приложения.

Формально ли верифицирован каждый бэкенд Fiat Crypto?

Нет. В репозитории для выходных бэкендов указаны разные уровни доказательств, поддержки и тестирования.

Какой путь через бэкенд имеет наиболее сильную документированную проверку?

Для бэкенда Bedrock2 есть дополнительное доказательство, связывающее его абстрактное синтаксическое дерево с внутренним представлением Fiat Crypto.

Чем Fiat Crypto полезен для блокчейнов?

Он может снизить количество ошибок реализации арифметики в подписях, ключах, доказательствах и других криптографических операциях, используемых блокчейн-программами.

Можно ли использовать Fiat Crypto в кошельках?

Сгенерированную арифметику можно интегрировать в криптографическую часть кошелька, однако полноценный кошелек по-прежнему требует отдельной разработки с учетом безопасности.

Fiat Crypto — это то же самое, что конвертация фиатной валюты в криптовалюту?

Нет, конвертация фиатной валюты в криптовалюту — это финансовый сервис для покупки цифровых активов за государственную валюту.

Fiat Crypto — это то же самое, что Fiat–Shamir?

Нет. Fiat–Shamir преобразует интерактивные доказательства, а Fiat Crypto синтезирует верифицированные реализации арифметических операций.

Имеет ли Fiat Crypto открытый исходный код?

Да, проект общедоступен и распространяется на условиях нескольких разрешительных лицензий с открытым исходным кодом, перечисленных в репозитории.

Заключение

Fiat Crypto — это система формальной верификации и генерации кода для создания эффективной криптографической арифметики.

Она позволяет разработчикам описывать модульные операции на высоком уровне и получать низкоуровневые реализации с помощью машинно проверяемых преобразований.

Проект особенно актуален для криптовалют: цифровые подписи, публичные ключи, кошельки, узлы и системы доказательств с нулевым разглашением в блокчейне зависят от корректной арифметики конечных полей.

Fiat Crypto может генерировать операции для важных простых полей и таких стратегий реализации, как арифметика Солинаса и Монтгомери.

К поддерживаемым направлениям относятся бэкенды C и Bedrock2/C, а также внешне поддерживаемые бэкенды для других языков.

Точный уровень гарантий зависит от выбранного бэкенда и границ формального доказательства.

Формальная верификация снижает риск арифметических ошибок, но не доказывает все свойства полноценного криптографического приложения.

Разработчикам по-прежнему необходимо проверять безопасность протокола, обработку приватных ключей, случайность, сериализацию, поведение компилятора и оборудования, а также устойчивость к атакам по побочным каналам.

Поэтому Fiat Crypto следует рассматривать как мощную основу для криптографического программного обеспечения с высокими гарантиями, а не как полноценную замену тестированию, аудиту и безопасному проектированию систем.