Linux 맬웨어는 종종 Linux 커널에 임베드하여 네트워크 트래픽 처리 방법을 사용자 지정할 수 있는 작은 실행 로직 비트인 버클리 패킷 필터(BPF) 소켓 프로그램에 숨어 있습니다. 인터넷에 가장 지속적으로 존재하는 위협 중 일부는 이러한 필터를 이용해 특정 "마법의" 패킷을 수신할 때까지 휴면 상태를 유지합니다. 이러한 필터는 길이가 수백 개에 달할 수 있고 복잡한 논리적 점프를 포함할 수 있으므로, 수작업으로 리버스 엔지니어링하려면 느린 프로세스이며 이로 인해 보안 연구자에게는 병목 현상이 발생합니다.
더 나은 방법을 찾기 위해 저희는 코드를 단순한 명령이 아닌 일련의 제약 조건으로 처리하는 방법인 기호 실행을 살펴보았습니다. Z3 정리 증명을 이용하면 악의적 필터의 역순으로 작업하여 이를 트리거하는 데 필요한 패킷을 자동으로 생성할 수 있습니다. 이번 게시물에서는 이를 자동화하는 도구를 구축하여, 몇 시간에 걸친 수동 조립 분석 작업을 단 몇 초 만에 끝낼 수 있는 작업을 소개합니다.
악성 필터를 분석하는 방법을 알아보기 전에 해당 필터를 실행하는 엔진을 이해해야 합니다. 버클리 패킷 필터(BPF)는 커널이 바이트코드 명령 세트를 기반으로 네트워크 스택에서 특정 패킷을 가져올 수 있는 매우 효율적인 기술입니다.
많은 최신 개발자가 관찰 가능성 및 보안을 위해 사용되는 강력한 기술인 eBPF (Extended BPF)에 익숙하지만, 이 게시물에서는 "기존" BPF에 초점을 맞춥니다. 원래 tcpdump와 같은 도구를 위해 설계된 클래식 BPF는 단 두 개의 레지스트리가 있는 단순한 가상 머신을 사용하여 네트워크 트래픽을 고속으로 평가합니다. 커널 내 깊숙이에서 실행되고 사용자 공간 도구로부터 트래픽을 "숨길 수 있으므로" 은밀한 백도어를 구축하려는 맬웨어 작성자가 선호하는 도구가 되었습니다.
LLM 을 사용하여 BPF 명령의 컨텍스트 기반 표현을 생성하면 이미 분석가의 수동 오버헤드가 줄어들고 있으며, LLM을 통해 제공되는 컨텍스트가 추가되더라도 검증 조건에 해당하는 네트워크 패킷을 생성하는 것은 여전히 많은 작업이 될 수 있습니다.
BPF 프로그램이 20개 이하의 명령어만 있는 경우에는 대부분 이것이 문제가 되지 않지만, 일부 샘플에서 관찰된 바와 같이 BPF 프로그램이 100개 이상의 명령어로 구성되면 이것이 기하급수적으로 더 복잡해지고 시간이 많이 소요될 수 있습니다.
문제를 분석해 보면 결과에 따라 실행 경로를 계속 진행하거나, 실행을 중지하고 최종 결과를 확인하는 결과를 볼 수 있습니다.
이런 종류의 문제는 결정론적 결과를 가져옵니다. Z3는 주어진 제약 조건에서 문제를 해결할 방법을 갖춘 정리 증명인 Z3로 해결할 수 있습니다.
BPFDoor는 정교하고 패시브한 Linux 백도어로서, Red Menshen(Earth Bluecrow라고도 함)을 비롯한 중국 기반의 위협 행위자들이 사이버 스파이 활동을 하는 데 주로 사용됩니다. 이 맬웨어는 최소 2021년부터 활동해 왔으며, 통신, 교육, 정부 부문을 대상으로 손상된 네트워크에 은밀한 발판을 유지하도록 설계되었으며 아시아와 중동에서의 사업을 중심으로 합니다.
BPFDoor는 BPF를 사용하여 특정 네트워크 포트를 열지 않고도 모든 들어오는 트래픽을 모니터링합니다.
Fortinet 의 연구에서 공유된 샘플에 주목해 보겠습니다(82ed617816453eba2d755642e3efebfcbd19705ac626f6bc8ed238f4fc111bb0). BPF 명령어를 분석하고 몇 가지 주석을 추가하면 다음과 같이 작성할 수 있습니다.
(000) ldh [0xc] ; Read halfword at offset 12 (EtherType)
(001) jeq #0x86dd, jt 2, jf 6 ; 0x86DD (IPv6) -> ins 002 else ins 006
(002) ldb [0x14] ; Read byte at offset 20 (Protocol)
(003) jeq #0x11, jt 4, jf 15 ; 0x11 (UDP) -> ins 004 else DROP
(004) ldh [0x38] ; Read halfword at offset 56 (Dst Port)
(005) jeq #0x35, jt 14, jf 15 ; 0x35 (DNS) -> ACCEPT else DROP
(006) jeq #0x800, jt 7, jf 15 ; 0x800 (IPv4) -> ins 007 else DROP
(007) ldb [23] ; Read byte at offset 23 (Protocol)
(008) jeq #0x11, jt 9, jf 15 ; 0x11 (UDP) -> ins 009 else DROP
(009) ldh [20] ; Read halfword at offset 20 (fragment)
(010) jset #0x1fff, jt 15, jf 11 ; fragmented -> DROP else ins 011
(011) ldxb 4*([14]&0xf) ; Load index (x) register ihl & 0xf
(012) ldh [x + 16] ; Read halfword at offset x+16 (Dst Port)
(013) jeq #0x35, jt 14, jf 15 ; 0x35 (DNS) -> ACCEPT else DROP
(014) ret #0x40000 (ACCEPT)
(015) ret #0 (DROP)
위의 예에서는 ACCEPT 결과로 이어지는 두 가지 경로(5단계와 13단계)가 있음을 확인할 수 있습니다. 또한 오프셋과 값을 포함하여 특정 바이트를 검사하는 것을 명확하게 관찰할 수 있습니다.
이러한 유효성 검사를 수행하고 ACCEPT 경로와 일치하는 모든 것을 추적하면 자동으로 패킷을 만들 수 있습니다.
BPF 명령어에 제시된 조건을 검증하는 패킷의 최단 경로를 찾으려면 바람직하지 않은 조건으로 끝나지 않는 경로를 추적해야 합니다.
작은 대기열을 만드는 것으로 시작합니다. 이 대기열에는 몇 가지 중요한 데이터 포인트가 있습니다.
다음 명령어에 대한 포인터입니다.
실행된 명령어의 현재 경로 + 다음 명령어.
조건을 확인하는 명령어를 만날 때마다 부울 값을 사용하여 결과를 추적하고 이를 대기열에 저장하므로 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 or accept, stop parsing this instruction
if instruction.class == jump_instruction:
if instruction.operation == unconditional_jump:
next_pc = pc + 1 + instruction_constant
queue.append((next_pc, path + [next_pc]))
continue
# Conditional jump, explore both
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]))
# else: same as above but reverse order of appending
# else: sequential instruction, append to the queue
이전의 BPDoor 예시에 대해 이 로직을 실행하면 허용된 패킷의 최단 경로가 표시됩니다.
(000) code=0x28 jt=0 jf=0 k=0xc ; Read halfword at offset 12 (EtherType)
(001) code=0x15 jt=0 jf=4 k=0x86dd ; IPv6 packet
(002) code=0x30 jt=0 jf=0 k=0x14 ; Read byte at offset 20 (Protocol)
(003) code=0x15 jt=0 jf=11 k=0x11 ; Protocol number 17 (UDP)
(004) code=0x28 jt=0 jf=0 k=0x38 ; Read word at offset 56 (Destination Port)
(005) code=0x15 jt=8 jf=9 k=0x35 ; Destination port 53
(014) code=0x06 jt=0 jf=0 k=0x40000 ; Accept
이는 이미 BPF 명령을 분석하고 백도어에 허용된 패킷이 어떻게 표시되는지 파악할 때 BPF 제약을 자동으로 해결하는 데 유용한 자동화입니다. 하지만 여기서 한 걸음 더 나아갈 수 있다면 어떨까요?
예상된 패킷을 자동화된 방식으로 다시 제공하는 작은 도구를 만들 수 있다면 어떨까요?
일련의 제약 조건이 주어질 때 문제를 해결하는 데 완벽한 도구 중 하나는 Z3입니다. Microsoft에서 개발한 이 도구는 정리 증명이라고 할 수 있으며 내부에서 매우 복잡한 수학 연산을 수행하는 사용하기 쉬운 함수를 노출합니다.
유효한 Magic 패킷을 만들기 위해 사용할 또 다른 도구는 대화형 패킷 조작에 널리 사용되는 Python 라이브러리인 scapy입니다.
허용된 패킷의 경로를 파악할 방법이 이미 있다는 점을 고려할 때, 문제를 자체적으로 해결한 다음 이 솔루션을 네트워크 패킷의 각 오프셋에 있는 바이트로 변환하는 일만 남았습니다.
지정된 프로그램에서 수행된 경로를 탐색하는 일반적인 기술을 기호 실행이라고 합니다. 이 기술을 위해 Cloudflare는 제약 조건을 포함하여 변수로 사용할 수 있는 입력을 제공합니다. Cloudflare는 경로가 성공한 결과의 결과를 알고 있으므로, 도구를 조율하여 이러한 모든 성공적인 경로를 찾고 최종 결과를 맥락에 맞는 형식으로 표시할 수 있습니다.
이를 위해서는 확인 중인 조건의 결과로 상수, 레지스트리, 다양한 부울 연산자 등의 상태를 추적할 수 있는 소형 머신을 구현해야 합니다.
class BPFPacketCrafter:
MIN_PKT_SIZE = 64 # Minimum packet size (Ethernet + IP + UDP headers)
LINK_ETHERNET = "ethernet" # DLT_EN10MB - starts with Ethernet header
LINK_RAW = "raw" # DLT_RAW - starts with IP header directly
MEM_SLOTS = 16 # Number of scratch memory slots (M[0] to 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
# Symbolic packet bytes
self.packet = [BitVec(f"pkt_{i}", 8) for i in range(self.pkt_size)]
# Symbolic registers (32-bit)
self.A = BitVecVal(0, 32) # Accumulator
self.X = BitVecVal(0, 32) # Index register
# Scratch memory M[0-15] (32-bit words)
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"(누산기) 레지스를 기본 상태로 초기화합니다.
성공적인 경로로 식별된 경로의 지침을 반복합니다.
Z3 check() 함수를 사용하여 조건이 주어진 제약(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에 표시되는 제약 조건의 첫 번째 부분은 링크 계층 BPF 명령을 처리할 때 유효한 이더넷 IP를 구축할 수 있도록 추가된 제약 조건입니다. "If" 문은 감지된 프로토콜에 따라 특정 제약 조건을 적용합니다.
IPv4 로직(0x0800):
pkt_14 & 240 == 64: 바이트 14가 IP 헤더의 시작입니다. 0xF0 마스크는 버전이 4(0x40)인지 확인하기 위해 높은 니블(버전 필드)을 격리합니다.
pkt_14 & 15 == 5: 15 (0x0F), 낮은 니블을 격리(Ihl - 인터넷 Header Length). 따라서 헤더 길이는 5(20바이트)가 되어야 하며, 이는 옵션을 제외한 표준 크기입니다.
IPv6 로직(0x86dd):
다른 값을 검사하는 두 번째 부분을 보면 네트워크 패킷 값을 관찰할 수 있습니다.
예상 값 옆에 주어진 패킷에서 해당 값이 존재해야 하는 위치의 바이트 오프셋을 볼 수 있습니다(예: pkt_12, pkt_13).
특정 오프셋에 어떤 바이트가 존재해야 하는지 확인했으니, 이제 scapy를 사용해 이를 실제 네트워크 패킷으로 변환할 수 있습니다. 이전 Z3 제약 조건의 바이트에서 새 패킷을 생성하면 패킷이 어떻게 보이는지 명확하게 확인할 수 있으며 추가 처리를 위해 저장할 수 있습니다.
###[ Ethernet ]###
dst = 00:00:00:00:00:00
src = 00:00:00:00:00:00
type = IPv6 <-- IPv6 Packet
###[ IPv6 ]###
version = 6
tc = 0
fl = 0
plen = 0
nh = UDP <-- UDP Protocol
hlim = 0
src = ::
dst = ::
###[ UDP ]###
sport = 0
dport = domain <-- Port 53
len = 0
chksum = 0x0
이 새로 만들어진 패킷은 추가 연구에 사용하거나 네트워크를 통해 스캔하여 이러한 임플란트의 존재를 식별하는 데 사용할 수 있습니다.
특정 BPF 지침 세트가 수행하는 작업을 이해하는 것은 번거롭고 시간이 많이 소모되는 작업일 수 있습니다. 사용된 예는 총 16개 명령에 불과하지만, 200개 이상의 명령인 샘플을 이해하는 데 적어도 하루는 걸렸을 것입니다. 이제 Z3 솔버를 사용하여 이 시간을 초 단위로 단축하고 허용된 패킷의 경로뿐만 아니라 이 패킷의 뼈대까지 표시할 수 있습니다.
커뮤니티에서 BPF 기반 임플란트의 해체를 자동화할 수 있도록 filterforge 도구를 오픈 소스로 제공했습니다. 여러분은 저희 GitHub 리포지토리에서 소스 코드와 사용 예시를 찾아보실 수 있습니다.
이 연구 결과를 게시하고, 분석가가 BPF 명령어를 알아내는 데 소요되는 시간을 줄여주는 도구를 공유함으로써, 다른 분들의 추가 연구에 이 형태의 자동화를 확장하기 위한 계기가 되길 바랍니다.