Автоматическая генерация вредоносных пакетов: как байт-код взламывает сеть

Вредоносное ПО для Linux часто скрывается в программах для сокетов Berkeley Packet Filter (BPF) — небольших исполняемых фрагментах кода, которые можно встроить в ядро Linux для настройки обработки сетевого трафика. Некоторые из наиболее устойчивых угроз в Интернете используют эти фильтры, чтобы оставаться в спящем режиме до получения специального "волшебного" пакета. Поскольку эти фильтры могут состоять из сотен инструкций и включать сложные логические переходы, их обратная разработка вручную — это медленный процесс, создающий узкое место для исследователей безопасности.

В поисках лучшего решения мы обратили внимание на символьное выполнение (symbolic execution) — метод, который рассматривает код как серию ограничений, а не просто инструкций. Используя доказыватель теорем Z3, мы можем двигаться в обратном направлении от вредоносного фильтра, чтобы автоматически сгенерировать пакет, необходимый для его активации. В этой статье мы объясняем, как создали инструмент для автоматизации этого процесса, превращая часы ручного анализа ассемблера в задачу, которая занимает всего несколько секунд.

Прежде чем мы рассмотрим, как деконструировать вредоносные фильтры, нужно понять механизм, который их выполняет. Berkeley Packet Filter (BPF) — это высокоэффективная технология, позволяющая ядру извлекать определённые пакеты из сетевого стека на основе набора инструкций в байт-коде.

Хотя многие современные разработчики знакомы с eBPF (Extended BPF), мощной эволюцией технологии, используемой для наблюдения и безопасности, эта статья фокусируется на "классическом" BPF. Изначально созданный для таких инструментов, как tcpdump, классический BPF использует простую виртуальную машину всего с двумя регистрами для высокоскоростной оценки сетевого трафика. Поскольку он работает глубоко внутри ядра и может "скрывать" трафик от инструментов пользовательского пространства, он стал любимым инструментом авторов вредоносного ПО, стремящихся создать скрытые бэкдоры.

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

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

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

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

BPFDoor — это сложный пассивный бэкдор для Linux, в основном используемый кибершпионами из китайских угрозовых группировок, включая Red Menshen (также известную как Earth Bluecrow). Активный как минимум с 2021 года, этот вредоносный код предназначен для сохранения скрытого доступа в скомпрометированных сетях, нацеливаясь на телекоммуникации, образование и государственный сектор, с особым вниманием к операциям в Азии и на Ближнем Востоке.

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

Давайте сосредоточимся на образце, который был опубликован в исследовании компании Fortinet (82ed617816453eba2d755642e3efebfcbd19705ac626f6bc8ed238f4fc111bb0). Если мы дизассемблируем инструкции BPF и добавим аннотации, можно записать следующее:

(000) ldh [0xc]                   ; Читаем полуслово по смещению 12 (EtherType)
(001) jeq #0x86dd, jt 2, jf 6     ; 0x86DD (IPv6) -> инструкция 002, иначе 006
(002) ldb [0x14]                  ; Читаем байт по смещению 20 (Протокол)
(003) jeq #0x11, jt 4, jf 15      ; 0x11 (UDP) -> инструкция 004, иначе DROP
(004) ldh [0x38]                  ; Читаем полуслово по смещению 56 (Порт назначения)
(005) jeq #0x35, jt 14, jf 15     ; 0x35 (DNS) -> ACCEPT, иначе DROP
(006) jeq #0x800, jt 7, jf 15     ; 0x800 (IPv4) -> инструкция 007, иначе DROP
(007) ldb [23]                    ; Читаем байт по смещению 23 (Протокол)
(008) jeq #0x11, jt 9, jf 15      ; 0x11 (UDP) -> инструкция 009, иначе DROP
(009) ldh [20]                    ; Читаем полуслово по смещению 20 (фрагмент)
(010) jset #0x1fff, jt 15, jf 11  ; фрагментирован -> DROP, иначе инструкция 011
(011) ldxb 4*([14]&0xf)           ; Загружаем индекс (регистр x): ihl & 0xf
(012) ldh [x + 16]                ; Читаем полуслово по смещению x+16 (Порт назначения)
(013) jeq #0x35, jt 14, jf 15     ; 0x35 (DNS) -> ACCEPT, иначе DROP
(014) ret #0x40000 (ACCEPT)
(015) ret #0 (DROP)

