기술 요약: LLM 기반 프로그램 분석을 위한 에이전트적 해석

1. 문제 제기

대형 언어 모델 (LLM) 은 소스 코드 이상의 정보, 즉 문서, 보안 권고사항, 버전별 메타데이터, 비공식 API 계약 등에 접근함으로써 프로그램 분석에 고유한 능력을 제공합니다. 그러나 LLM 에 "원샷 (one-shot)" 전체 프로그램 분석을 의존하는 것은 본질적으로 다음 세 가지 주요 이유로 인해 취약합니다:

1. 맥락 민감성: 실증 연구에 따르면 모델의 성능은 맥락 길이와 작업 복잡도가 증가함에 따라 저하되며, 결과는 프롬프트 내 정보의 순서에 크게 의존합니다. 중요한 증거 (예: 특정 보안 권고사항) 가 제공되더라도 신뢰성 있게 활용되지 않을 수 있습니다.
2. 지속 가능한 상태의 부재: 단일화된 LLM 응답은 어떤 특정 주장이 지지되었는지, 반박되었는지, 아니면 미결 상태로 남았는지를 추적할 수 있는 지속 가능한 상태를 갖지 못합니다. 이로 인해 자기 모순적인 추론이나 자신의 결론을 지지하지 못하는 추론을 처리하기 어렵습니다.
3. 의존성 구조의 부재: 단일 회차 답변은 피드백을 위한 메커니즘을 제공하지 않습니다. 나중에 발견된 사실이 이전 질문의 범위가 잘못되었거나, 상류 구성 요소가 다른 가설 하에서 재검토가 필요함을 드러낼 경우, 비구조화된 답변은 이러한 반복적 정제를 용이하게 할 수 없습니다.

결과적으로, 특히 소스 코드나 형식 명세에 관련 사실이 완전히 포함되지 않은 증거 의존적 프로그램 분석을 위해, 즉흥적인 LLM 프롬프팅과 완전히 명세된 정적 분석 사이의 간극을 메우는 프레임워크가 필요합니다.

2. 방법론: 에이전트적 해석

본 논문은 LLM 기반 추론에 격자 기반 정적 분석의 엄격함을 적용하는 에이전트적 해석 (Agentic Interpretation) 프레임워크를 제안합니다. 이 방법론은 고차원 분석 목표를 프로그램 지점과 구성 요소 경계에 고정된 국소적 주장으로 분해하고, 유한 높이 격자와 작업 목록 (worklist) 알고리즘을 통해 그 진화를 관리합니다.

2.1 핵심 구성 요소

• 평가 그래프 ($G^*$): 프로그램 유도 그래프 ($G_{prog}$) 를 확장한 것으로 다음을 포함합니다:
  • 보조 노드: 단일 프로그램 지점에 매핑되지 않는 구성 요소 간 상호작용이나 목표를 나타내는 노드.
  • 맥락 간선: 노드 $n$의 주장이 평가될 때, 선행 노드들의 현재 평가 상태와 증거를 받도록 하는 순방향 흐름 간선.
  • 피드백 간선: 하류 평가가 변경될 때 (예: 반박된 구성 주장이 불투명한 구성 요소 내 표적 검색을 유발함) 상류 노드의 재평가를 트리거하는 역방향 흐름 간선.
• 평가 도메인 (격자): 주장의 증거 상태를 요약하는 유한 높이 join-반격자 (join-semilattice, $A$).
  • 논문은 AGraded 격자를 예시로 들며, 이는 $\{ \perp, w, s \} \times \{ \perp, w, s \}$로 표현됩니다. 여기서 첫 번째 좌표는 지지 증거를, 두 번째 좌표는 반박 증거를 나타냅니다. 값은 부재 ($\perp$) 에서 약함 ($w$), 강함 ($s$) 으로 범위를 가집니다.
  • 이 격자는 구체적인 프로그램 상태에 대한 추상 도메인이 아니라, 증거 상태에 대한 인식론적 (epistemic) 도메인입니다. 이는 주장이 지지되거나 반박되었는지, 그리고 그 증거의 강도를 기록합니다.
• 작업 목록 하네스: 분석 상태를 관리하는 제어 루프.
  • 맥락화: 노드 $n$에 대해 하네스는 소스 코드, 고차원 목표, 선행 노드들의 현재 평가를 사용하여 프롬프트 맥락 ($\Gamma_n$) 을 구성합니다.
  • 노드 변환기: LLM 에이전트는 두 가지 작업을 수행합니다:
    1. 평가: 맥락에 대한 기존 주장을 평가하여 업데이트된 평가와 증거 기록을 반환합니다.
    2. 생성: 맥락에 기반하여 새로운 관련 주장을 제안합니다.
  • 전파: 새로운 평가와 기존 평가의 join 이 격자 순서에서 엄격한 증가를 초래하는 경우, 해당 노드의 확장된 후속 노드들이 재평가를 위해 대기열에 추가됩니다.

2.2 분석 과정

이 과정은 불투명한 서드파티 구성 요소 (JSON 파서 및 서명 검증기) 를 가진 프로그램에 대한 보안 검토를 통해 설명됩니다.

