Alignment Contracts for Agentic Security Systems

이 Isaac David, Marco Guarnieri, Arthur Gervais 의 논문 "Alignment Contracts for Agentic Security Systems"에 대한 상세한 기술 요약입니다.

1. 문제 제기

대규모 언어 모델 (LLM) 로 구동되어 보안 테스트 (예: 침투 테스트) 를 계획, 실행, 검증할 수 있는 자율 에이전트인 **에이전틱 보안 시스템 (Agentic Security Systems)**의 부상은 중대한 비대칭 제어 문제를 야기합니다.

• 딜레마: 이러한 에이전트는 승인된 범위 내에서 취약점 악용, 시스템 탐지 등 강력한 공격 능력을 유지해야 하는 동시에, 승인되지 않은 범위 (예: 승인되지 않은 대상 공격, 적대자에게 데이터 유출) 에서는 동일한 능력을 엄격히 거부해야 합니다.
• 기존 가드레일의 실패: 현재 안전 메커니즘 (예: 프롬프트 필터링, 의도 분류, 포괄적 거부) 은 다음과 같은 이유로 불충분합니다:
  1. 에이전트의 의도를 추론하는 데 의존하는 경우가 많으며, 이는 적대적 프롬프트 인젝션이나 모델 백도에어에 대해 신뢰할 수 없습니다.
  2. **관측 가능한 효과 (observable effects)**를 기반으로 승인된 행동과 승인되지 않은 행동 사이의 "경계"에 대한 공식적이고 1 급 (first-class) 정의가 부족합니다.
  3. 느슨한 정책으로 인해 행동 자체가 기술적으로 "허용"된다면, 에이전트가 손상되거나 조작되더라도 해로운 행동을 수행하지 않을 것을 보장할 수 없습니다.

핵심 과제는 LLM 의 내부 상태나 적대적 조작과 무관하게, 시스템이 모든 *실현된 효과 (네트워크 요청, 파일 접근, 프로세스 실행 등)*가 운영자가 정의한 제약 조건 내에 머무르도록 보장하는 **책임 경계 (responsibility boundary)**를 강제하는 것입니다.

2. 방법론: 정렬 계약 (Alignment Contracts)

저자들은 **관측 가능한 효과 추적 (observable effect traces)**에 대한 행동 제약을 명시하고 강제하기 위한 공식 프레임워크인 **정렬 계약 (Alignment Contracts)**을 제안합니다.

A. 핵심 개념

• 효과 알파벳 ($\Sigma$): 관측 가능한 효과 클래스의 유한 집합 (예: 네트워크용 NET, 파일 시스템용 FS, 프로세스 실행용 EXEC).
• 이벤트: 효과 클래스, 매개변수 (예: 목적지 IP, 메서드), 타임스탬프, 에이전트 ID 를 나타내는 튜플 $e = \langle \sigma, p, t, i \rangle$.
• 추적 (Trace): 이벤트의 유한 시퀀스.
• 계약 ($C$): 다음을 정의하는 튜플:
  • 범위 ($S$): 어떤 대상이 승인되었는지.
  • 허용/금지 효과 ($E_{allow}, E_{forbid}$): 허용되거나 금지된 특정 행동 클래스.
  • 예산 ($B$): 리소스 제한 (예: 최대 10,000 건의 요청).
  • 공개 정책 ($D$): 민감한 데이터 (취약점, 자격 증명 등) 가 흐를 수 있는 곳.
  • 비용 및 흐름: 리소스 및 데이터 추출에 대한 회계 함수.

B. 강제 메커니즘

시스템은 효과 관측 가능성 가정 (EOA) 하에 작동하는 **참조 모니터 (Reference Monitor)**에 의존합니다:

1. 중재: 모든 외부 효과는 실행 전에 중재 계층 (예: 타입 지정 도구 래퍼, HTTP 프록시, 커널 후크) 을 통과해야 합니다.
2. 허용성 확인: 제안된 모든 이벤트 $e$와 현재 추적 접두사 $\tau$에 대해 모니터가 $Adm(e, \tau, C)$가 성립하는지 확인합니다. 여기에는 다음 검증이 포함됩니다:
   • 대상이 범위 내에 있는지.
   • 효과가 허용되고 금지되지 않았는지.
   • 예산이 초과되지 않았는지.
   • 공개 흐름이 승인되었는지.
3. 행동: 허용되면 이벤트가 허용되고, 그렇지 않으면 거부됩니다. 모니터는 LLM 의 내부 추론을 무시하고 관측 가능한 데이터만으로 작동합니다.

C. 공식적 기초

• 안전 속성: 계약 만족은 유한 추적에 대한 **안전 속성 (safety property)**으로 정의됩니다. 계약이 위반되면 위반을 증명하는 유한한 "나쁜 접두사 (bad prefix)"가 존재합니다.
• 기계화: 핵심 정리는 형식적 증명 도우미인 Lean 4를 사용하여 검증되어 프레임워크의 논리적 타당성을 보장합니다.

3. 주요 기여

