논문 요약: Agentic AI 기술에 대한 형식적 분석 및 공급망 보안 (Formal Analysis and Supply Chain Security for Agentic AI Skills)

이 논문은 2026 년 현재 급격히 확산되고 있는 '에이전트 기술 (Agentic AI Skills)' 생태계의 심각한 공급망 보안 취약점을 해결하기 위해 제안된 SkillFortify라는 형식적 분석 프레임워크를 소개합니다. 저자는 기존 도구들이 휴리스틱 (heuristic) 에 의존하여 위험을 완전히 차단하지 못하는 한계를 지적하고, 수학적 보장이 가능한 최초의 분석 도구를 제시합니다.

1. 문제 정의 (Problem)

• 배경: OpenClaw(228,000 개의 GitHub 스타) 와 Anthropic Agent Skills(75,600 개) 와 같은 에이전트 기술 생태계가 급성장하면서, 개발자들은 제 3 자 기술을 암묵적인 신뢰로 설치하고 실행하고 있습니다.
• 위협: 2026 년 1 월 'ClawHavoc'캠페인에서 1,200 개 이상의 악성 기술이 OpenClaw 마켓플레이스에 침투하여 AMOS 자격 증명 도난 도구를 배포했습니다. 또한, MalTool 은 LLM 기반 에이전트를 대상으로 한 6,487 개의 악성 도구를 발견했으나, 기존 바이러스 백신 (VirusTotal 등) 은 이를 대부분 탐지하지 못했습니다.
• 현재의 한계: 기존 보안 도구 (Snyk agent-scan, Cisco skill-scanner 등) 는 패턴 매칭이나 휴리스틱 규칙에 의존합니다. 이들은 "알려진 나쁜 패턴을 탐지했는가?"에 답할 뿐, "이 기술이 선언된 권한을 초과하여 자원에 접근할 수 있는가?"를 수학적으로 증명하지 못합니다. Cisco 의 문서조차 "결과가 없다는 것이 위험이 없다는 뜻은 아니다"라고 명시하고 있습니다.

2. 방법론 (Methodology)

SkillFortify 는 40 년간의 형식적 방법론 (Formal Methods) 연구를 에이전트 기술 보안에 적용하여 다음과 같은 4 가지 핵심 기법을 통합합니다.

1. DY-Skill 공격자 모델 (Formal Threat Model):

   • 기존 Dolev-Yao 공격자 모델을 에이전트 기술 공급망 (설치, 로드, 구성, 실행, 영속화) 의 5 단계 수명 주기에 맞게 적응화했습니다.
   • 공격자가 메시지를 가로채고, 주입하고, 변조하며, 새로운 기술을 합성 (Forge) 할 수 있음을 정의하고, 이 모델이 상징적 공격자 중 최대 (Maximal) 라는 것을 증명했습니다.

2. 형식적 정적 분석 (Sound Static Analysis):

   • **추상 해석 (Abstract Interpretation)**을 기반으로 한 정적 분석 프레임워크를 구축했습니다.
   • 4 가지 권한 레벨 ({NONE, READ, WRITE, ADMIN}) 로 구성된 격자 (Lattice) 구조를 사용하여 기술의 실제 실행이 선언된 권한을 초과하지 않음을 수학적으로 보장 (Soundness) 합니다.
   • Galois 연결 (Galois connection) 을 통해 추상 도메인이 구체적 실행을 과대 평가 (Over-approximation) 하도록 설계하여, 위양성 (False Positive) 은 발생할 수 있으나 위음성 (False Negative, 악성 코드를 놓치는 경우) 은 발생하지 않음을 보장합니다.

3. 권한 기반 샌드박싱 (Capability-Based Sandboxing):

   • Object-Capability 모델에 기반하여, 기술이 실행 시 선언된 권한 집합의 전이 폐포 (Transitive Closure) 를 초과할 수 없음을 증명했습니다.
   • 위임 (Delegation) 과정에서 권한이 증폭되지 않도록 보장합니다.