1. 초기화: 작업 목록에 모든 프로그램 및 보조 노드가 시드됩니다.
2. 반복적 정제:
   • 1 단계: 구성 요소의 초기 독립적 평가 (예: 파서 및 검증기에 대한 문서 검토).
   • 2 단계: 증거의 구성. 프레임워크는 구성 요소 간 주장 (예: "구성 요소들이 공동으로 안전을 보장하는가?") 을 평가합니다. 구성 주장이 약하게 반박되면, 피드백 간선이 상류 구성 요소의 재조사를 트리거합니다.
   • 3 단계: 피드백 기반 정제. 반박된 구성의 맥락 (예: "프로세서가 유효성 검사를 수행하지 않음") 은 LLM 이 광범위한 검토 대신 특정 취약점 (예: 프로토타입 오염) 을 위한 표적 검색을 수행하도록 안내합니다.
   • 4 단계: 안정화. 강화된 상류 증거가 전방으로 전파되어 글로벌 목표에 대한 강력한 반박으로 이어집니다. 평가에서 더 이상 엄격한 증가가 발생하지 않을 때 작업 목록이 비어집니다.

3. 주요 기여

본 논문은 세 가지 주요 기여를 합니다:

1. 프레임워크 제안: 증거 의존적 프로그램 분석을 위한 구조화된 접근법으로 에이전트적 해석을 도입하며, LLM 이 필요하지만 직접적인 프롬프팅만으로는 불충분한 적합한 문제 영역을 규명합니다.
2. 형식적 모델: 평가 그래프, 평가 도메인, 노드 변환기, 작업 목록 알고리즘을 정의하여 핵심 모델을 형식화합니다.
3. 디자인 공간 특성화: 디자인 공간을 탐구합니다.
   • 평가 격자: 거친 격자 (예: 존재/부재) 와 세밀한 격자 (예: 강도, 신뢰 기반) 간의 트레이드오프를 논의합니다. 증거 강도와 신뢰 기반 (예: "모델 전용" 대 "검증됨") 을 별도로 추적하는 AStratified 도메인을 도입합니다.
   • 주장 관리: 주장의 표준화, 세분성, 범위를 다룹니다.
   • 쿼리 설계: 평가 쿼리 (지지/반박) 와 생성 쿼리 (새로운 주장 제안) 를 구분합니다.
   • 종결: 비결정적 LLM 응답이 존재하더라도 업데이트가 단조롭다면 (join 을 통해), 유한 높이 격자와 제한된 주장 생성을 가진 알고리즘이 종료됨을 증명합니다.

4. 결과 및 한계

• 결과: 논문은 불투명한 구성 요소를 가진 핸들러에 대한 보안 검토라는 구체적 예시를 제공하여, 프레임워크가 목표를 어떻게 분해하고, 피드백 루프를 활용하여 검색을 정제하며, 최종 평가에 어떻게 안정화되는지 보여줍니다. 이는 여러 출처의 약한 증거를 결합하여 강력한 반박으로 전환함으로써 글로벌 보안 목표가 위반됨을 프레임워크가 어떻게 감지할 수 있는지 보여줍니다.
• 한계:
  • 논문은 진행 중인 작업을 기술합니다. 실제 구현이나 실험적 평가는 포함하지 않습니다.
  • 프레임워크는 종결과 유계성을 보장하지만, 전통적인 의미의 **정확성 (soundness)**을 보장하지는 않습니다 (즉, LLM 의 결론이 정확함을 증명하지는 않음). 이는 LLM 의 증거 역할을 명시적이고 감사 가능하게 만듭니다.
  • 프레임워크는 증거를 지속적으로 오인하는 에이전트를 수정할 수는 없으며, 그러한 오류를 가시화할 뿐입니다.
  • 종료 증명 주장이 결코 취소되지 않으며 평가가 join 을 통해만 증가한다는 가정에 의존합니다. 신념 수정 (평가 하향) 메커니즘은 제한된 교체 또는 시대별 재계산이 필요한 향후 작업으로 논의됩니다.

5. 의의

이 작업의 의의는 프로그램 분석에서 LLM 기반 추론에 구조적 엄격함을 도입하려는 시도점에 있습니다. LLM 의 출력을 위한 형식적 검증기가 필요한 "생성 및 확인" 패러다임과 LLM 이 정확성에 영향을 미칠 수 없는 "휴리스틱 오라클" 패러다임에서 벗어나, 에이전트적 해석은 중간 지점을 목표로 합니다.

이는 다음과 같은 증거 의존적 분석에서 중요합니다:

• 관련 사실이 형식화될 수 없는 경우 (예: 비공식 API 계약, 보안 권고사항).
• 완전한 검증자가 존재하지 않는 경우.
• 분석이 다양한 비코드 출처의 정보를 종합해야 하는 경우.

이 프레임워크는 LLM 을 블랙박스 생성기에서 더 큰 분석 시스템의 유계적이고 감사 가능한 구성 요소로 변환합니다. 이는 분석이 통제되고 원칙적인 방식으로 진행되도록 보장하며, 관심사의 분리를 가능하게 합니다: LLM 은 증거를 제공하고, 격자 기반 하네스는 분석이 유계적이고 추적 가능하도록 보장합니다. 이 접근법은 프로그램 분석에서 에이전트 시스템을 위한 형식적 기반 기술 설계에 대한 향후 논의를 고무하는 것을 목표로 합니다.