프로그램 분석을 위한 은하수를 여행하는 히치하이커를 위한 안내서, 제3부: 대체로 무해한 LLM들

LLM(Large Language Models)은 코드에 대해 추론하고 잠재적인 버그가 실제 실행 컨텍스트에서 트리거될 수 있는지 판단하는 버그 분석에 점점 더 많이 사용되고 있으며, 최근 연구들은 유망한 실증적 결과들을 보여주고 있습니다. 하지만 실증적인 효과성이 있다고 해서, 모델이 생성한 그럴듯한 근거(rationale)가 경고(warning)를 해제(discharging)하기에 충분한 것은 아닙니다. 이러한 구분은 특히 '버그 없음(no-bug)' 결정에서 매우 중요합니다. 보고된 오류 상태가 분석 중인 프로그램 컨텍스트 내에서 도달 불가능(unreachable)하다는 것을 입증해야 하며, 단순히 왜 발생하지 않을 수 있는지에 대한 그럴듯한 설명을 제공하는 것만으로는 보고된 오류나 경고를 기각할 수 없기 때문입니다. 우리는 프로그램 동작 추론(program-behavior reasoning)이 LLM에 의해 직접 수행되기보다는 형식 분석(formal analysis)에 기반해야 한다고 주장합니다. 우리는 LLM의 보조와 프로그램 동작 추론을 분리하여, 후자를 백엔드 분석(backend analysis)에 위임하는 버그 분석 시스템인 Evident를 제시합니다. 보고된 위치와 데이터 흐름(data flow)을 명시하는 경고가 주어지면, Evident는 경고별 분석 하네스(analysis harness)를 구축하는 데에만 LLM을 사용합니다. 그 후 Evident는 백엔드를 호출하기 전에 해당 하네스를 검증합니다. 백엔드는 하네스 상대적 체크(harness-relative check)를 수행합니다: 즉, 보고된 오류 상태가 구축된 하네스와 그 가정(assumptions) 하에서 도달 불가능한지를 확인합니다. 우리는 기존의 두 가지 정적 탐지기(static detectors)로부터 추출한 200개의 실제 Android 커널 드라이버 경고를 대상으로 Evident를 평가했습니다. Evident는 데이터셋 내의 확인된 버그를 하나도 해제하지 않으면서, 111개의 오탐(false alarms)을 해제하는 것을 포함하여 151개의 사례(76%)를 정확하게 분류했습니다. 나머지 사례들은 해결되지 않았거나 잠재적 버그로서 보수적으로 유지되었습니다. 또한 Evident는 이전의 LLM 기반 필터링과 수동 분류(manual triage) 모두에서 간과되었던 확인된 취약점(vulnerability)을 재발견했습니다.