4. SAT 기반 의존성 해결 및 신뢰 점수 대수:

   • Agent Dependency Graph (ADG): 기술 간 의존성, 버전 제약, 충돌, 그리고 권한 제약을 포함하는 그래프를 정의했습니다.
   • SAT 해결: 의존성 해결 문제를 SAT(Propositional Satisfiability) 문제로 인코딩하여, 보안 정책 (권한) 을 위반하지 않는 설치 계획을 자동으로 생성하고 결정적 (Deterministic) 인 Lockfile 을 생성합니다.
   • 신뢰 점수 대수: 출처, 행동 분석, 커뮤니티, 역사적 데이터를 기반으로 신뢰 점수를 계산하며, 의존성 체인을 따라 신뢰가 전파되고 유지되지 않는 기술은 지수적으로 감소하도록 설계했습니다.

3. 주요 기여 (Key Contributions)

1. DY-Skill 공격자 모델: 에이전트 기술 공급망에 대한 최초의 형식적 위협 모델 및 최대성 증명.
2. 정적 분석 프레임워크: 추상 해석을 기반으로 한 정밀한 정적 분석 및 안전성 (Soundness) 증명.
3. 권한 기반 샌드박싱: 실행 시 권한 증폭을 방지하는 격리 증명.
4. Agent Dependency Graph (ADG): SAT 기반 해결 알고리즘과 보안 경계가 포함된 Lockfile 의미론.
5. 신뢰 점수 대수: 증분적 증거에 따라 신뢰 점수가 감소하지 않는 (Monotonicity) 형식적 속성을 가진 신뢰 시스템.
6. SkillFortifyBench: 540 개의 기술 (270 개 악성, 270 개 정상) 로 구성된 벤치마크 및 평가.

4. 실험 결과 (Results)

SkillFortify 는 540 개의 기술로 구성된 벤치마크에서 다음과 같은 성과를 거두었습니다.

• 탐지 정확도: F1 점수 96.95% (95% 신뢰 구간: [95.1%, 98.4%]).
• 정밀도 (Precision): 100% (거짓 양성 0 개). 이는 개발자의 경보 피로 (Alert Fatigue) 를 방지하고 CI/CD 파이프라인에 통합하기에 이상적입니다.
• 재현율 (Recall): 94.07% (16 개의 위음성 발생). 주로 관계형 공격 (타입스쿼팅, 의존성 혼동) 이나 복잡한 MCP 구성에서 발생했습니다.
• 성능:
  • 1,000 개의 노드를 가진 의존성 그래프를 100ms 미만 (약 92ms) 에 해결.
  • 540 개의 기술을 포함한 전체 스캔을 1.378 초 내에 완료.
• 결정론적 Lockfile: 동일한 입력에 대해 항상 비트 단위로 동일한 JSON 출력을 생성하여 무결성을 보장합니다.

5. 의의 및 결론 (Significance)

• 패러다임의 전환: 에이전트 기술 보안이 휴리스틱 패턴 매칭에서 수학적 보장이 있는 형식적 분석으로 전환되어야 함을 입증했습니다.
• 실용성: 이론적 프레임워크를 넘어, 오픈소스 도구 (SkillFortify) 로 구현되어 실제 CI/CD 파이프라인, IDE 플러그인, 엔터프라이즈 규정 준수 (SBoM 생성) 에 즉시 적용 가능합니다.
• 규제 대응: EU AI Act 및 NIST AI 위험 관리 프레임워크와 같은 규제 요구사항을 충족하는 구체적인 메커니즘 (ASBoM, 신뢰 점수, 권한 검증) 을 제공합니다.
• 미래 지향성: 정적 분석의 한계 (동적 실행 시나리오) 를 인정하면서도, 이를 보완할 런타임 샌드박싱 및 신뢰 프로토콜에 대한 청사진을 제시했습니다.

이 논문은 에이전트 AI 생태계가 개발자 실험 단계에서 엔터프라이즈 생산 환경으로 확장됨에 따라, "설치하고 신뢰 (Install and Trust)"하는 방식은 더 이상 유효하지 않으며, **형식적 검증과 심층 방어 (Defense-in-Depth)**가 필수적임을 강력하게 주장합니다.