기술 요약: 하이멀달

문제 정의

확장된 버클리 패킷 필터(eBPF) 프로그램은 네트워킹, 관측 가능성 및 보안을 위한 리눅스 커널 확장에서 핵심적입니다. 커널 내 eBPF 검증기는 저수준 메모리 안전성과 종결성을 강제하지만, 초기화 규칙, 스키마 일관성, 오류 처리와 같은 고수준 소스 수준의 속성은 강제하지 못합니다. 저자들은 커널 검증기를 통과하고 컴파일되지만 데이터를 조용히 손상시키거나 민감한 정보를 유출하거나 잘못된 강제 결과를 초래할 수 있는 여섯 가지 범주의 소스 수준 버그를 문서화했습니다.

식별된 주요 취약점은 다음과 같습니다:

• 초기화되지 않은 상태: 영구 초기화 없이 스택에 상주하는 구조체를 생성하는 프로그램은 커널 포인터와 반환 주소를 포함한 CPU 당 스택 잔여물을 유출하며, 이는 커널 주소 공간 레이아웃 무작위화 (KASLR) 슬라이드를 복구하기에 충분합니다.
• 확인되지 않은 헬퍼 반환: 실패하는 헬퍼 함수 (예: bpf_probe_read_user_str) 는 종종 무시되어 잘린 문자열 대신 오래된 스택 데이터가 생성됩니다.
• 버퍼/크기 불일치: 개발자가 출력 헬퍼에 잘못된 크기를 전달하면 커널 포인터가 포함된 인접한 비공개 필드가 유출될 수 있습니다.
• 후크/컨텍스트 불일치: 잘못된 컨텍스트 구조체 (예: XDP 후크에서의 __sk_buff) 를 사용하면 데이터가 잘못 해석됩니다.
• 맵 유형/스키마 혼동: 선언된 맵 값 크기와 실제 데이터 간의 불일치, 또는 맵 조회 결과를 관련 없는 유형으로 재해석하는 경우입니다.
• 부호/부호 없는 혼동: 오류를 나타내는 부호 있는 헬퍼 반환 값을 부호 없는 필드에 저장하면 맵 키로 사용되는 가짜 큰 양수 값이 생성됩니다.

또한, eBPF 검증기 자체도 (불완전한 가지치기, 계약 검증 누락 등) 알려진 취약점을 가지고 있어 악용될 수 있습니다. Rust 와 같은 메모리 안전한 언어로의 이전은 이러한 격차를 해소할 수 있지만, 대규모로 수동 재작성은 실용적이지 않으며 기존 자동화 번역 도구는 eBPF 컨텍스트에서 의미적 동등성이나 안전성을 보장할 만큼 엄격하지 않습니다.

방법론: 하이멀달 파이프라인

하이멀달은 레거시 libbpf C 프로그램을 관용적이고 안전한 Aya Rust 로 번역하는 자동화 파이프라인입니다. 이는 대규모 언어 모델 (LLM), 정적 분석, 형식 검증을 결합한 5 단계 반복 프로세스를 사용합니다:

1. LLM 번역: LLM 은 Aya API 매핑, 후크 매크로 및 작동 예제를 사용하여 C 소스를 Rust 로 번역합니다.
2. 컴파일 및 커널 검증: 생성된 Rust 코드는 eBPF 바이트코드로 컴파일됩니다. 컴파일러 린트 가드 (예: 사용되지 않는 unsafe 블록 거부) 와 커널 검증기가 기본 안전성과 정확성을 확인합니다. 오류는 수리를 위해 LLM 으로 피드백됩니다.
3. 안전성 확인 (정적 분석): 커스텀 정적 분석 엔진이 컴파일러와 검증기가 놓칠 수 있는 Rust 소스의 unsafe 탈출구를 스캔합니다. 여기에는 타입 지정되지 않은 링 버퍼 예약 금지, 영구 초기화 강제, 헬퍼 반환에 대한 Result 유형의 명시적 처리 요구가 포함됩니다.
4. 심볼릭 실행: 원래 C 바이너리와 컴파일된 Rust 바이너리는 커스텀 angr 용 eBPF 백엔드에 로드됩니다. 이 백엔드는 eBPF 헬퍼, 맵, 재배치 및 원자 연산을 모델링합니다. 심볼릭 실행을 수행하여 모든 가능한 경로를 탐색하고 반환 값 및 맵 부작용에 대한 구조화된 수식을 생성합니다.
5. 동등성 확인: Z3 기반 솔버가 C 및 Rust 프로그램이 의미적으로 동등한지 확인합니다. 저자들은 조건부 의미적 동등성을 도입하여 선언된 안전 조건 (예: 헬퍼 호출 성공) 을 만족하는 입력에 대해서만 동등성을 요구합니다. 이는 버그가 트리거되는 경로에서 버그가 있는 C 소스와 동등하다고 간주되도록 하되, 유효한 경로에서는 로직이 보존됨을 여전히 검증할 수 있게 하여 오류를 처리하거나 메모리를 영구 채우는 더 안전한 Rust 번역을 허용합니다. 반례가 발견되면 표적 수리를 위해 LLM 으로 피드백됩니다.

