Как использовать Python для проверки протокола Signal

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 file
array_len = 42 # Pick whichever length you want to check
llvm_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] -> HMACContext
hmac_init = undefined

hmac_update : {n} [n][8] -> HMACContext -> HMACContext
hmac_update = undefined

hmac_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 = 32
init_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", где также рассматривается тестирование ПО и многие другие аспекты профессии программиста.

Узнайте, как прокачаться и в других специальностях или освоить их с нуля:

• Профессия Data Scientist

• Профессия Data Analyst

• Курс по Data Engineering