bpf

From bytecode to bytes- automated magic packet generation (새 탭에서 열림)

리눅스 악성코드는 커널 내에서 네트워크 트래픽을 처리하는 BPF(Berkeley Packet Filter) 프로그램을 이용해 특정 '매직 패킷'을 받을 때까지 잠복하는 방식을 자주 사용합니다. 수백 줄에 달하는 복잡한 BPF 바이트코드를 수동으로 역공학하여 매직 패킷의 구조를 파악하는 것은 분석가에게 매우 고무적인 작업이나 시간 소모가 큽니다. 이 글은 Z3 정리 증명기(Theorem Prover)를 활용한 심볼릭 실행(Symbolic Execution) 기법을 통해, 복잡한 필터 조건을 논리적 제약식으로 변환하고 이를 통과하는 패킷을 단 몇 초 만에 자동으로 생성하는 자동화 도구의 원리와 성과를 설명합니다. ### Classic BPF와 악성코드의 은닉 기법 * **Classic BPF의 특성:** 현대적인 eBPF와 달리 2개의 레지스터만을 사용하는 단순한 가상 머신 구조로, tcpdump와 같은 도구에서 네트워크 트래픽을 고속 필터링하기 위해 설계되었습니다. * **백도어 활용:** 커널 깊숙한 곳에서 동작하며 사용자 공간의 보안 도구로부터 트래픽을 숨길 수 있다는 점 때문에, BPFDoor와 같은 지능형 지속 위협(APT) 공격자들이 선호합니다. * **분석의 한계:** 악성 BPF 프로그램은 100줄 이상의 복잡한 명령어로 구성되기도 하며, LLM을 활용한 코드 해석만으로는 실제 필터를 통과하는 정확한 네트워크 패킷 바이트를 재현하기 어렵습니다. ### BPFDoor 사례를 통한 필터 논리 분석 * **동작 원리:** BPFDoor는 특정 포트를 열지 않고 유입되는 모든 트래픽을 감시하다가, 미리 정의된 특정 조건(오프셋, 프로토콜, 포트 등)을 만족하는 패킷이 들어오면 활성화됩니다. * **명령어 구조:** 실제 샘플 분석 결과, 이더넷 타입(IPv4/IPv6), 프로토콜(UDP), 목적지 포트(DNS/53) 등을 순차적으로 검사하여 'ACCEPT' 또는 'DROP' 여부를 결정하는 논리적 경로를 가집니다. * **경로 탐색:** 필터 내에는 패킷을 허용(ACCEPT)하는 여러 경로가 존재하며, 각 경로는 특정 바이트 위치의 값이 무엇이어야 하는지에 대한 구체적인 제약 조건을 포함하고 있습니다. ### 심볼릭 실행 및 Z3를 이용한 패킷 자동 생성 * **제약 조건 해결:** BPF의 결정론적(Deterministic) 특성을 활용해, 패킷 데이터를 미지수(Symbolic)로 두고 Z3 정리 증명기를 통해 필터 조건을 만족하는 값을 역산합니다. * **최단 경로 탐색 알고리즘:** 큐(Queue) 기반의 탐색 방식을 사용하여 'ACCEPT' 결과에 도달하는 가장 효율적인 명령어 실행 경로를 추적합니다. * **자동화의 이점:** 분석가가 수동으로 어셈블리 코드를 보며 패킷 바이트를 계산할 필요 없이, 알고리즘이 자동으로 유효한 명령어 경로를 따라가며 매직 패킷의 전체 바이트 배열을 생성해 줍니다. 이러한 자동화 방식은 수 시간이 걸리던 수동 분석 작업을 단 몇 초 만에 완료할 수 있게 해줍니다. 보안 분석가들은 이 기술을 활용해 BPF 기반 백도어를 신속하게 무력화하고, 침해 사고 대응 과정에서 공격자가 사용하는 통제 신호를 즉각적으로 식별할 수 있습니다.