이를 지원하기 위해 저자들은 ELF 로더, 아키텍처 정의, VEX IR 리프터 및 헬퍼 스텁을 포함한 완전한 angr 용 eBPF 백엔드를 구축했습니다. 또한 심볼릭 키 하의 맵 부작용을 모델링하고 "마지막 쓰기 우선" 시맨틱을 포착하는 커스텀 ITE-체인 인코딩을 개발했습니다.

주요 기여

• 하이멀달 파이프라인: 관찰 가능한 행동 보존에 대한 프로그램별 형식 보장을 갖춘 프로덕션 eBPF 프로그램을 C 에서 Rust 로 번역하는 최초의 자동화 시스템.
• 조건부 동등성: 버그 트리거링 경로에서 다르게 동작하는 안전성 개선 번역을 검증하기 위해 동등성 검사를 안전한 실행 경로로 제한하는 새로운 검증 접근법.
• eBPF 심볼릭 실행 백엔드: 커널 헬퍼, 맵 및 BPF-to-BPF 호출을 모델링하여 바이트코드 수준에서 형식 추론을 가능하게 하는 angr 을 위한 완전한 eBPF 백엔드.
• Safe-Aya 정적 분석기: 커널 검증기를 통과하지만 안전하지 않은 Rust 패턴 (예: 타입 지정되지 않은 링 버퍼, 무시된 헬퍼 오류) 을 거부하는 정책 엔진.
• 보안 발견: KASLR 복구 (스택 잔여물을 통해) 및 링 버퍼 내 교차 이벤트 콘텐츠 유출을 포함한 10 개의 오픈 소스 eBPF 프로그램에서 이전에 보고되지 않은 정보 유출 발견.
• 벤치마크 및 평가: 102 개 eBPF 프로그램의 공개 벤치마크 및 번역 파이프라인에 대한 포괄적 평가.

결과

이 시스템은 다양한 출처 (libbpf-tools, libbpf-bootstrap, KEN, Suricata 등) 의 102 개 실제 eBPF 프로그램에서 평가되었습니다.

• 성공률: 하이멀달은 **96 개의 형식 검증 동등 번역 (94.1%)**을 생성했습니다. 나머지 6 개는 심볼릭 실행 한계로 인해 부분적으로 검증되었거나 솔버 확장성 한계를 초과했습니다.
• 버그 해결: 96 개의 검증된 번역에서 하이멀달은 관찰된 초기화되지 않은 상태, 확인되지 않은 헬퍼 반환, 부호/부호 없는 혼동의 모든 사례를 100% 해결했습니다.
• 베이스라인 대비 비교: 하이멀달 파이프라인이 없는 베이스라인 LLM 에이전트와 비교하여 하이멀달 (에이전틱) 은 98% 의 3 회 통과율(컴파일, 커널 검증, 안전성, 동등성) 을 달성했으며, 베이스라인은 4~12% 였습니다.
• 런타임 오버헤드: 10 개 프로그램에 대한 런타임 검증 결과, Rust 번역은 일반적으로 modest 한 오버헤드 (C 대비 기하 평균 0.44 배3.60 배) 를 발생시켰으며, 대부분 1.14 배1.89 배 사이였습니다.
• 안전성: 번역은 식별된 취약점을 유발한 특정 안전하지 않은 패턴 (초기화되지 않은 메모리, 확인되지 않은 오류) 을 제거했습니다.

의의

이 논문은 하이멀달이 관찰 가능한 행동 보존에 대한 프로그램별 형식 보장을 갖춘 프로덕션 eBPF 프로그램의 메모리 안전한 이전을 자동화하는 최초의 시스템이라고 주장합니다. 이는 커널 검증기의 저수준 보장과 현대 eBPF 애플리케이션의 고수준 안전 요구사항 사이의 격차를 해소합니다. LLM 과 형식 검증 및 정적 분석을 결합함으로써 하이멀달은 자동화 번역이 문법적으로 정확할 뿐만 아니라 의미적으로 동등하며 커널 검증기가 감지할 수 없는 특정 범주의 소스 수준 안전성 버그가 없는 코드를 생성할 수 있음을 입증합니다. 이 작업은 eBPF 이전을 위한 새로운 벤치마크를 수립하고 더 견고하고 메모리 안전한 커널 확장을 구축하기 위한 기반을 제공합니다.