Неподдельное происхождение кода: гарантии компиляции с нулевым разглашением

Автор: Денис Аветисян


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

🚀 Квантовые новости

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

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

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

Обеспечение подлинности программного обеспечения и подтверждение его происхождения из исходного кода является критически важной, но сложной задачей. В работе под названием ‘Verifiable Provenance of Software Artifacts with Zero-Knowledge Compilation’ предложен новый подход к установлению происхождения программного обеспечения, основанный на использовании виртуальных машин с доказательством с нулевым разглашением (zkVM). Авторы демонстрируют, что компиляция программного обеспечения внутри zkVM позволяет генерировать криптографические доказательства, подтверждающие соответствие между исходным кодом, компилятором и полученным исполняемым файлом. Возможно ли создание надежной цепочки поставок программного обеспечения, основанной на zk-компиляции, и какие дополнительные меры безопасности потребуются для ее реализации?


Растущая Угроза Целостности Программного Обеспечения

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

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

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

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

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

Верифицируемая Компиляция: Криптографическое Подтверждение Целостности

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

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

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

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

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

Практическая Реализация и Тестирование Прототипа

Прототип системы использует компилятор ChibiCC и виртуальную машину с доказательствами с нулевым разглашением RISC Zero zkVM для генерации верифицируемых доказательств компиляции кода на языке C. ChibiCC преобразует исходный код C в промежуточное представление, которое затем обрабатывается zkVM. zkVM генерирует доказательство того, что компиляция была выполнена корректно, а также данные, необходимые для верификации этого доказательства. Данный подход позволяет убедиться в целостности процесса компиляции и в том, что исполняемый код соответствует исходному коду, что критически важно для приложений, требующих высокой степени доверия и безопасности.

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

Идентификатор образа (ImageID), генерируемый RISC Zero, представляет собой криптографический отпечаток компилятора, используемого для создания доказательств. Этот идентификатор является неотъемлемой частью процесса установления доверия, поскольку позволяет криптографически подтвердить целостность и подлинность компилятора. ImageID служит доказательством того, что именно определенная, проверенная версия компилятора была использована для генерации доказательств, что исключает возможность манипулирования кодом компилятора для обхода проверок или внедрения вредоносного кода. Данный механизм позволяет убедиться в том, что каждое доказательство сгенерировано надежным и известным компилятором.

Успешная генерация и верификация доказательств демонстрирует практическую реализуемость и эффективность предложенного подхода. Экспериментальные данные, полученные на 200 случайно сгенерированных программах с использованием Csmith, показывают, что медианное время компиляции составляет от 57.01 до 979.12 секунд. При этом медианное время верификации значительно ниже и находится в диапазоне от 47.93 до 68.75 секунд. Данные результаты подтверждают возможность создания верифицируемых доказательств компиляции для C-кода в приемлемые временные рамки.

Размер генерируемых квитанций (receipts) варьируется в зависимости от размера компилируемой C-программы. В ходе тестирования наблюдался диапазон размеров от 0.27 МБ для небольших программ до 120 МБ для более сложных. Этот разброс обусловлен тем, что квитанция содержит данные, необходимые для верификации вычислений, включая код программы, входные данные и результаты, а также доказательства, сгенерированные RISC Zero zkVM. Таким образом, увеличение размера исходного кода приводит к пропорциональному увеличению размера квитанции, необходимой для подтверждения корректности компиляции и выполнения.

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

Усиление Гарантий Происхождения Программного Обеспечения: Комплексный Подход

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

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

Методы, такие как код с доказательством (Proof-Carrying Code, PCC) и формальная верификация, представляют собой дополнительные уровни гарантии и доверия в обеспечении целостности программного обеспечения. PCC предполагает, что вместе с исполняемым кодом предоставляется формальное доказательство его соответствия определенным свойствам безопасности, которое может быть проверено получателем без доступа к исходному коду. Формальная верификация, в свою очередь, использует математические методы для доказательства корректности программного обеспечения, гарантируя, что оно ведет себя именно так, как предполагается, и не содержит уязвимостей. Эти подходы, хотя и требуют значительных вычислительных ресурсов и экспертизы, позволяют значительно повысить уверенность в надежности и безопасности программного обеспечения, особенно в критически важных системах, где ошибки недопустимы.

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

Представленное исследование демонстрирует стремление к созданию надежных и прозрачных систем, что находит отклик в философии элегантного дизайна. Авторы предлагают подход к установлению происхождения программного обеспечения посредством использования машин виртуальных доказательств с нулевым разглашением. Этот метод позволяет генерировать криптографические доказательства, подтверждающие компиляцию бинарного кода из конкретного исходного кода с использованием определенного компилятора. Как заметил Давид Гильберт: «Мы должны знать. Мы должны знать, что мы знаем, и мы должны знать, что мы не знаем». Эта фраза отражает суть стремления к верификации и установлению достоверности, что является ключевым аспектом предложенного решения для обеспечения безопасности цепочки поставок программного обеспечения и подтверждения целостности программных артефактов.

Что дальше?

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

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

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


Оригинал статьи: https://arxiv.org/pdf/2602.11887.pdf

Связаться с автором: https://www.linkedin.com/in/avetisyan/

Смотрите также:

2026-02-14 08:03