Galois работает над повышением удобства SAW, инструмента для верификации программ наCиJava, исходный код кторого открыт. Основным способом взаимодействия пользователей сSAW является его спецификация иязык программирования сценариев. Чтобы сделать SAW как можно более доступным, вкачестве языка программирования SAW теперь можно использовать Python! Для демонстрации этой новой возможности в Galoisсоздали пример, выполнив проверку части реализации протокола Signal наязыкеС.В частности, как спецификация SAW определяются условия, при которых сообщение протокола Signal будет успешно аутентифицировано. К старту курса о Fullstack-разработке на Python мы перевели материал об этом примере.
SAW-клиент Python
Управление SAW может осуществляться средствами Python через библиотеку saw-client вPyPI. Реализация спомощью Python непредставляет сложности управление SAW осуществляется через JSON-RPC API, как показано впредыдущей статье. Библиотека saw-client постоянно развивалась, итеперь вней реализован высокоуровневый интерфейс, отвечающий зареализацию функций RPC.
Помимо Python, вSAW также используется альтернативный язык программирования сценариев, называемый SAWScript. Хотя наSAWScript возможно писать теже проверки, что иPython, этотязыкнелишён недостатков. SAWScript специализированный язык, поэтому ондовольно сложен для понимания теми, кто впервые берётся заизучениеSAW. Кроме того, вSAWScript практически отсутствует возможность подключения внешних библиотек. Если вызахотите написать наSAWScript то, чего нет встандартной библиотеке, вам придётся реализовать нужную функцию самостоятельно.
Сдругой стороны, Python широко используемый язык, изначально хорошо знакомый гораздо большему числу людей. УPython также имеется богатый набор библиотек ивспомогательных программ, доступных вкаталоге PyPI. Даже если Python невходит вчисло ваших любимых языков программирования, мывсё равно советуем попробовать saw-client. Если под рукой неокажется ничего другого, код, написанный вsaw-client, может послужить источником вдохновения для реализации аналогичного клиента надругом языке.
Базовая спецификация вsaw-client
Давайте рассмотрим, как saw-client можно использовать для создания спецификаций реального кода наязыкеC. Для примера возьмём libsignal-protocol-c. Эта библиотека представляет собой реализованный наязыке Cпротокол Signal, криптографический протокол, используемый для шифрования мгновенных сообщений, голосовых ивидеозвонков. Этот протокол применяется вприложении Signal Messenger, получившем название попротоколу, нотакже поддерживается вдругих приложениях, таких как WhatsApp, Facebook Messenger иSkype.
Общее описание возможностей SAW сиспользованием библиотеки libsignal-protocol-c приведено вразделе "Планы".
Для начала рассмотрим базовую структуру данных, используемую библиотекой libsignal-protocol-c, аименно signal_buffer:
struct signal_buffer { size_t len; uint8_t data[];};
signal_buffer представляет собой байтовый массив (массив данных) сдлинойlen. При отправке сообщения спомощью libsignal-protocol-c основным компонентом сообщения является signal_buffer.
Чтобы быть уверенным, что libsignal-protocol-c работает так, как заявлено, нужно убедиться, что содержимое signal_buffer сообщения соответствует ожидаемому. Библиотека проверяет соответствие двух буферов signal_buffer спомощью функции signal_constant_memcmp:
int signal_constant_memcmp(const void *s1, const void *s2, size_t n){ size_t i; const unsigned char *c1 = (const unsigned char *) s1; const unsigned char *c2 = (const unsigned char *) s2; unsigned char result = 0; for (i = 0; i < n; i++) { result |= c1[i] ^ c2[i]; } return result;}
Интуитивно понятно, что утилита signal_constant_memcmp должна проверить, одинаковоли содержимое двух байтовых массивов signal_buffer. Если они одинаковы, функция вернёт значение0. Если содержимое несовпадает, возвращается значение, указывающее набайты, вкоторых массивы отличаются.
При этом напервый взгляд может быть неочевидно, что при одинаковых массивах функция вернёт значение0. Учитывая, что манипуляций сбитами происходит довольно много, вполне возможно, что кто-то мог допустить ошибку при написании кода, манипулирующего битами. Правильность такого кода можно проверить, сверив его соспецификацией, созданной спомощью saw-client. Такая спецификация может выглядеть примерно так:
from saw_client.llvm import *class ConstantMemcmpEqualSpec(Contract): def specification(self) -> None: _1 self.execute_func(_2) _3
Класс Contract определяет спецификации SAW сиспользованием метода specification. Чтобы создать собственную спецификацию, достаточно создать подкласс Contract ипереопределить метод specification. Каждая спецификация состоит изтрёх частей:
-
Предварительные условия (_1), определяющие допущения, которые необходимо сделать перед вызовом верифицируемой функции.
-
Аргументы для передачи впроверяемую функцию (_2).
-
Постусловия (_3), определяющие характер проверки после вызова верифицируемой функции.
Учитывая требования кспецификации, проверим, как утилита signal_constant_memcmp работает в пределах спецификации SAW:
class ConstantMemcmpEqualSpec(Contract): n: int def __init__(self, n: int): super().__init__() self.n = n def specification(self) -> None: s1 = self.fresh_var(array_ty(self.n, i8), "s1") s1p = self.alloc(array_ty(self.n, i8), points_to = s1) s2 = self.fresh_var(array_ty(self.n, i8), "s2") s2p = self.alloc(array_ty(self.n, i8), points_to = s2) self.precondition(cryptol(f"{s1.name()} == {s2.name()}")) self.execute_func(s1p, s2p, cryptol(f"{self.n} : [64]")) self.returns(cryptol("0 : [32]"))
Предварительными условиями являются наличие двух байтовых массивов (s1p иs2p), содержимое которых s1 иs2одинаково. Вчастности, одинаковость содержимого гарантирует вызов self.precondition(...). Аргумент self.precondition(...) записывается наCryptol, предметно-ориентированном языке программирования (DSL), используемом вкриптографии. Приведённое выражение наCryptol довольно простое, так как выполняет только проверку равенства, нониже мыувидим более сложные примеры наCryptol.
Аргументами функции являются два байтовых массива суказанием ихдлин (self.n), преобразуемых вначале ввыражение Cryptol, чтобы SAW мог получить оних представление. Порстусловие, снова ввиде выражения наCryptol, заключается втом, что функция возвращает значение 0.
После проведения всей подготовительной работы проверяем, что signal_constant_memcmp соответствует созданной нами спецификации:
mod = llvm_load_module("libsignal-protocol-c.bc") # An LLVM bitcode filearray_len = 42 # Pick whichever length you want to checkllvm_verify(mod, "signal_constant_memcmp", ConstantMemcmpEqualSpec(array_len))
Если проверка пройдёт нормально, можно запустить этот код наPython иувидеть следующий результат:
Verified: lemma_ConstantMemcmpEqualSpec (defined at signal_protocol.py:122)
Ура! Инструмент SAW проверил правильность работы утилиты signal_constant_memcmp. Важно отметить, что нам ненужно было даже упоминать обитовых манипуляциях внутри функции SAW выполнил ихавтоматически. Отметим, однако, что команда ConstantMemcmpEqualSpec определяет происходящее только втом случае, если байтовые массивы равны друг другу. Еслибы мыхотели охарактеризовать происходящее вслучае неравенства байтовых массивов, потребоваласьбы несколько более сложная спецификация.
Также следует отметить, что вприведённом выше коде встречаются повторения, так как мыдважды вызываем функцию self.fresh_var(), азатем self.alloc(). Ксчастью, Python избавляет оттаких проблем:
def ptr_to_fresh(spec: Contract, ty: LLVMType, name: str) -> Tuple[FreshVar, SetupVal]: var = spec.fresh_var(ty, name) ptr = spec.alloc(ty, points_to = var) return (var, ptr)class ConstantMemcmpEqualSpec(Contract): ... def specification(self) -> None: (s1, s1p) = ptr_to_fresh(self, array_ty(self.n, i8), "s1") (s2, s2p) = ptr_to_fresh(self, array_ty(self.n, i8), "s2") ...
Верификация кода сиспользованием HMAC
Отбиблиотеки libsignal-protocol-c требуется гораздо больше, чем просто хранить сообщения она также должна отправлять иполучатьих. Кроме того, шифровать сообщения необходимо так, чтобы ихмог прочитать только предполагаемый получатель, чтобы частную переписку немогли перехватить третьи лица.
Одним изосновных этапов шифрования сообщения является присоединение кода аутентификации сообщения (MAC), который можно использовать для проверки того, что после отправки сообщения его содержимое неменялось. Вчастности, libsignal-protocol-c использует HMAC, тип MAC, вычисляемый спомощью криптографической хеш-функции.
Подробное описание работы HMAC тема для отдельной статьи. Но, ксчастью, для создания спецификации SAW, связанной сHMAC, ненужно вдаваться вдетали. Вместо этого можно использовать неинтерпретируемые функции. Для начала создадим ряд функций Cryptol, определяющих характер работы HMAC:
hmac_init : {n} [n][8] -> HMACContexthmac_init = undefinedhmac_update : {n} [n][8] -> HMACContext -> HMACContexthmac_update = undefinedhmac_final : HMACContext -> [SIGNAL_MESSAGE_MAC_LENGTH][8]hmac_final = undefined
Это будут неинтерпретируемые функции, используемые для создания кода, связанного сHMAC, вбиблиотеке libsignal-protocol-c. Основная идея заключается втом, что, получив навходе криптографический ключ, hmac_init создаст HMACContext. HMACContext будет многократно обновляться через hmac_update, используя данные первого аргумента. Затем hmac_final преобразует HMACContext вsignal_buffer достаточной длины для хранения MAC.
Определение HMACContext зависит оттого, какая криптографическая хэш-функция используется всочетании сHMAC. Параметры библиотеки libsignal-protocol-c настроены для используемых еюхеш-функций, поэтому можно свободно подключать библиотеки OpenSSL, Common Crypto или другую подходящую библиотеку.
Поскольку эти функции считаются неинтерпретируемыми, SAW небудет ихоценивать вовремя верификации. Другими словами, то, как реализованы эти функции, неимеет значения; undefined выбрано для удобства, ноподойдёт илюбая другая реализация.
После определения этих функций можно связать ихссоответствующими функциями Cвсамой библиотеке. Например, вот сокращённая спецификация для функции signal_hmac_sha256_initC:
class SignalHmacSha256InitSpec(Contract): key_len: int def specification(self) -> None: hmac_context_ptr = self.alloc(...) (key_data, key) = ptr_to_fresh(self, array_ty(self.key_len, i8), "key_data") self.execute_func(..., hmac_context_ptr, key, cryptol(f"{self.key_len} : [64]")) init = f"hmac_init`{{ {self.key_len} }} {key_data.name()}" dummy_hmac_context = self.alloc(..., points_to = cryptol(init)) self.points_to(hmac_context_ptr, dummy_hmac_context) self.returns(cryptol("0 : [32]"))key_len = 32init_spec = llvm_assume(mod, "signal_hmac_sha256_init", SignalHmacSha256InitSpec(key_len))
Нестарайтесь понять каждую строчку кода. Просто знайте, что самой важной его частью является последняя строка, вкоторой вместо llvm_verify используется llvm_assume. Функция llvm_assume позволяет SAW использовать спецификацию, фактически немоделируя её посути SAW трактует еёкак аксиому. Это позволяет привязать поведение signal_hmac_sha256_init кнеинтерпретируемой функции hmac_init впостусловиях спецификации.
Аналогичным образом llvm_assume также можно использовать для создания спецификаций, включающих hmac_update иhmac_final. После этого можно проверить очень важную функцию, связанную сMAC: signal_message_verify_mac. Фактически данная функция принимает сообщение вкачестве аргумента, вычисляет MAC для данных внутри сообщения ипроверяет, совпадаетли онсMAC вконце сообщения. Если значения совпадают, можно суверенностью утверждать, что при отправке получателю сообщение неменялось.
Объяснение всех тонкостей работы signal_message_verify_mac занялобы довольно много времени, поэтому вэтой заметке мыкоснёмся лишь главного вопроса: как должно выглядеть содержимое сообщения? Данные внутри сообщения могут быть произвольными, однако MAC вконце должен иметь вполне определённую форму. Эту форму можно определить спомощью функции Python:
def mk_hmac(serialized_len: int, serialized_data: FreshVar, receiver_identity_key_data : FreshVar, sender_identity_key_data: FreshVar, mac_key_len: int, mac_key_data: FreshVar) -> SetupVal: sender_identity_buf = f""" [{DJB_TYPE}] # {sender_identity_key_data.name()} : [{DJB_KEY_LEN} + 1][8] """ receiver_identity_buf = f""" [{DJB_TYPE}] # {receiver_identity_key_data.name()} : [{DJB_KEY_LEN} + 1][8] """ hmac = f""" hmac_final (hmac_update`{{ {serialized_len} }} {serialized_data.name()} (hmac_update`{{ {DJB_KEY_LEN}+1 }} ({receiver_identity_buf}) (hmac_update`{{ {DJB_KEY_LEN}+1 }} ({sender_identity_buf}) (hmac_init`{{ {mac_key_len} }} {mac_key_data.name()})))) """ return cryptol(hmac)
Довольно сложно, неправдали? Ноещё раз нестарайтесь понять каждую строчку кода. Тут важно понять, что сначала вызывается hmac_init, затем выполняются несколько вызовов hmac_update, после чего осуществляется вызов hmac_finalcall. Это весьма близко интуитивным допущениям, сделанным ранее для HMAC, поэтому, если SAW убедится втом, что MAC выглядит как данное выражение Cryptol, можно быть уверенным, что онработает так, как ожидалось.
Далее нам нужно использовать это вспецификации. Вот выдержка изспецификации для signal_message_verify_mac, вкоторой впредусловиях описывается, как должно выглядеть валидное сообщение:
lass SignalMessageVerifyMacSpec(Contract): serialized_len: int def specification(self) -> None: ... mac_index = 8 + self.serialized_len - SIGNAL_MESSAGE_MAC_LENGTH ser_len = f"{self.serialized_len} : [64]" self.points_to(serialized[0], cryptol(ser_len)) self.points_to(serialized[8], serialized_message_data) self.points_to(serialized[mac_index], mk_hmac(...)) self.execute_func(...) self.returns(cryptol("1 : [32]"))
Здесь serialized указывает наsignal_buffer для всего сообщения. Для описания памяти, содержащейся вразличных частях буфера, можно использовать нотацию слайса Python (например, serialized[0]). Первая часть содержит self.serialized_len, общую длину сообщения. Через восемь байтразмещается serialized_message_data данные сообщения. Всамом конце буфера содержится MAC, вычисленный спомощью mk_hmac(...).
Проверяем всё напрактике вызываем llvm_verify согласно этой спецификации. Вэтот раз нужно передать несколько дополнительных аргументов. Нужно явно указать, какие допущения мысделали ранее спомощью llvm_assume посредством аргумента lemmas. Также нужно указать инструменту решения SMT, какие функции должны рассматриваться как неинтерпретируемые. Это делается спомощью аргумента script:
uninterps = ["hmac_init", "hmac_update", "hmac_final"]llvm_verify(mod, "signal_message_verify_mac", SignalMessageVerifyMacSpec(...), lemmas=[init_spec, update_spec1, update_spec2, final_spec], script=ProofScript([z3(uninterps)]))
В результате мы видим долгожданную зелёную галочку:
Планы
Спомощью saw-client мысмогли получить ряд интересных данных окоде вlibsignal-protocol-c. Мысмогли продемонстрировать, что signal_message_verify_mac, функция, проверяющая целостность сообщения, отправленного попротоколу Signal, работает правильно, если последняя часть сообщения содержит верный код аутентификации сообщения (MAC). Кроме того, мыопределили, каким должно быть содержимое MAC относительно абстрактной спецификации криптографических хэш-функций.
Однако спомощью инструмента saw-client можно сделать гораздо больше, чем рассказано вданной заметке. Мыпроверяли ключевое свойство кода, проверяющего целостность сообщений. Нотакая проверка целостности некасалась сообщений, передаваемых попроводам. Мытакже нестали полностью определять поведение HMAC, хотя это можно былобы сделать; смотрите здесь.
Несмотря нато что saw-client может использоваться как самостоятельный инструмент верификации, внекоторых аспектах saw-client недостигает функциональности SAWScript. saw-client внастоящее время неподдерживает ряд функций SAW, например функцию инициализации глобальных переменных вспецификациях. Кроме того, некоторые идиомы SAWScript реализованы вsaw-client нетак "красиво", пример квазикавычки ввыражениях Cryptol. Мысчитаем, что современем нам удастся решить эти проблемы.
Вперспективе мыпопытаемся сделать Python полноправным языком написания кода для SAW, иданная работа первый шаг вэтом направлении. Весь код, представленный вэтой заметке, можно найти здесь. Рекомендуем испытать вработе инструмент saw-client. Любые ваши пожелания икомментарии отправляйте в трекер проблем ивопросов SAW.
А если вам инетересен не только анализ программ с помощью Python, но и активная разработка на этом языке в направлениях как бекенда, так и фронтенда, то вы можете обратить внимание на наш курс "Fullstack-разработчик на Python", где также рассматривается тестирование ПО и многие другие аспекты профессии программиста.
Узнайте, как прокачаться и в других специальностях или освоить их с нуля:
Другие профессии и курсыПРОФЕССИИ
КУРС