В приведённом выше примере мы можем установить, что есть два пути, ведущих к результату ACCEPT (шаги 5 и 13). Мы также можем чётко наблюдать проверку определённых байтов, включая их смещения и значения.

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

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

Начнём с создания небольшой очереди. Эта очередь содержит несколько важных данных:

• Указатель на следующую инструкцию.

• Наш текущий путь выполненных инструкций + следующая инструкция.

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

paths = []
queue = dequeue([(0, [0])])

while queue:
	pc, path = queue.popleft()

	if pc >= len(instructions):
            continue

instruction = instructions[pc]
	
	if instruction.class == return_instruction:
		if instruction_constant != 0:  # accept
			paths.append(path)
		continue  # drop или accept, остановить разбор этой инструкции

if instruction.class == jump_instruction:
	if instruction.operation == unconditional_jump:
		next_pc = pc + 1 + instruction_constant
		queue.append((next_pc, path + [next_pc]))
		continue

	# Условный переход, исследуем обе ветки
	pc_true = pc + 1 + instruction.jump_true
	pc_false = pc + 1 + instruction.jump_false
	
	if instruction.jump_true <= instruction.jump_false:
		queue.append((pc_true, path + [pc_true]))
		queue.append((pc_false, path + [pc_false]))
	# иначе: то же самое, но в обратном порядке добавления
# иначе: последовательная инструкция, добавить в очередь

Если мы выполним эту логику на нашем предыдущем примере BPFDoor, мы получим кратчайший путь к принятому пакету:

(000) code=0x28 jt=0 jf=0  k=0xc     ; Читаем полуслово по смещению 12 (EtherType)
(001) code=0x15 jt=0 jf=4  k=0x86dd  ; Пакет IPv6
(002) code=0x30 jt=0 jf=0  k=0x14    ; Читаем байт по смещению 20 (Протокол)
(003) code=0x15 jt=0 jf=11 k=0x11    ; Номер протокола 17 (UDP)
(004) code=0x28 jt=0 jf=0  k=0x38    ; Читаем слово по смещению 56 (Порт назначения)
(005) code=0x15 jt=8 jf=9  k=0x35    ; Порт назначения 53
(014) code=0x06 jt=0 jf=0  k=0x40000 ; Принять (Accept)

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

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

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

Другой инструмент, который мы будем использовать для создания наших валидных "волшебных" пакетов, — это scapy, популярная библиотека Python для интерактивного манипулирования пакетами.

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

Распространённая техника для исследования путей, проходимых в данной программе, называется символьным выполнением (symbolic execution). Для этой техники мы предоставляем входные данные, которые можно использовать как переменные, включая ограничения. Зная результат успешного пути, мы можем настроить наш инструмент на поиск всех таких успешных путей и отображение конечного результата в контекстуализированном формате.

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

class BPFPacketCrafter:
    MIN_PKT_SIZE = 64           # Минимальный размер пакета (заголовки Ethernet + IP + UDP)
    LINK_ETHERNET = "ethernet"  # DLT_EN10MB - начинается с заголовка Ethernet
    LINK_RAW = "raw"            # DLT_RAW - начинается непосредственно с IP-заголовка
    MEM_SLOTS = 16              # Количество ячеек временной памяти (M[0] до M[15])

    def __init__(self, ins: list[BPFInsn], pkt_size: int = 128, ltype: str = "ethernet"):
        self.instructions = ins
        self.pkt_size = max(self.MIN_PKT_SIZE, pkt_size)
        self.ltype = ltype

        # Символьные байты пакета
        self.packet = [BitVec(f"pkt_{i}", 8) for i in range(self.pkt_size)]

        # Символьные регистры (32-битные)
        self.A = BitVecVal(0, 32)  # Аккумулятор
        self.X = BitVecVal(0, 32)  # Индексный регистр

        # Временная память M[0-15] (32-битные слова)
        self.M = [BitVecVal(0, 32) for _ in range(self.MEM_SLOTS)]

