Криптографические хеш-функции используются во многих приложениях, которые критически полагаются на свою устойчивость к атакам криптоанализа и правильность их реализации. Тем не менее, уязвимости в реализациях криптографических хеш-функций могут оставаться незамеченными более десяти лет, как показало недавнее обнаружение переполнения буфера в реализации SHA-3 в расширенном пакете кода Kec-cak (XKCP) влияя на Python, PHP и несколько других программных проектов. В этом документе объясняется, как была обнаружена уязвимость к переполнению буфера в XKCP. В более общем плане мы изучаем применение формальных методов к пяти финалистам пакетов, представленных на конкурс NIST SHA-3, что позволяет нам (повторно) обнаруживать уязвимости в реализациях Keccak и BLAKE, а также обнаруживать ранее нераскрытую уязвимость в реализация Гростля. Мы также показываем, как тот же подход повторно обнаруживает уязвимость, затрагивающую 11 из 12 реализованных криптографических хэш-функций в библиотеке Apple CoreCrypto. Наш подход состоит в удалении определенных строк кода и последующем использовании KLEE в качестве инструмента для доказательства функциональной эквивалентности. Мы обсуждаем преимущества и ограничения нашего подхода и надеемся, что наша попытка объединить некоторые более ранние подходы может привести к новым открытиям.
Введение
(Криптографическая) хэш-функция принимает сообщение переменной длины и превращает его в вывод фиксированной длины, известный как «хеш-значение» или «хэш». Чтобы хеш-функция была безопасной, должно быть невозможно с вычислительной точки зрения инвертировать функцию для данного хэша (устойчивость к прообразу) или найти два разных сообщения, которые приводят к одному и тому же хешу (устойчивость к коллизиям). Эти свойства позволяют использовать хеш-значение вместо самого сообщения в схеме цифровой подписи, так что успешная проверка подписи подтверждает, что сообщение не было изменено.
В ответ на атаку криптоанализа на хэш-функцию SHA-1, представленную на CRYPTO 2005 Ваном и др. [36], NIST решил запустить конкурс SHA-3 на новый стандарт хэш-функции [29]. Конкурс был объявлен в ноябре 2007 г. К октябрю 2008 г. было получено 64 заявки, а 51 была выбрана в качестве кандидатов в первом туре в декабре 2008 г. Четырнадцать из них прошли в качестве кандидатов во второй тур в июле 2009 г., а пять финалистов ( BLAKE, Grøstl, JH, Keccak и Skein) были объявлены в декабре 2010 года. Конкурс SHA-3 завершился в октябре 2012 года, когда Кекчак был объявлен победителем.
Пакеты, подаваемые на конкурс SHA-3, должны были включать эталонные и оптимизированные реализации на языке программирования C [27]. NIST определил используемый интерфейс прикладного программирования (API) (см. Раздел 3), а также тестовые векторы, которые требовались в каждом пакете отправки.
Поскольку пакеты, представленные на конкурс SHA-3, подвергались публичному рассмотрению, в нескольких заявках в 2008 и 2009 годах сообщалось об ошибках. Систематический анализ, проведенный Forsythe и Held из Fortify Software [18], обнаружил множество ошибок, которые обычно появляются в коде C такие как чтение за пределами границ, утечки памяти и разыменование нулевого указателя. В течение оставшейся части конкурса об ошибках не сообщалось, и в конечном итоге получившийся стандарт SHA-3 стал широко применяться во многих криптографических библиотеках.
Однако в сентябре 2015 года реализация на сайте BLAKE была обновлена с комментарием: «исправлена ошибка, которая давала неверные хэши в конкретных случаях использования» [4]. В 2018 году Муха и соавт. [24] повторно обнаружили ошибку, используя новую методологию тестирования, которая в конечном итоге была интегрирована в проект Google Wycheproof [10], и показали, что ошибка позволяет нарушить устойчивость хеш-функции к коллизиям.
На CT-RSA 2020 Муха и Celi [22] показали уязвимость, затрагивающую 11 из 12 реализованных хеш-функций в библиотеке Apple CoreCrypto. Уязвимость требовала вызова реализации на входах размером не менее 4 ГиБ, что приводило к бесконечному циклу. Эта уязвимость показала ограничение в программе проверки криптографических алгоритмов NIST (CAVP), которая не выполняла тесты хеш-функций для входных данных размером более 65 535 бит. Чтобы обойти это ограничение, NIST ввел тест больших данных (LDT).
В октябре 2022 года Муха [31] обнаружил уязвимость, которая повлияла как на пакет представления Keccak для финального раунда, так и на итоговую реализацию SHA-3 его разработчиками. В зависимости от конкретных введенных данных уязвимость приводила либо к бесконечному циклу, либо к переполнению буфера, когда предоставленные злоумышленником значения подвергались операции XOR в памяти [23].
Наши вклады.
Недостаток предыдущей работы по поиску уязвимостей в реализациях хеш-функций заключается в том, что им не хватает общности и они явно не соответствуют требованиям, поскольку продолжают обнаруживаться новые уязвимости, которые оставались незамеченными более десяти лет (несмотря на широкое общественное внимание). Новый вклад этой статьи состоит в том, чтобы попытаться преодолеть эту проблему, представив новый подход, который можно использовать для поиска уязвимостей в реализациях хеш-функций библиотеки Apple CoreCrypto, а также в трех из пяти представленных финалистов SHA-3: БЛЕЙК, Кекчак и Грёстль. В этой статье объясняется, как была обнаружена уязвимость в Keccak. Уязвимость в Grøstl — это новый вклад в эту статью, о котором ранее не сообщалось. Наш подход включает символическое выполнение для поиска ошибок в течение нескольких секунд, в то время как выполнение тестовых векторов может занять гораздо больше времени.
Связанные работы
Подход NIST к тестированию криптографических реализаций восходит к 1977 году, когда в SP 500-20 были введены два набора тестовых векторов для стандарта шифрования данных (DES) [25]. Теперь известный как тесты известных ответов (KAT) или статические алгоритмические функциональные тесты (AFT), первый набор тестовых векторов был предназначен для «полного применения таблиц нелинейных замен» (S-блоков) DES. Второй набор тестовых векторов, называемый тестами Монте-Карло (MCT), содержал «псевдослучайные данные для проверки того, что устройство не было разработано только для того, чтобы пройти набор тестов». Первоначально предназначенный для тестирования аппаратных реализаций, этот подход может применяться как к аппаратному, так и к программному обеспечению и лежит в основе Программы проверки криптографических алгоритмов NIST (CAVP).
Заявки на конкурс NIST SHA-3 должны были включать реализации на языке программирования C. NIST определил API [27] и предоставил исходный код для создания KAT и MCT [28]. Эти KAT и MCT помогли обеспечить согласованность различных реализаций одного и того же алгоритма. Кроме того, интересным нововведением стало включение чрезвычайно длинного сообщения KAT, которое предоставляло сообщение размером 1 ГиБ с целью обеспечения правильной обработки больших входных данных.
Для (аутентифицированных) алгоритмов шифрования платформы SUPERCOP [7] и BRU-TUS [34] выполняют некоторые дополнительные тесты, такие как проверка правильности обработки перекрывающихся входных данных или того, возвращает ли шифрование с последующим дешифрованием исходный открытый текст.
Аумассон и Ромайлер представили криптодифференциальный фаззинг [3], который использует фаззер для сравнения выходных данных различных криптографических библиотек и поиска расхождений. Такой подход оказался очень эффективным, о чем свидетельствуют многочисленные ошибки, обнаруженные в проекте Cryptofuzz Вранкена [35].
Формальные методы и проверка программы также могут быть применены к реализации хеш-функции. Чуднов и др. [15] продемонстрировали, что реализация Keyed-Hash Mes-sage Authentication Code (HMAC) (с использованием хэш-функции SHA-256) библиотеки Amazon s2n соответствует формальной спецификации с использованием Software Analysis Workbench (SAW) Galois. Криптографическая библиотека HACL [32, 38] формально верифицируется с использованием структуры верификации F. Мы ссылаемся на Проценко и Хо [33] для объяснения того, как его реализация хэш-функции была недавно полностью переработана. Наконец, мы упомянем SPARKSkein Чепмена и др. [13] как реализацию финалиста SHA-3 Skein, которая была написана и проверена с использованием языка и набора инструментов SPARK [1].
Чепмен и др. [13] указали на ошибку в пакете отправки Skein в NIST. Ошибка связана с сообщениями длиной более 264-8 бит. Хотя это и нецелесообразно, это нарушает требование SHA-3 для отправки, что алгоритм-кандидат (и, следовательно, логически также правильная реализация алгоритма) «должен поддерживать максимальную длину сообщения не менее 264-1 бит» [26].
Оценка хеш-значения сообщения, которое предоставляется «на лету» с использованием любого количества вызовов Update() произвольной длины.
Чтобы доказать, что любое количество вызовов Update() произвольной длины приводит к правильному вычислению, достаточно доказать, что два вызова toUpdate() эквивалентны одному большему вызову Update() при конкатенации обоих входных данных.
Интерфейсы криптографических хеш-функций
API для конкурса SHA-3 был определен NIST [27], требуя структуры данных hashState и четырех вызовов функций: Init(), Update(), Final() и Hash(). API был разработан для 64-битных операционных систем, которые уже были широко распространены в начале конкурса SHA-3.
Цель структуры данных hashState — содержать «всю информацию, необходимую для описания текущего состояния алгоритма-кандидата SHA-3». Он должен содержать переменную hashbitlen для указания выходного размера конкретного экземпляра хеш-функции.
Четыре вызова функций показывают, как предполагается использовать hashState:
– Init() инициализирует структуру данных hashState.
– После инициализации можно выполнить любое количество вызовов Update() для обработки частей сообщения путем соответствующего обновления hashState. На практике этот API «инкрементного хеширования» обеспечивает значительное повышение эффективности, если сообщение недоступно все сразу или разделено на два или более несмежных массива [33, с. 9].
– Final() выполняет любую окончательную обработку, необходимую для hashState для вывода хеш-значения.
– Hash() обрабатывает сообщение одновременно, вызывая Init(), Update() и Final().
Предположим, что вычисления «все сразу» с использованием Init(), Update() и Final() верны. Тогда достаточным (но не необходимым) условием корректности вычислений с использованием любого количества вызовов Update() (как показано на рисунке 1) является:
Условие 1. Два последовательных вызова Update() изменяют hashState так же, как один вызов Update() при конкатенации обоих входов.
Можно видеть, что условие 1 является достаточным с помощью доказательства от противного, когда условие применяется рекурсивно, как показано на рисунке 2. Однако есть несколько случаев, когда условие 1 не является необходимым:
– Обозначим хэш-состояние как действительное тогда и только тогда, когда оно достижимо из Init(), за которым следует любое количество вызовов Update(). Тогда нет необходимости, чтобы условие 1 выполнялось, если hashState недействителен.
– Если функция Final() может вернуть одно и то же значение хеш-функции для двух различных, но допустимых структур данных hashState, условие 1 также не является обязательным. Однако на практике этого, по-видимому, не происходит, поскольку мы встречали только реализации, в которых hashState однозначно представляет уже обработанное сообщение.
– В NIST SHA-3 API все длины указываются в битах с использованием 64-битного целого числа без знака [27], а алгоритм-кандидат может устанавливать максимальную длину сообщения 264 − 1 бит [26]. Если указана максимальная длина сообщения, условие 1 не требуется для последовательности из двух вызовов Update(), которые превышают максимальную длину сообщения (поскольку в этом случае хеш-функция может быть не определена).
– Документ NIST SHA-3 API указывает, что все вызовы Update() содержат данные (в битах), которые делятся на восемь, за исключением, возможно, последнего вызова. Следовательно, для двух последовательных вызовов Update() мы можем ограничить первый вызов длиной данных, кратной восьми битам.
В следующем разделе нашей целью будет проверка условия 1 для данной реализации хеш-функции, возможно, вместе с некоторыми предварительными условиями для исключения вышеупомянутых случаев, когда условие 1 не является необходимым. Мы удалим некоторые строки кода: как и во многих предыдущих работах, мы стремимся к «менее амбициозной, но все же важной цели — формулированию частичных спецификаций поведения программы и предоставлению методологий и инструментов для проверки их корректности» [5].
Прежде чем закончить этот раздел, обратите внимание, что в этой статье мы будем предполагать, что Init(), Update() и Final() вызываются в "правильном" порядке. На практике может быть желательно вызывать Update() после Final(). Однако, как показали Benmocha [6], это может быть очень небезопасно для криптографических библиотек, которые не ожидают такого использования.
Проверка программы с помощью KLEE
В этой статье мы будем использовать KLEE [11], инструмент символьного выполнения, построенный поверх архитектуры компилятора LLVM (Low-Level Virtual Machine) [21].
Хотя типичным использованием KLEE является автоматическое создание тестовых векторов, обеспечивающих высокое покрытие кода, его также можно использовать для доказательства полной функциональной эквивалентности двух реализаций [11, §5.5]. Всякий раз, когда KLEE сталкивается с ветвью выполнения, основанной на символическом значении, он будет (концептуально) следовать обеим ветвям, поддерживая набор ограничений, называемых условиями пути для каждой ветви. Недостатком этого подхода является то, что количество путей может расти очень быстро.
В отличие от CBMC [16], который представляет собой средство проверки ограниченной модели для программ на C и C++, KLEE не требует ограничения количества итераций для каждого цикла. Конкурс NIST SHA-3 требовал, чтобы максимальная длина сообщения составляла не менее 264 - 1 бит, и обычно можно увидеть хеш-функции, которые итеративно обрабатывают сообщение, используя функцию сжатия, которая принимает 512 или 1024 бита на входе. Вычисление хеша для таких больших сообщений на практике невозможно, однако мы увидим, что наш подход с использованием KLEE обрабатывает такие входные данные довольно быстро (и без необходимости раскручивания цикла или ручных усилий по перезаписи циклов).
В следующих разделах мы покажем, как применить KLEE к эталонным реализациям пяти финалистов SHA-3, а также к реализации SHA-3 XKCP и хеш-функциям, реализованным в библиотеке Apple CoreCrypto. В этой статье мы предоставляем только полный исходный код для наших экспериментов KLEE с алгоритмом JH. Однако код для всех наших экспериментов будет доступен как программный артефакт.
В таблице 1 приведены данные о времени выполнения для 256-битного выходного хеш-значения, за исключением Keccak и SHA-3, где мы выберем скорость 1024 бит. Мы обнаружили, что время выполнения обычно не зависит от длины хеш-значения. Наши эксперименты проводились на процессоре Intel Core i7-1165G7 с использованием KLEE 2.3 с решателем по умолчанию STP (Simple теорема Prover) [12, 19].
4.1 JH
JH [37] — это хеш-функция, разработанная Хонджуном Ву, которая вышла в финал конкурса NIST SHA-3. Как требуется для всех представлений [26], JH поддерживает длину хэша 224, 256, 384 и 512 бит. Сообщение дополняется до числа, кратного 512 битам, а затем разбивается на 512-битные блоки, которые обрабатываются той же функцией сжатия F8().
Таблица 1. Время выполнения KLEE (в минутах и секундах) для скорости 1024 бита (для Keccak и SHA-3) или длины вывода хэша 256 бит (для всех остальных хеш-функций). Второй столбец — это время выполнения для поиска тестового вектора, выявляющего ошибку (если код неверен), а третий столбец — время выполнения для подтверждения правильности (после исправления реализации, если есть ошибка).
Мы предоставляем весь jh klee.c, который мы использовали в нашем эксперименте, в листинге 1. Он содержит функцию Update(), указанную в jh ref.h пакета представления JH. Для удобства чтения мы скорректировали отступ, а для компактности убрали комментарии к исходному коду. Единственное другое изменение, которое мы внесли в Update(), — это закомментировать строки, включающие memcpy() и F8(), поскольку наша (частичная) проверка эквивалентности не включает ни содержимое сообщения (только его длину), ни предполагают реализацию функции сжатия F8(). Более того, в этой статье мы не делаем никаких утверждений о правильности функций Init(), Final() или Hash().
В листинге 2 мы предоставляем Makefile, который использует Docker как простой и переносимый способ запуска KLEE на jh klee.c. Он либо вернет тестовый вектор, нарушающий условие 1, либо докажет, что такого тестового вектора не существует. Мы обнаруживаем, что через 50 секунд KLEE доказывает (частичную) согласованность функции Update(). Обзор времени выполнения для всех наших экспериментов приведен в таблице 1.
Пять строк в листинге 1 отмечены комментарием // необязательный в соответствии с рассуждениями в разделе 3. Их можно безопасно опустить с единственным недостатком, заключающимся в том, что они примерно удваивают время выполнения KLEE. Однако эти пять строк могут быть полезны для адаптации подхода к другим реализациям-кандидатам SHA-3, где они могут понадобиться.
Листинг 1. Приложение к JH (jh klee.c).
4.2 Skein
Skein — это представление SHA-3 финального раунда, разработанное Ferguson et al. [17]. Как и JH, его основное предложение обрабатывает сообщение блоками по 512 бит независимо от длины хеш-значения.
Хотя алгоритм, используемый реализацией Скейна для обработки сообщения в блоках, следует совершенно другому подходу по сравнению с JH, система проверки KLEE выглядит очень похожей с тем основным отличием, что утверждение о размере данных в буфере заменяется утверждением о u.h.bCnt .
Время выполнения даже меньше, чем для JH, так как KLEE требуется всего 34 секунды, чтобы доказать отсутствие тестовых векторов, нарушающих утверждения.
4.3 BLAKE
Другой представленный на финальном этапе SHA-3 — это хэш-функция BLAKE от Aumas-son. [2]. В зависимости от длины хеша BLAKE использует либо 512-битную, либо 1024-битную функцию сжатия. Он имеет переменную datalen для отслеживания количества битов в буфере, аналогично размеру данных в буфере для JH.
Однако он также отслеживает счетчик общего количества битов сообщения, обработанных на данный момент. В зависимости от длины хеша этот счетчик хранится либо в массиве с двумя 32-битными целыми числами без знака, либо в массиве с двумя 64-битными целыми числами без знака.
В сентябре 2015 года веб-сайт BLAKE [4] был обновлен, чтобы исправить ошибку во всех реализациях, представленных во время конкурса SHA-3. Используя наш подход, KLEE легко заново обнаруживает эту ошибку всего за пять секунд.
В частности, для 256-битного хеш-значения он предоставляет тестовый вектор, показывающий, что Update() для 384 битов, за которыми следуют 512 бит, приводит к другому состоянию, чем однократное обновление 384+512=896 бит.
Это согласуется с условиями ошибки, описанными Муха [24]: ошибка возникает, когда за неполным блоком (менее 512 бит) следует полный блок (512 бит).
Используя обновленный код на сайте BLAKE [4], мы сталкиваемся с препятствием при запуске KLEE. Он не завершается в течение разумного промежутка времени, так как страдает от проблемы взрыва пути, упомянутой в разделе 2.
Дальнейший анализ показывает, что ветвь if внутри цикла while является виновником. Для размера блока 512 бит код BLAKE выглядит следующим образом:
We found that this path explosion can be avoided if the counter of the mes-sage bits hashed so far is not stored as an array of two unsigned 32-bit variables, but as one unsigned 64-bit variable. More specifically, we change the BLAKE code as follows:
Мы обнаружили, что этого взрыва пути можно избежать, если счетчик хешированных до сих пор битов сообщения хранится не в виде массива из двух 32-битных переменных без знака, а в виде одной 64-битной переменной без знака. В частности, мы меняем код BLAKE следующим образом:
4.4 Grøstl
Теперь мы переходим к другому финалисту SHA-3: Grøstl от Gauravaram et al. [20]. Сообщение разбивается на 512-битные или 1024-битные блоки в зависимости от длины хеш-значения. Насколько нам известно, об ошибках в этой реализации не сообщалось.
В эталонной реализации Grøstl не все циклы находятся внутри Update(), но также и внутри функции Transform(), которая обрабатывает не только один блок, но и любое количество полных блоков. Здесь мы уже заметили первую проблему: все переменные, представляющие длину сообщения, являются 64-битными целыми числами, но функция Transform() объявлена с параметром (заданным пользователем) 32-битного типа u32, что приводит к некорректному неявному приведению .
Поскольку мы применяем наш подход с использованием KLEE, поиск второй ошибки занимает шесть секунд. Ошибка снова связана с использованием неверных типов: переменная index объявлена как int, что является 32-битным типом данных на 64-битных процессорах. Однако для достаточно больших входных сообщений значение индекса переполняется, что приводит к неопределенному поведению в языке программирования C.
В листинге 3 мы предоставляем программу для демонстрации ошибки. При компиляции с использованием gcc программа записывает в память большое количество данных, что почти наверняка приводит к сбою. Становится интереснее, когда мы компилируем эту программу с помощью clang. Неопределенное поведение приводит к тому, что clang выполняет оптимизацию, которая позволяет избежать переполнения буфера, но вместо этого выводит один и тот же хэш для двух сообщений разной длины. Таким образом, реализация нарушает свойство устойчивости к коллизиям (см. раздел 1).
Мы искали реализации, которые могут быть уязвимы из-за этой ошибки, но не обнаружили ни одного проекта или продукта, которые могли бы быть затронуты. По этой причине мы не отправили отчет об уязвимости. Наиболее заметное использование Grøstl, которое мы обнаружили, было частью алгоритма проверки работоспособности начальной версии криптовалюты Monero. Однако использование Grøstl там давно прекращено.
С исправлением двух ошибок типа доказать правильность с помощью KLEE оказалось намного сложнее, чем ожидалось. Мы снова сталкиваемся с проблемой взрыва пути, которую мы решили, жестко закодировав размер блока и переписав цикл, который побайтно копировал данные в буфер. С этими модификациями KLEE завершается через десять секунд с доказательством того, что утверждения недостижимы.
Листинг 3. Из-за неопределенного поведения ошибка Grøstl приводит к ошибке сегментации при компиляции с использованием gcc или коллизии при компиляции с использованием clang (groestl bug.c).
4.5 Keccak
Единственный финалист SHA-3, который мы еще не изучали в этой статье, — это заявка, выигравшая конкурс: Keccak by Bertoni [9]. Keccak дополняет сообщение и разбивает его на блоки, которые затем обрабатываются криптографической перестановкой. Размер блока, также известный как скорость, имеет значение по умолчанию 1024 бита [9]. Сейчас мы сосредоточимся на этом значении по умолчанию, а влияние размера блока обсудим позже.
Об уязвимости сообщил Муха, и ей присвоен код CVE-2022-37454 [31]. Как победитель конкурса SHA-3 эталонный код Keccak довольно широко распространен, и уязвимость затронула различные проекты, такие как Python и PHP. Подробности об уязвимости см. у Муха и Celi [23]. В этой статье мы объясняем, как уязвимость была обнаружена с помощью KLEE.
Прямой подход с использованием KLEE не заканчивается в разумные сроки. Следовательно, может быть полезно исключить бесконечный цикл в реализации Keccak, так как это приведет к тому, что KLEE также войдет в бесконечный цикл.
Для завершения цикла while(i < databitlen) достаточным, но не необходимым условием является то, что i продвигается вперед в каждой итерации цикла. Это легко проверить, введя старую переменную i, которая инициализируется значением i. Когда переменная i изменяется, мы гарантируем, что она отличается от предыдущей итерации цикла:
В конце цикла устанавливаем old i = i. С этим дополнительным кодом для обнаружения бесконечных циклов KLEE требуется менее секунды для вывода ошибки утверждения. Анализируя тестовый вектор, предоставленный KLEE, мы можем подтвердить, что действительно нашли бесконечный цикл. Обратите внимание, что этот дополнительный код используется только для того, чтобы мы могли легко обнаружить бесконечный цикл в KLEE, дополнительный код не требуется для правильной реализации (которая не содержит бесконечный цикл).
Оказывается, есть не только вход, который приводит к бесконечному циклу, но и другой вход, который вызывает запись большого количества данных в память, что приводит к ошибке сегментации. Детали этого переполнения буфера приведены Муха и Celi [23] и выходят за рамки данной статьи.
Ошибка проявляется, когда в буфере уже есть x битов данных, а затем выполняется Update() из 232 - x битов или более. В приведенном ниже коде Кекчака могут возникнуть две проблемы: старшие биты могут быть отброшены из-за неправильного приведения к 32-битному целому числу, а добавление может переполниться:
Мы можем исправить эту ошибку, немного изменив код так, чтобы partialBlock не превышал размера блока. В этом случае для partialBlock достаточно 32-битного целого числа:
Для исправленного кода KLEE требуется всего 39 секунд, чтобы доказать, что утверждения не могут быть нарушены.
Наконец, мы отмечаем, что KLEE, по-видимому, не прекращает работу в разумные сроки для размеров блоков, не кратных двум. Такие размеры блоков были предложены во время конкурса SHA-3 для обеспечения различных уровней безопасности. К сожалению, решатели часто сталкиваются с трудностями при делении на константу, не являющуюся степенью двойки. KLEE имеет флаг -solver-optimize-divides, который пытается оптимизировать такие деления, прежде чем передать их решателю. Однако даже с этим флагом мы не смогли найти способ заставить KLEE завершаться для размеров блоков, не кратных двум.
4.6 XKCP (SHA-3)
Расширенный пакет кода Keccak (XKCP) [8] поддерживается командой Keccak. Он содержит стандартизированный NIST вариант хеш-функции Keccak. Между представлением Keccak в финальном раунде и стандартом SHA-3 отличается только заполнение сообщения.
Реализация SHA-3 в XKCP основана на реализации представления Keccak в финальном раунде. Тем не менее, он претерпел довольно много рефакторинга. По этой причине мы указываем XKCP SHA-3 как отдельную реализацию в таблице 1.
Та же ошибка, которая влияет на отправку Keccak в финальном раунде, присутствует и в XKCP, хотя для ее запуска требуются два вызова Update() с общей длиной 232 байта (4 ГиБ), а не 232 бита (512 МиБ). Более того, у него есть еще одна ошибка (отсутствующая в представлении Keccak), из-за которой сообщения чуть меньше 264 байт приводят к бесконечному циклу. Это связано с переполнением в операции сравнения (dataByteLen >= (i + rateInBytes)), которое в исправленной версии кода заменено на dataByteLen-i >= rateInBytes.
Используя KLEE, требуется менее одной секунды, чтобы предоставить тестовый вектор, который вызывает ошибку, при условии, что мы снова расширим код для обнаружения бесконечных циклов. Для размера блока 1024 бит KLEE требуется 20 секунд, чтобы доказать, что утверждения недостижимы.
4.7 CoreCrypto
Наконец, мы хотели бы вернуться к бесконечному циклу в библиотеке Apple CoreCrypto. Уязвимость затронула 11 из 12 реализованных хеш-функций и получила код CVE-2019-8741 [30]. Подробности об ошибке см. у Mouha и Celi [22].
Подход с использованием KLEE довольно прост в реализации. KLEE находит уязвимый тестовый вектор менее чем за секунду для исходной реализации и может доказать недостижимость утверждений менее чем за три минуты для обновленной реализации.
Здесь мы хотим отметить интересное совпадение. Если мы начнем с исправленной реализации Update() в Apple CoreCrypto с небольшим рефакторингом (например, заменив len на dataByteLen-i, переименовав переменные и функции и удалив ненужный код), мы получим исправленную реализацию Update(), который используется XKCP. Кажется, что Update() достаточно прост, чтобы две команды могли независимо прийти к одной и той же реализации (вплоть до простого рефакторинга), но достаточно сложен, чтобы содержать уязвимости, которые оставались нераскрытыми более десяти лет.
Ограничения и обсуждение
После завершения конкурса SHA-3 в 2012 г. уязвимости были обнаружены в реализациях финалиста SHA-3 BLAKE в 2015 г. [4], в 11 из 12 реализованных хэш-функций библиотеки Apple CoreCrypto в 2019 г. [30], а недавно в эталонной реализации победителя SHA-3 Keccak [31].
Все эти уязвимости были связаны с функцией Update(), которая используется для обработки сообщения блоками. Тем не менее, влияние уязвимостей совершенно различно. В то время как реализация XKCP SHA-3 содержала уязвимость переполнения буфера с возможностью выполнения произвольного кода, влияние уязвимости в библиотеке Apple CoreCrypto ограничивается бесконечным циклом. Уязвимость BLAKE нельзя использовать для запуска какой-либо ошибки времени выполнения, однако ее можно использовать для нарушения свойства устойчивости к коллизиям хеш-функции.
Это позволяет нам сделать первое наблюдение, что подходы к предотвращению проблем с безопасностью памяти (такие как обеспечение соблюдения стандартов кодирования, песочница или переход от C/C++ к более безопасным языкам программирования) были бы полезными, но недостаточными, чтобы избежать уязвимостей, описанных в этом документе. бумага. Мы также достигаем пределов подходов с использованием тестовых векторов: тест больших данных (LDT) может занять довольно много времени для выполнения сообщения размером 4 ГиБ для обнаружения ошибок в библиотеке Apple CoreCrypto, а для ошибки XKCP — один большой вызов. to Update() не активирует уязвимость (поскольку требует, чтобы некоторые данные уже присутствовали в буфере).
Поэтому может быть интересно рассмотреть подходы, использующие символьное выполнение. Подход, который мы описываем в этой статье с использованием KLEE, оказывается довольно простым в развертывании. Мы выполнили (частичную) проверку эквивалентности функции Update(), закомментировав строки, включающие содержимое сообщения и функцию сжатия. В производственной среде средства проверки переопределяют эти функции, а не комментируют их, поэтому проверки могут быть частью процесса непрерывной интеграции, подобного тому, как Amazon Web Services в настоящее время развертывает CBMC [14].
В то время как подходы, использующие большие тестовые векторы, могут занять некоторое время (особенно на медленном оборудовании), символическое выполнение может найти ошибки за несколько секунд или доказать правильность менее чем за 12 минут, как показано в таблице 1. приблизиться к низкозатратному подходу к формальным методам и проверке программ и, возможно, даже к более строгим подходам, используемым в таких проектах, как HACL* [32, 38] или SPARKSkein [13].
Действительно, тестом здесь было бы увидеть, насколько легко наш подход распространяется на другие заявки на конкурс SHA-3. Мы изучили реализации всех пяти финалистов конкурса и обнаружили, что можем либо доказать правильность, либо обнаружить новые ошибки (как в случае с Grøstl, где мы показываем, как неопределенное поведение может нарушить устойчивость к коллизиям реализации хеш-функции). И хотя наш подход предназначен для проверки соответствия двух вызовов Update() одному вызову конкатенации обоих входных данных, он также находит ошибки, которые могут быть вызваны одним вызовом Update(), как показано ошибками в Grøstl и Библиотека Apple CoreCrypto (поскольку они заставляют KLEE входить в бесконечный цикл).
Наконец, хотя наш подход был полезен для обнаружения ошибок, мы еще раз подчеркиваем, что недостаточно утверждать, что реализации правильны. Например, мы не делаем заявлений о потенциальных ошибках в Init(), Final() или Hash(), а также о потенциальных ошибках в закомментированных строках Update(). Мы также не занимаемся ошибками, связанными с использованием API, например обнаруженными Benmocha et al. [6].
Заключение и будущая работа
Мы пересмотрели реализации пяти финалистов конкурса NIST SHA-3. С 2008 по 2012 год они подвергались тщательному публичному рассмотрению. Однако только в 2015 году была обнаружена уязвимость в реализации BLAKE, а совсем недавно — в победившей заявке Kecak с использованием техники, которая впервые описана в этом документе.
Мы показали, как эти ошибки могут быть (повторно) обнаружены всего за несколько секунд, требуя лишь минимальных усилий для создания системы проверки исходного кода. Более того, мы также обнаружили уязвимость в представлении Grøstl, позволяющую создавать два сообщения, которые приводят к одному и тому же значению хеш-функции при компиляции с помощью clang. Наш подход также позволил бы обнаружить ошибку в библиотеке Apple CoreCrypto, о которой сообщалось в 2019 году.
Наш подход требует символьного выполнения, чтобы проверить, эквивалентны ли два вызова Update() (с некоторыми удаленными строками кода) одному вызову Update() при конкатенации обоих входных данных. Для проверки этого свойства мы использовали фреймворк символьного исполнения KLEE.
К сожалению, наш подход основан на пробах и ошибках. В частности, чтобы доказать, что ни одно из утверждений не работает, нам иногда приходилось немного переписывать код, чтобы избежать сбоя KLEE из-за взрыва пути. Это ограничение, поскольку в идеале мы хотели бы вообще не вносить изменений в исходный код, но, возможно, это приемлемый компромисс для достижения цели (частичной) проверки программы.
Интересное направление будущей работы — найти способ расширить наш подход на Keccak и SHA-3, когда размер блока не является степенью двойки.
Переведено специально для xss.pro
Автор перевода: yashechka
Источник: Nicky Mouha Strativia, Largo, MD, USA nicky@mouha.be
Введение
(Криптографическая) хэш-функция принимает сообщение переменной длины и превращает его в вывод фиксированной длины, известный как «хеш-значение» или «хэш». Чтобы хеш-функция была безопасной, должно быть невозможно с вычислительной точки зрения инвертировать функцию для данного хэша (устойчивость к прообразу) или найти два разных сообщения, которые приводят к одному и тому же хешу (устойчивость к коллизиям). Эти свойства позволяют использовать хеш-значение вместо самого сообщения в схеме цифровой подписи, так что успешная проверка подписи подтверждает, что сообщение не было изменено.
В ответ на атаку криптоанализа на хэш-функцию SHA-1, представленную на CRYPTO 2005 Ваном и др. [36], NIST решил запустить конкурс SHA-3 на новый стандарт хэш-функции [29]. Конкурс был объявлен в ноябре 2007 г. К октябрю 2008 г. было получено 64 заявки, а 51 была выбрана в качестве кандидатов в первом туре в декабре 2008 г. Четырнадцать из них прошли в качестве кандидатов во второй тур в июле 2009 г., а пять финалистов ( BLAKE, Grøstl, JH, Keccak и Skein) были объявлены в декабре 2010 года. Конкурс SHA-3 завершился в октябре 2012 года, когда Кекчак был объявлен победителем.
Пакеты, подаваемые на конкурс SHA-3, должны были включать эталонные и оптимизированные реализации на языке программирования C [27]. NIST определил используемый интерфейс прикладного программирования (API) (см. Раздел 3), а также тестовые векторы, которые требовались в каждом пакете отправки.
Поскольку пакеты, представленные на конкурс SHA-3, подвергались публичному рассмотрению, в нескольких заявках в 2008 и 2009 годах сообщалось об ошибках. Систематический анализ, проведенный Forsythe и Held из Fortify Software [18], обнаружил множество ошибок, которые обычно появляются в коде C такие как чтение за пределами границ, утечки памяти и разыменование нулевого указателя. В течение оставшейся части конкурса об ошибках не сообщалось, и в конечном итоге получившийся стандарт SHA-3 стал широко применяться во многих криптографических библиотеках.
Однако в сентябре 2015 года реализация на сайте BLAKE была обновлена с комментарием: «исправлена ошибка, которая давала неверные хэши в конкретных случаях использования» [4]. В 2018 году Муха и соавт. [24] повторно обнаружили ошибку, используя новую методологию тестирования, которая в конечном итоге была интегрирована в проект Google Wycheproof [10], и показали, что ошибка позволяет нарушить устойчивость хеш-функции к коллизиям.
На CT-RSA 2020 Муха и Celi [22] показали уязвимость, затрагивающую 11 из 12 реализованных хеш-функций в библиотеке Apple CoreCrypto. Уязвимость требовала вызова реализации на входах размером не менее 4 ГиБ, что приводило к бесконечному циклу. Эта уязвимость показала ограничение в программе проверки криптографических алгоритмов NIST (CAVP), которая не выполняла тесты хеш-функций для входных данных размером более 65 535 бит. Чтобы обойти это ограничение, NIST ввел тест больших данных (LDT).
В октябре 2022 года Муха [31] обнаружил уязвимость, которая повлияла как на пакет представления Keccak для финального раунда, так и на итоговую реализацию SHA-3 его разработчиками. В зависимости от конкретных введенных данных уязвимость приводила либо к бесконечному циклу, либо к переполнению буфера, когда предоставленные злоумышленником значения подвергались операции XOR в памяти [23].
Наши вклады.
Недостаток предыдущей работы по поиску уязвимостей в реализациях хеш-функций заключается в том, что им не хватает общности и они явно не соответствуют требованиям, поскольку продолжают обнаруживаться новые уязвимости, которые оставались незамеченными более десяти лет (несмотря на широкое общественное внимание). Новый вклад этой статьи состоит в том, чтобы попытаться преодолеть эту проблему, представив новый подход, который можно использовать для поиска уязвимостей в реализациях хеш-функций библиотеки Apple CoreCrypto, а также в трех из пяти представленных финалистов SHA-3: БЛЕЙК, Кекчак и Грёстль. В этой статье объясняется, как была обнаружена уязвимость в Keccak. Уязвимость в Grøstl — это новый вклад в эту статью, о котором ранее не сообщалось. Наш подход включает символическое выполнение для поиска ошибок в течение нескольких секунд, в то время как выполнение тестовых векторов может занять гораздо больше времени.
Связанные работы
Подход NIST к тестированию криптографических реализаций восходит к 1977 году, когда в SP 500-20 были введены два набора тестовых векторов для стандарта шифрования данных (DES) [25]. Теперь известный как тесты известных ответов (KAT) или статические алгоритмические функциональные тесты (AFT), первый набор тестовых векторов был предназначен для «полного применения таблиц нелинейных замен» (S-блоков) DES. Второй набор тестовых векторов, называемый тестами Монте-Карло (MCT), содержал «псевдослучайные данные для проверки того, что устройство не было разработано только для того, чтобы пройти набор тестов». Первоначально предназначенный для тестирования аппаратных реализаций, этот подход может применяться как к аппаратному, так и к программному обеспечению и лежит в основе Программы проверки криптографических алгоритмов NIST (CAVP).
Заявки на конкурс NIST SHA-3 должны были включать реализации на языке программирования C. NIST определил API [27] и предоставил исходный код для создания KAT и MCT [28]. Эти KAT и MCT помогли обеспечить согласованность различных реализаций одного и того же алгоритма. Кроме того, интересным нововведением стало включение чрезвычайно длинного сообщения KAT, которое предоставляло сообщение размером 1 ГиБ с целью обеспечения правильной обработки больших входных данных.
Для (аутентифицированных) алгоритмов шифрования платформы SUPERCOP [7] и BRU-TUS [34] выполняют некоторые дополнительные тесты, такие как проверка правильности обработки перекрывающихся входных данных или того, возвращает ли шифрование с последующим дешифрованием исходный открытый текст.
Аумассон и Ромайлер представили криптодифференциальный фаззинг [3], который использует фаззер для сравнения выходных данных различных криптографических библиотек и поиска расхождений. Такой подход оказался очень эффективным, о чем свидетельствуют многочисленные ошибки, обнаруженные в проекте Cryptofuzz Вранкена [35].
Формальные методы и проверка программы также могут быть применены к реализации хеш-функции. Чуднов и др. [15] продемонстрировали, что реализация Keyed-Hash Mes-sage Authentication Code (HMAC) (с использованием хэш-функции SHA-256) библиотеки Amazon s2n соответствует формальной спецификации с использованием Software Analysis Workbench (SAW) Galois. Криптографическая библиотека HACL [32, 38] формально верифицируется с использованием структуры верификации F. Мы ссылаемся на Проценко и Хо [33] для объяснения того, как его реализация хэш-функции была недавно полностью переработана. Наконец, мы упомянем SPARKSkein Чепмена и др. [13] как реализацию финалиста SHA-3 Skein, которая была написана и проверена с использованием языка и набора инструментов SPARK [1].
Чепмен и др. [13] указали на ошибку в пакете отправки Skein в NIST. Ошибка связана с сообщениями длиной более 264-8 бит. Хотя это и нецелесообразно, это нарушает требование SHA-3 для отправки, что алгоритм-кандидат (и, следовательно, логически также правильная реализация алгоритма) «должен поддерживать максимальную длину сообщения не менее 264-1 бит» [26].
Оценка хеш-значения сообщения, которое предоставляется «на лету» с использованием любого количества вызовов Update() произвольной длины.
Чтобы доказать, что любое количество вызовов Update() произвольной длины приводит к правильному вычислению, достаточно доказать, что два вызова toUpdate() эквивалентны одному большему вызову Update() при конкатенации обоих входных данных.
Интерфейсы криптографических хеш-функций
API для конкурса SHA-3 был определен NIST [27], требуя структуры данных hashState и четырех вызовов функций: Init(), Update(), Final() и Hash(). API был разработан для 64-битных операционных систем, которые уже были широко распространены в начале конкурса SHA-3.
Цель структуры данных hashState — содержать «всю информацию, необходимую для описания текущего состояния алгоритма-кандидата SHA-3». Он должен содержать переменную hashbitlen для указания выходного размера конкретного экземпляра хеш-функции.
Четыре вызова функций показывают, как предполагается использовать hashState:
– Init() инициализирует структуру данных hashState.
– После инициализации можно выполнить любое количество вызовов Update() для обработки частей сообщения путем соответствующего обновления hashState. На практике этот API «инкрементного хеширования» обеспечивает значительное повышение эффективности, если сообщение недоступно все сразу или разделено на два или более несмежных массива [33, с. 9].
– Final() выполняет любую окончательную обработку, необходимую для hashState для вывода хеш-значения.
– Hash() обрабатывает сообщение одновременно, вызывая Init(), Update() и Final().
Предположим, что вычисления «все сразу» с использованием Init(), Update() и Final() верны. Тогда достаточным (но не необходимым) условием корректности вычислений с использованием любого количества вызовов Update() (как показано на рисунке 1) является:
Условие 1. Два последовательных вызова Update() изменяют hashState так же, как один вызов Update() при конкатенации обоих входов.
Можно видеть, что условие 1 является достаточным с помощью доказательства от противного, когда условие применяется рекурсивно, как показано на рисунке 2. Однако есть несколько случаев, когда условие 1 не является необходимым:
– Обозначим хэш-состояние как действительное тогда и только тогда, когда оно достижимо из Init(), за которым следует любое количество вызовов Update(). Тогда нет необходимости, чтобы условие 1 выполнялось, если hashState недействителен.
– Если функция Final() может вернуть одно и то же значение хеш-функции для двух различных, но допустимых структур данных hashState, условие 1 также не является обязательным. Однако на практике этого, по-видимому, не происходит, поскольку мы встречали только реализации, в которых hashState однозначно представляет уже обработанное сообщение.
– В NIST SHA-3 API все длины указываются в битах с использованием 64-битного целого числа без знака [27], а алгоритм-кандидат может устанавливать максимальную длину сообщения 264 − 1 бит [26]. Если указана максимальная длина сообщения, условие 1 не требуется для последовательности из двух вызовов Update(), которые превышают максимальную длину сообщения (поскольку в этом случае хеш-функция может быть не определена).
– Документ NIST SHA-3 API указывает, что все вызовы Update() содержат данные (в битах), которые делятся на восемь, за исключением, возможно, последнего вызова. Следовательно, для двух последовательных вызовов Update() мы можем ограничить первый вызов длиной данных, кратной восьми битам.
В следующем разделе нашей целью будет проверка условия 1 для данной реализации хеш-функции, возможно, вместе с некоторыми предварительными условиями для исключения вышеупомянутых случаев, когда условие 1 не является необходимым. Мы удалим некоторые строки кода: как и во многих предыдущих работах, мы стремимся к «менее амбициозной, но все же важной цели — формулированию частичных спецификаций поведения программы и предоставлению методологий и инструментов для проверки их корректности» [5].
Прежде чем закончить этот раздел, обратите внимание, что в этой статье мы будем предполагать, что Init(), Update() и Final() вызываются в "правильном" порядке. На практике может быть желательно вызывать Update() после Final(). Однако, как показали Benmocha [6], это может быть очень небезопасно для криптографических библиотек, которые не ожидают такого использования.
Проверка программы с помощью KLEE
В этой статье мы будем использовать KLEE [11], инструмент символьного выполнения, построенный поверх архитектуры компилятора LLVM (Low-Level Virtual Machine) [21].
Хотя типичным использованием KLEE является автоматическое создание тестовых векторов, обеспечивающих высокое покрытие кода, его также можно использовать для доказательства полной функциональной эквивалентности двух реализаций [11, §5.5]. Всякий раз, когда KLEE сталкивается с ветвью выполнения, основанной на символическом значении, он будет (концептуально) следовать обеим ветвям, поддерживая набор ограничений, называемых условиями пути для каждой ветви. Недостатком этого подхода является то, что количество путей может расти очень быстро.
В отличие от CBMC [16], который представляет собой средство проверки ограниченной модели для программ на C и C++, KLEE не требует ограничения количества итераций для каждого цикла. Конкурс NIST SHA-3 требовал, чтобы максимальная длина сообщения составляла не менее 264 - 1 бит, и обычно можно увидеть хеш-функции, которые итеративно обрабатывают сообщение, используя функцию сжатия, которая принимает 512 или 1024 бита на входе. Вычисление хеша для таких больших сообщений на практике невозможно, однако мы увидим, что наш подход с использованием KLEE обрабатывает такие входные данные довольно быстро (и без необходимости раскручивания цикла или ручных усилий по перезаписи циклов).
В следующих разделах мы покажем, как применить KLEE к эталонным реализациям пяти финалистов SHA-3, а также к реализации SHA-3 XKCP и хеш-функциям, реализованным в библиотеке Apple CoreCrypto. В этой статье мы предоставляем только полный исходный код для наших экспериментов KLEE с алгоритмом JH. Однако код для всех наших экспериментов будет доступен как программный артефакт.
В таблице 1 приведены данные о времени выполнения для 256-битного выходного хеш-значения, за исключением Keccak и SHA-3, где мы выберем скорость 1024 бит. Мы обнаружили, что время выполнения обычно не зависит от длины хеш-значения. Наши эксперименты проводились на процессоре Intel Core i7-1165G7 с использованием KLEE 2.3 с решателем по умолчанию STP (Simple теорема Prover) [12, 19].
4.1 JH
JH [37] — это хеш-функция, разработанная Хонджуном Ву, которая вышла в финал конкурса NIST SHA-3. Как требуется для всех представлений [26], JH поддерживает длину хэша 224, 256, 384 и 512 бит. Сообщение дополняется до числа, кратного 512 битам, а затем разбивается на 512-битные блоки, которые обрабатываются той же функцией сжатия F8().
Таблица 1. Время выполнения KLEE (в минутах и секундах) для скорости 1024 бита (для Keccak и SHA-3) или длины вывода хэша 256 бит (для всех остальных хеш-функций). Второй столбец — это время выполнения для поиска тестового вектора, выявляющего ошибку (если код неверен), а третий столбец — время выполнения для подтверждения правильности (после исправления реализации, если есть ошибка).
Мы предоставляем весь jh klee.c, который мы использовали в нашем эксперименте, в листинге 1. Он содержит функцию Update(), указанную в jh ref.h пакета представления JH. Для удобства чтения мы скорректировали отступ, а для компактности убрали комментарии к исходному коду. Единственное другое изменение, которое мы внесли в Update(), — это закомментировать строки, включающие memcpy() и F8(), поскольку наша (частичная) проверка эквивалентности не включает ни содержимое сообщения (только его длину), ни предполагают реализацию функции сжатия F8(). Более того, в этой статье мы не делаем никаких утверждений о правильности функций Init(), Final() или Hash().
В листинге 2 мы предоставляем Makefile, который использует Docker как простой и переносимый способ запуска KLEE на jh klee.c. Он либо вернет тестовый вектор, нарушающий условие 1, либо докажет, что такого тестового вектора не существует. Мы обнаруживаем, что через 50 секунд KLEE доказывает (частичную) согласованность функции Update(). Обзор времени выполнения для всех наших экспериментов приведен в таблице 1.
Пять строк в листинге 1 отмечены комментарием // необязательный в соответствии с рассуждениями в разделе 3. Их можно безопасно опустить с единственным недостатком, заключающимся в том, что они примерно удваивают время выполнения KLEE. Однако эти пять строк могут быть полезны для адаптации подхода к другим реализациям-кандидатам SHA-3, где они могут понадобиться.
Листинг 1. Приложение к JH (jh klee.c).
4.2 Skein
Skein — это представление SHA-3 финального раунда, разработанное Ferguson et al. [17]. Как и JH, его основное предложение обрабатывает сообщение блоками по 512 бит независимо от длины хеш-значения.
Хотя алгоритм, используемый реализацией Скейна для обработки сообщения в блоках, следует совершенно другому подходу по сравнению с JH, система проверки KLEE выглядит очень похожей с тем основным отличием, что утверждение о размере данных в буфере заменяется утверждением о u.h.bCnt .
Время выполнения даже меньше, чем для JH, так как KLEE требуется всего 34 секунды, чтобы доказать отсутствие тестовых векторов, нарушающих утверждения.
4.3 BLAKE
Другой представленный на финальном этапе SHA-3 — это хэш-функция BLAKE от Aumas-son. [2]. В зависимости от длины хеша BLAKE использует либо 512-битную, либо 1024-битную функцию сжатия. Он имеет переменную datalen для отслеживания количества битов в буфере, аналогично размеру данных в буфере для JH.
Однако он также отслеживает счетчик общего количества битов сообщения, обработанных на данный момент. В зависимости от длины хеша этот счетчик хранится либо в массиве с двумя 32-битными целыми числами без знака, либо в массиве с двумя 64-битными целыми числами без знака.
В сентябре 2015 года веб-сайт BLAKE [4] был обновлен, чтобы исправить ошибку во всех реализациях, представленных во время конкурса SHA-3. Используя наш подход, KLEE легко заново обнаруживает эту ошибку всего за пять секунд.
В частности, для 256-битного хеш-значения он предоставляет тестовый вектор, показывающий, что Update() для 384 битов, за которыми следуют 512 бит, приводит к другому состоянию, чем однократное обновление 384+512=896 бит.
Это согласуется с условиями ошибки, описанными Муха [24]: ошибка возникает, когда за неполным блоком (менее 512 бит) следует полный блок (512 бит).
Используя обновленный код на сайте BLAKE [4], мы сталкиваемся с препятствием при запуске KLEE. Он не завершается в течение разумного промежутка времени, так как страдает от проблемы взрыва пути, упомянутой в разделе 2.
Дальнейший анализ показывает, что ветвь if внутри цикла while является виновником. Для размера блока 512 бит код BLAKE выглядит следующим образом:
We found that this path explosion can be avoided if the counter of the mes-sage bits hashed so far is not stored as an array of two unsigned 32-bit variables, but as one unsigned 64-bit variable. More specifically, we change the BLAKE code as follows:
Мы обнаружили, что этого взрыва пути можно избежать, если счетчик хешированных до сих пор битов сообщения хранится не в виде массива из двух 32-битных переменных без знака, а в виде одной 64-битной переменной без знака. В частности, мы меняем код BLAKE следующим образом:
4.4 Grøstl
Теперь мы переходим к другому финалисту SHA-3: Grøstl от Gauravaram et al. [20]. Сообщение разбивается на 512-битные или 1024-битные блоки в зависимости от длины хеш-значения. Насколько нам известно, об ошибках в этой реализации не сообщалось.
В эталонной реализации Grøstl не все циклы находятся внутри Update(), но также и внутри функции Transform(), которая обрабатывает не только один блок, но и любое количество полных блоков. Здесь мы уже заметили первую проблему: все переменные, представляющие длину сообщения, являются 64-битными целыми числами, но функция Transform() объявлена с параметром (заданным пользователем) 32-битного типа u32, что приводит к некорректному неявному приведению .
Поскольку мы применяем наш подход с использованием KLEE, поиск второй ошибки занимает шесть секунд. Ошибка снова связана с использованием неверных типов: переменная index объявлена как int, что является 32-битным типом данных на 64-битных процессорах. Однако для достаточно больших входных сообщений значение индекса переполняется, что приводит к неопределенному поведению в языке программирования C.
В листинге 3 мы предоставляем программу для демонстрации ошибки. При компиляции с использованием gcc программа записывает в память большое количество данных, что почти наверняка приводит к сбою. Становится интереснее, когда мы компилируем эту программу с помощью clang. Неопределенное поведение приводит к тому, что clang выполняет оптимизацию, которая позволяет избежать переполнения буфера, но вместо этого выводит один и тот же хэш для двух сообщений разной длины. Таким образом, реализация нарушает свойство устойчивости к коллизиям (см. раздел 1).
Мы искали реализации, которые могут быть уязвимы из-за этой ошибки, но не обнаружили ни одного проекта или продукта, которые могли бы быть затронуты. По этой причине мы не отправили отчет об уязвимости. Наиболее заметное использование Grøstl, которое мы обнаружили, было частью алгоритма проверки работоспособности начальной версии криптовалюты Monero. Однако использование Grøstl там давно прекращено.
С исправлением двух ошибок типа доказать правильность с помощью KLEE оказалось намного сложнее, чем ожидалось. Мы снова сталкиваемся с проблемой взрыва пути, которую мы решили, жестко закодировав размер блока и переписав цикл, который побайтно копировал данные в буфер. С этими модификациями KLEE завершается через десять секунд с доказательством того, что утверждения недостижимы.
Листинг 3. Из-за неопределенного поведения ошибка Grøstl приводит к ошибке сегментации при компиляции с использованием gcc или коллизии при компиляции с использованием clang (groestl bug.c).
4.5 Keccak
Единственный финалист SHA-3, который мы еще не изучали в этой статье, — это заявка, выигравшая конкурс: Keccak by Bertoni [9]. Keccak дополняет сообщение и разбивает его на блоки, которые затем обрабатываются криптографической перестановкой. Размер блока, также известный как скорость, имеет значение по умолчанию 1024 бита [9]. Сейчас мы сосредоточимся на этом значении по умолчанию, а влияние размера блока обсудим позже.
Об уязвимости сообщил Муха, и ей присвоен код CVE-2022-37454 [31]. Как победитель конкурса SHA-3 эталонный код Keccak довольно широко распространен, и уязвимость затронула различные проекты, такие как Python и PHP. Подробности об уязвимости см. у Муха и Celi [23]. В этой статье мы объясняем, как уязвимость была обнаружена с помощью KLEE.
Прямой подход с использованием KLEE не заканчивается в разумные сроки. Следовательно, может быть полезно исключить бесконечный цикл в реализации Keccak, так как это приведет к тому, что KLEE также войдет в бесконечный цикл.
Для завершения цикла while(i < databitlen) достаточным, но не необходимым условием является то, что i продвигается вперед в каждой итерации цикла. Это легко проверить, введя старую переменную i, которая инициализируется значением i. Когда переменная i изменяется, мы гарантируем, что она отличается от предыдущей итерации цикла:
В конце цикла устанавливаем old i = i. С этим дополнительным кодом для обнаружения бесконечных циклов KLEE требуется менее секунды для вывода ошибки утверждения. Анализируя тестовый вектор, предоставленный KLEE, мы можем подтвердить, что действительно нашли бесконечный цикл. Обратите внимание, что этот дополнительный код используется только для того, чтобы мы могли легко обнаружить бесконечный цикл в KLEE, дополнительный код не требуется для правильной реализации (которая не содержит бесконечный цикл).
Оказывается, есть не только вход, который приводит к бесконечному циклу, но и другой вход, который вызывает запись большого количества данных в память, что приводит к ошибке сегментации. Детали этого переполнения буфера приведены Муха и Celi [23] и выходят за рамки данной статьи.
Ошибка проявляется, когда в буфере уже есть x битов данных, а затем выполняется Update() из 232 - x битов или более. В приведенном ниже коде Кекчака могут возникнуть две проблемы: старшие биты могут быть отброшены из-за неправильного приведения к 32-битному целому числу, а добавление может переполниться:
Мы можем исправить эту ошибку, немного изменив код так, чтобы partialBlock не превышал размера блока. В этом случае для partialBlock достаточно 32-битного целого числа:
Для исправленного кода KLEE требуется всего 39 секунд, чтобы доказать, что утверждения не могут быть нарушены.
Наконец, мы отмечаем, что KLEE, по-видимому, не прекращает работу в разумные сроки для размеров блоков, не кратных двум. Такие размеры блоков были предложены во время конкурса SHA-3 для обеспечения различных уровней безопасности. К сожалению, решатели часто сталкиваются с трудностями при делении на константу, не являющуюся степенью двойки. KLEE имеет флаг -solver-optimize-divides, который пытается оптимизировать такие деления, прежде чем передать их решателю. Однако даже с этим флагом мы не смогли найти способ заставить KLEE завершаться для размеров блоков, не кратных двум.
4.6 XKCP (SHA-3)
Расширенный пакет кода Keccak (XKCP) [8] поддерживается командой Keccak. Он содержит стандартизированный NIST вариант хеш-функции Keccak. Между представлением Keccak в финальном раунде и стандартом SHA-3 отличается только заполнение сообщения.
Реализация SHA-3 в XKCP основана на реализации представления Keccak в финальном раунде. Тем не менее, он претерпел довольно много рефакторинга. По этой причине мы указываем XKCP SHA-3 как отдельную реализацию в таблице 1.
Та же ошибка, которая влияет на отправку Keccak в финальном раунде, присутствует и в XKCP, хотя для ее запуска требуются два вызова Update() с общей длиной 232 байта (4 ГиБ), а не 232 бита (512 МиБ). Более того, у него есть еще одна ошибка (отсутствующая в представлении Keccak), из-за которой сообщения чуть меньше 264 байт приводят к бесконечному циклу. Это связано с переполнением в операции сравнения (dataByteLen >= (i + rateInBytes)), которое в исправленной версии кода заменено на dataByteLen-i >= rateInBytes.
Используя KLEE, требуется менее одной секунды, чтобы предоставить тестовый вектор, который вызывает ошибку, при условии, что мы снова расширим код для обнаружения бесконечных циклов. Для размера блока 1024 бит KLEE требуется 20 секунд, чтобы доказать, что утверждения недостижимы.
4.7 CoreCrypto
Наконец, мы хотели бы вернуться к бесконечному циклу в библиотеке Apple CoreCrypto. Уязвимость затронула 11 из 12 реализованных хеш-функций и получила код CVE-2019-8741 [30]. Подробности об ошибке см. у Mouha и Celi [22].
Подход с использованием KLEE довольно прост в реализации. KLEE находит уязвимый тестовый вектор менее чем за секунду для исходной реализации и может доказать недостижимость утверждений менее чем за три минуты для обновленной реализации.
Здесь мы хотим отметить интересное совпадение. Если мы начнем с исправленной реализации Update() в Apple CoreCrypto с небольшим рефакторингом (например, заменив len на dataByteLen-i, переименовав переменные и функции и удалив ненужный код), мы получим исправленную реализацию Update(), который используется XKCP. Кажется, что Update() достаточно прост, чтобы две команды могли независимо прийти к одной и той же реализации (вплоть до простого рефакторинга), но достаточно сложен, чтобы содержать уязвимости, которые оставались нераскрытыми более десяти лет.
Ограничения и обсуждение
После завершения конкурса SHA-3 в 2012 г. уязвимости были обнаружены в реализациях финалиста SHA-3 BLAKE в 2015 г. [4], в 11 из 12 реализованных хэш-функций библиотеки Apple CoreCrypto в 2019 г. [30], а недавно в эталонной реализации победителя SHA-3 Keccak [31].
Все эти уязвимости были связаны с функцией Update(), которая используется для обработки сообщения блоками. Тем не менее, влияние уязвимостей совершенно различно. В то время как реализация XKCP SHA-3 содержала уязвимость переполнения буфера с возможностью выполнения произвольного кода, влияние уязвимости в библиотеке Apple CoreCrypto ограничивается бесконечным циклом. Уязвимость BLAKE нельзя использовать для запуска какой-либо ошибки времени выполнения, однако ее можно использовать для нарушения свойства устойчивости к коллизиям хеш-функции.
Это позволяет нам сделать первое наблюдение, что подходы к предотвращению проблем с безопасностью памяти (такие как обеспечение соблюдения стандартов кодирования, песочница или переход от C/C++ к более безопасным языкам программирования) были бы полезными, но недостаточными, чтобы избежать уязвимостей, описанных в этом документе. бумага. Мы также достигаем пределов подходов с использованием тестовых векторов: тест больших данных (LDT) может занять довольно много времени для выполнения сообщения размером 4 ГиБ для обнаружения ошибок в библиотеке Apple CoreCrypto, а для ошибки XKCP — один большой вызов. to Update() не активирует уязвимость (поскольку требует, чтобы некоторые данные уже присутствовали в буфере).
Поэтому может быть интересно рассмотреть подходы, использующие символьное выполнение. Подход, который мы описываем в этой статье с использованием KLEE, оказывается довольно простым в развертывании. Мы выполнили (частичную) проверку эквивалентности функции Update(), закомментировав строки, включающие содержимое сообщения и функцию сжатия. В производственной среде средства проверки переопределяют эти функции, а не комментируют их, поэтому проверки могут быть частью процесса непрерывной интеграции, подобного тому, как Amazon Web Services в настоящее время развертывает CBMC [14].
В то время как подходы, использующие большие тестовые векторы, могут занять некоторое время (особенно на медленном оборудовании), символическое выполнение может найти ошибки за несколько секунд или доказать правильность менее чем за 12 минут, как показано в таблице 1. приблизиться к низкозатратному подходу к формальным методам и проверке программ и, возможно, даже к более строгим подходам, используемым в таких проектах, как HACL* [32, 38] или SPARKSkein [13].
Действительно, тестом здесь было бы увидеть, насколько легко наш подход распространяется на другие заявки на конкурс SHA-3. Мы изучили реализации всех пяти финалистов конкурса и обнаружили, что можем либо доказать правильность, либо обнаружить новые ошибки (как в случае с Grøstl, где мы показываем, как неопределенное поведение может нарушить устойчивость к коллизиям реализации хеш-функции). И хотя наш подход предназначен для проверки соответствия двух вызовов Update() одному вызову конкатенации обоих входных данных, он также находит ошибки, которые могут быть вызваны одним вызовом Update(), как показано ошибками в Grøstl и Библиотека Apple CoreCrypto (поскольку они заставляют KLEE входить в бесконечный цикл).
Наконец, хотя наш подход был полезен для обнаружения ошибок, мы еще раз подчеркиваем, что недостаточно утверждать, что реализации правильны. Например, мы не делаем заявлений о потенциальных ошибках в Init(), Final() или Hash(), а также о потенциальных ошибках в закомментированных строках Update(). Мы также не занимаемся ошибками, связанными с использованием API, например обнаруженными Benmocha et al. [6].
Заключение и будущая работа
Мы пересмотрели реализации пяти финалистов конкурса NIST SHA-3. С 2008 по 2012 год они подвергались тщательному публичному рассмотрению. Однако только в 2015 году была обнаружена уязвимость в реализации BLAKE, а совсем недавно — в победившей заявке Kecak с использованием техники, которая впервые описана в этом документе.
Мы показали, как эти ошибки могут быть (повторно) обнаружены всего за несколько секунд, требуя лишь минимальных усилий для создания системы проверки исходного кода. Более того, мы также обнаружили уязвимость в представлении Grøstl, позволяющую создавать два сообщения, которые приводят к одному и тому же значению хеш-функции при компиляции с помощью clang. Наш подход также позволил бы обнаружить ошибку в библиотеке Apple CoreCrypto, о которой сообщалось в 2019 году.
Наш подход требует символьного выполнения, чтобы проверить, эквивалентны ли два вызова Update() (с некоторыми удаленными строками кода) одному вызову Update() при конкатенации обоих входных данных. Для проверки этого свойства мы использовали фреймворк символьного исполнения KLEE.
К сожалению, наш подход основан на пробах и ошибках. В частности, чтобы доказать, что ни одно из утверждений не работает, нам иногда приходилось немного переписывать код, чтобы избежать сбоя KLEE из-за взрыва пути. Это ограничение, поскольку в идеале мы хотели бы вообще не вносить изменений в исходный код, но, возможно, это приемлемый компромисс для достижения цели (частичной) проверки программы.
Интересное направление будущей работы — найти способ расширить наш подход на Keccak и SHA-3, когда размер блока не является степенью двойки.
Переведено специально для xss.pro
Автор перевода: yashechka
Источник: Nicky Mouha Strativia, Largo, MD, USA nicky@mouha.be