1. 공식 모델: 추적 기반 의미론을 가진 유한 효과 알파벳 위의 튜플로 정의된 정렬 계약. 논문은 위반이 유한 시간 내에 감지되도록 보장하는 **유한-나쁜-접두사 증인 속성 (Finite-Bad-Prefix Witness Property)**을 증명합니다.
2. 강제 타당성: EOA 하에서 저자들은 효과가 완전히 중재된다면 적대적, 프롬프트 인젝션, 또는 백도어된 에이전트라 할지라도 어떤 에이전트라도 계약 만족 추적을 생성함을 증명합니다. 이는 신뢰를 신뢰할 수 없는 LLM 에서 감사 가능한 작은 강제 장벽으로 이동시킵니다.
3. 계약 대수:
   • 정제 ($C' \sqsubseteq C$): 타당성을 유지하면서 더 엄격한 계약 (더 좁은 범위, 더 엄격한 예산) 을 생성하는 메커니즘.
   • 일방향 조합: 조직 정책과 참여 범위를 병합하는 등 계약을 결합하기 위한 규칙과 증명된 타당성 보장.
   • 결정 가능성: 논문은 허용성 확인이 결정 가능하며 계산적으로 효율적임을 입증합니다 (캐싱을 사용한 $O(|Res|)$ 온라인).
4. 적응 스키마: 서브 에이전트 생성, 도구 교체 등 동적 시스템 변경을 처리하기 위한 "계약 보존" 적응 규칙을 정의하는 프레임워크.
5. 불가능성 결과: 논문은 이 접근법의 한계를 공식적으로 규정합니다:
   • 불결정성: 튜링 완전 언어의 경우 도구가 언제나 금지된 효과를 시도하는지 여부를 사전에 정적으로 분석하는 것은 결정 불가능합니다.
   • 우회 한계: 도구가 중재 계층을 우회하는 경우 (예: 커널 모듈 또는 사이드 채널을 통해), 타당성 보장은 무너집니다.
   • 관측 가능성 경계: 은밀한 채널 (페이로드 스테가노그래피, 타이밍 채널) 과 모델링되지 않은 효과는 정리의 범위를 벗어납니다.

4. 결과 및 평가

• 이론적 보장: Lean 4 아티팩트는 참조 모니터가 올바르게 구현되고 EOA 가 성립하면 시스템이 타당함을 검증합니다. LLM 의 행동은 보장과 무관하며, 실현된 효과만이 중요합니다.
• 사례 연구 (웹 침투 테스트): 프레임워크는 웹 침투 테스트 시나리오에 적용되었습니다. 다음과 같은 제약을 성공적으로 모델링했습니다:
  • "*.example.com 에 대한 HTTP GET/HEAD 만 허용."
  • "파일 시스템 작업 금지."
  • "최대 10,000 건의 요청."
  • "대시보드에만 보고서 전송."
  • 모니터는 에이전트가 "프롬프트 인젝션"을 통해 evil.com 으로 데이터를 유출하거나 승인되지 않은 도메인에 접근하려는 시도를 정확하게 차단했습니다.
• 복잡도: 핵심 허용성 확인은 실제 배포에서 이벤트당 상수 시간으로 수행됨이 입증되었습니다 (작은 고정 리소스 집합 가정). 이는 런타임 강제에 적합합니다.

5. 중요성

이 논문은 AI 에이전트 보안의 패러다임 전환을 나타냅니다:

• 의도에서 효과로: LLM 의 내부 의도를 "정렬"하려는 시도 (이는 어렵고 취약함) 에서 관측 가능한 효과에 대한 제약 강제 (검증 가능함) 로 전환합니다.
• 공식적 신뢰: 기계화된 증명을 사용하여 중재 계층이 안전하다면 에이전트가 계약을 위반할 수 없음을 수학적으로 엄밀하게 보장합니다. 이는 신뢰 컴퓨팅 기반 (TCB) 을 모니터와 중재 경계로 축소하여 LLM 을 제외합니다.
• 실용적 적용성: 이 프레임워크는 실제 오펜시브 보안 워크플로우를 위해 설계되었으며, 에이전트가 부수적 피해나 데이터 유출을 일으킬까 봐 두려워하지 않고 강력한 자율 에이전트를 안전하게 배포할 수 있는 방법을 제공합니다.
• 명확한 경계: 시스템이 보장할 수 없는 것 (예: 페이로드 내용 검사, 타이밍 채널) 을 명시적으로 밝힘으로써 기술에 대한 과도한 의존을 방지하고, 향후 엔지니어링 노력이 이러한 특정 격차를 해소하는 방향으로 이끌도록 합니다.

요약하자면, **정렬 계약 (Alignment Contracts)**은 에이전틱 보안 시스템이 승인된 경계 내에서 엄격하게 작동하도록 보장하는 최초의 공식적이고 결정 가능하며 기계적으로 검증된 프레임워크를 제공하여, LLM 추론의 "블랙박스"를 강제 가능한 효과 제약의 "화이트박스"로 변환합니다.