기술 요약: 리눅스 커널 드라이버의 참조 카운팅 버그 자동 탐지

문제 정의

리눅스 모놀리식 커널에서 장치 드라이버는 핵심 커널과 동일한 권한 수준에서 작동하므로, 드라이버의 버그는 치명적인 보안 위험이 됩니다. 참조 카운팅 (refcount) 은 커널 객체의 수명 주기를 수동으로 관리하는 데 사용되는 주요 메커니즘입니다. 참조 카운트는 객체에 대한 활성 참조 수를 추적하며, 양수 카운트는 객체가 사용 중임을 나타내고, 0 은 해당 객체를 해제해도 안전함을 의미합니다.

참조 카운트가 실제 참조 수와 일치하지 않을 때 참조 카운팅 버그가 발생합니다. 과도한 참조 카운트는 메모리 누수로 이어지는 반면, 불충분한 참조 카운트는 use-after-free(UAF) 취약점을 초래합니다. 이러한 문제들은 커널 코드베이스의 복잡성 (드라이버는 커널의 약 66.5% 를 구성함) 과 드라이버 구현의 다양성으로 인해 광범위하게 존재합니다. 기존 정적 분석 도구들은 리눅스 커널의 규모와 복잡성으로 인해 종종 어려움을 겪어, 높은 오탐률이나 확장성 부족을 초래합니다.

방법론: DrvHorn

저자들은 리눅스 커널 드라이버 내에서 참조 카운팅 버그를 탐지하도록 설계된 새로운 자동화 도구인 DrvHorn을 소개합니다. 이 도구는 리눅스 커널이 제공하는 구조화된 인터페이스를 활용하여 참조 카운팅 검증 문제를 어설션 (assertion) 검사 문제로 변환합니다.

핵심 아키텍처

DrvHorn 은 LLVM 비트코드로 컴파일된 리눅스 커널 소스 코드를 기반으로 작동합니다. 그 워크플로우는 네 가지 주요 단계로 구성됩니다:

1. 어설션 검사로 축소:
   DrvHorn 은 전체 커널을 검증하는 대신 드라이버 초기화 단계에 집중합니다. 초기화가 실패할 경우 누수를 방지하기 위해 획득한 모든 자원을 해제해야 한다는 관찰을 활용합니다. 이 도구는 드라이버의 초기화 함수를 호출하고, 실패 시 참조 카운트의 순 변화 (장치, 장치 트리 노드, 펌웨어 노드에 대해) 가 0 이어야 한다는 어설션을 생성하는 검증 목표를 생성합니다. 어설션이 실패하면 버그가 보고됩니다.

2. 리눅스 커널 모델링:
   커널의 복잡성을 관리하기 위해 DrvHorn 은 참조 카운팅 동작을 보존하는 단순화된 추상화로 특정 커널 API 를 대체합니다:

   • 장치 트리: struct device_node의 복잡한 포인터 구조를 모델링하는 대신, DrvHorn 은 NULL 반환, NULL 이 아닌 값 반환, 참조 카운트 감소, 또는 감소 없음의 네 가지 명확한 동작 유형에 기반하여 API(예: of_get_next_child, of_find_node_by_name) 를 모델링합니다.
   • 장치 및 버스: 참조 카운트가 증가된 장치를 반환하는 API(예: usb_find_interface) 는 버스 인자에 의해 결정된 특정 비-별칭 (non-aliasing) 메모리 영역을 가리키는 포인터를 반환하도록 모델링되어, 불필요한 별칭 위반을 방지합니다.
   • 장치 리소스 관리 (Devres): 이 도구는 __devm_add_action()을 단순화하여 호출 지점 직후 관련 정리 (cleanup) 함수를 즉시 호출함으로써, devres 목록을 명시적으로 추적하는 대신 처리합니다.

3. 공격적 프로그램 슬라이싱:
   표준 데드 코드 제거 (DCE) 는 커널 규모에는 불충분합니다. DrvHorn 은 맞춤형 공격적 슬라이싱 기법을 구현합니다:

   • 필수 인자: 참조 카운트를 변경할 수 있는 struct kref를 포함하는 인자는 필수로 표시됩니다.
   • 명령어 수집: 이 도구는 필수 인자에 의존하는 분기, 반환, 호출을 포함하여 참조 카운팅 검증에 필요한 명령어를 재귀적으로 수집합니다.
   • 비필수 대체: 필수로 간주되지 않는 명령어는 제거됩니다. 비필수 결과를 가진 함수 호출은 부수 효과 손실을 완화하기 위해 LLVM 의 writeonly 속성을 사용하여 비결정적 값으로 대체됩니다.