В приведенном выше коде мы описали основу машины для сохранения состояния во время символьного выполнения. Конечно, есть и другие условия, за которыми нужно следить, но они обрабатываются в процессе решения. Для обработки инструкции ADD машина сопоставляет операцию BPF с операцией сложения в Z3:

def _execute_ins(self, insn: BPFInsn):
    cls = insn.cls
    if cls == BPFClass.ALU:
        op = insn.op
        src_val = BitVecVal(insn.k, 32) if insn.src == BPFSrc.K else self.X
        if op == BPFOp.ADD:
            self.A = self.A + src_val

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

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

• Инициализировать регистры "x" (индексный) и "a" (аккумулятор) их базовым состоянием.

• Выполнить цикл по инструкциям из пути, который был идентифицирован как успешный;

  • Выполнять не-переходные инструкции как есть, отслеживая состояния регистров.

  • Определить, встретилась ли инструкция перехода, и проверить, следует ли выполнять ветвление.

• Использовать функцию check() Z3 для проверки, удовлетворено ли наше условие при заданном ограничении (ACCEPT).

• Преобразовать массивы битовых векторов Z3 в байты.

• Использовать scapy для создания пакетов из преобразованных байтов.

Если мы посмотрим на ограничения, построенные решателем Z3, мы сможем отследить шаги выполнения, предпринятые Z3 для построения байтов пакета:

[If(Concat(pkt_12, pkt_13) == 0x800,
    pkt_14 & 0xF0 == 0x40,
    True),
 If(Concat(pkt_12, pkt_13) == 0x800, pkt_14 & 0x0F >= 5, True),
 If(Concat(pkt_12, pkt_13) == 0x800, pkt_14 & 0x0F == 5, True),
 If(Concat(pkt_12, pkt_13) == 0x86DD,
    pkt_14 & 0xF0 == 0x60,
    True),
 0x86DD == ZeroExt(16, Concat(pkt_12, pkt_13)),
 0x11 == ZeroExt(24, pkt_20),
 0x35 == ZeroExt(16, Concat(pkt_56, pkt_57))]

Первая часть отображаемых ограничений Z3 — это ограничения, добавленные для обеспечения построения корректного ethernet IP-пакета при работе с инструкциями BPF канального уровня. Операторы "If" применяют специфические ограничения в зависимости от обнаруженного протокола:

• Логика для IPv4 (0x0800):

  • pkt_14 & 240 == 64: Байт 14 — начало IP-заголовка. Маска 0xF0 выделяет старшую тетраду (поле Версия), чтобы проверить, равна ли версия 4 (0x40).

  • pkt_14 & 15 == 5: Маска 15 (0x0F) выделяет младшую тетраду (IHL — длина заголовка IP). Это предписывает длину заголовка равной 5 (20 байт), что является стандартным размером без опций.

• Логика для IPv6 (0x86dd):

  • pkt_14 & 240 == 0x60: Проверяет, равно ли поле версии 6 (0x60).

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

• 0x86DD: Условие для пакета с заголовком IPv6.

• 0x11: Номер протокола UDP.

• 0x35: Порт назначения (53).

Помимо ожидаемых значений, мы видим смещение байта, где они должны находиться в данном пакете (например, pkt_12, pkt_13).

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

###[ Ethernet ]###
  dst       = 00:00:00:00:00:00
  src       = 00:00:00:00:00:00
  type      = IPv6                 <-- Пакет IPv6
###[ IPv6 ]###
     version   = 6
     tc        = 0
     fl        = 0
     plen      = 0
     nh        = UDP               <-- Протокол UDP
     hlim      = 0
     src       = ::
     dst       = ::
###[ UDP ]###
        sport     = 0
        dport     = domain         <-- Порт 53
        len       = 0
        chksum    = 0x0

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

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

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