4. CHC 기반 검증:
   축소된 어설션 문제는 SeaHorn이라는 제약 호른 절 (Constraint Horn Clause, CHC) 솔버를 사용하여 해결됩니다. 저자들은 루프 풀링 수를 수동으로 설정해야 하는 바운드 모델 체커 (SeaBMC 등) 보다 CHC 솔버가 참조 카운팅 조작에서 흔히 발생하는 루프 처리에 더 적합하기 때문에 SeaHorn 을 선택했습니다.

주요 기여

• 새로운 불변식: 모든 드라이버에 적용 가능한 보편적인 참조 카운팅 불변식 도출: 드라이버 초기화가 실패할 때 참조 카운트 차이는 0 이어야 한다.
• 자동화 도구: 커널 모델링, 공격적 슬라이싱, CHC 해결을 통합하여 완전 자동화된 탐지를 달성하는 DrvHorn 개발.
• 확장성과 정확도: 기존 최첨단 도구보다 현저히 낮은 오탐률로 수천 개의 드라이버를 분석할 수 있는 능력.
• 실제 영향: 리눅스 커널에서 이전에 알려지지 않았던 버그를 발견하고 패치하는 것.

평가 결과

저자들은 x86-64 리눅스 커널 v6.6( allyesconfig 로 컴파일됨) 의 3,387 개 플랫폼 드라이버에 대해 DrvHorn 을 평가했습니다.

• 버그 탐지: DrvHorn 은 777 개의 잠재적 버그를 보고했습니다.
• 검증: 수동 검사를 통해 545 개가 실제 버그로 확인되었습니다.
• 오탐: 232 개의 오탐이 발생하여 오탐률은 **29.9%**였습니다. 저자들은 이 중 27 개는 슬라이싱 정책의 부조화 (간접 정보 흐름) 로 인해 발생했으며, 나머지는 솔버의 메모리 모델에서의 보수적 포인터 분석 때문이라고 지적했습니다.
• 새로움: 확인된 버그 중 424 개는 이전에 알려지지 않았습니다.
• 상류 병합: 저자들은 발견된 버그에 대한 패치를 제출했으며, 45 개가 리눅스 커널에 병합되었습니다.
• 오탐 (False Negatives): v6.6 릴리스 이후 수정된 17 개의 알려진 버그에 대한 테스트에서 DrvHorn 은 간접 정보 흐름과 관련된 슬라이싱 제한으로 인해 단 하나만 놓쳤으며, 이는 낮은 오탐률을 시사합니다.
• 타임아웃: 이 도구는 300 초 제한으로 807 개의 드라이버에서 타임아웃되었으며, 이는 종종 유틸리티 함수의 복잡한 중첩 루프로 인해 발생했습니다.
• 비교: 바운드 모델 체킹인 SeaBMC 와 비교했을 때, SeaBMC 는 DrvHorn 이 찾은 실제 버그의 39.4% 를 놓쳤으며, 이 중 24.2% 에서 타임아웃되어 이 특정 작업에 대한 CHC 기반 접근법의 우월성을 확인시켜 주었습니다.

중요성과 주장

이 논문은 DrvHorn 이 다양한 리눅스 드라이버 생태계에서 기존 도구들이 달성하기 어려웠던 확장성과 정확도의 균형을 달성했다고 주장합니다. 특히 드라이버에 초점을 맞추고 커널의 드라이버 인터페이스를 활용하여 간단한 불변식을 도출함으로써, 다른 검증 노력들을 종종 괴롭히는 복잡한 서브시스템별 불변식의 필요성을 피합니다.

저자들은 DrvHorn 이 완전하지도 불완전하지도 않음 (버그를 놓치거나 오탐을 보고할 수 있음) 을 강조하지만, 발견된 실제의 알려지지 않은 버그의 높은 수와 성공적인 상류 패치 병합으로 그 실용적 유용성이 입증되었다고 말합니다. 이 도구는 중요한 보안 취약점 벡터를 해결하는 리눅스 커널 드라이버에 대한 완전 자동화되고 고정밀한 정적 검증을 향한 중요한 걸음을 나타냅니다.

인정된 제한 사항:

• 이 도구는 현재 초기화 단계에 초점을 맞추고 있으며, 정리/종료 함수로의 확장은 향후 과제로 남겨둡니다.
• 현재 struct kref 유형 외의 참조 카운팅은 검증하지 않습니다.
• 오탐률은 이전 연구보다 낮지만 여전히 무시할 수 없습니다 (29.9%). 이는 주로 솔버의 보수적 메모리 모델링 때문입니다.
• 간접 정보 흐름은 슬라이싱 정책에 의해 완전히 포착되지 않아 일부 버그 누락과 오탐이 발생합니다.