기술 요약: 당신이 알고 있었을 것이라 가정하며: 에이전트형 AI를 이용한 흐름 정책용 인식론적 의미론의 수정

1. 문제 정의

정보 흐름에 관한 고수준 보안 요구사항, 특히 선택적 다운그레이딩(기밀 해제)을 포함하는 요구사항은 정밀하게 정형화하기가 매우 어렵다. 인식론적 논리(epistemic logic)가 보안성(특정 권한 수준의 관찰자가 알 수 있도록 허용된 것)을 정의하기 위한 유망한 프레임워크로 등장했지만, 표현력이 풍부한 흐름 정책을 위한 견고하고 일반적인 프레임워크는 여전히 찾아보기 힘들다.

이전 연구인 CN(Naumann et al., CSF 2018)은 반응형 프로그램 모델을 위한 통합 프레임워크를 제공하려고 시도했다. CN에서 정책은 코드 내의 assume 문을 통해 표현되었으며, 파생된 릴리스 정책(release policy)은 오직 입력 스트림의 관점에서만 표현되었다. 그러나 CN의 정형화에는 컨퍼런스 발표 중에 발표된 중대한 결함이 있었다. 원래의 릴리스 정책 정의와 안전성이 보안성을 함의한다는 이후의 증명은 불충분하고 부정확했다. 또한, 기존의 기계 검증 적응 방식(예: 동시성 C 프로그램을 위한 Murray et al.)은 인식론적 추론에 필요한 다중 실행의 정렬(alignment) 문제를 사소하게 만드는 상수 시간 실행(constant-time execution)과 같은 강력한 속성에 의존하는 경우가 많다.

핵심 과제는 다음과 같은 사항을 수행하는 교정된, 기계 검증된 정형화를 제공하는 것이다:

1. 상태 의존적 다운그레이딩을 올바르게 처리하도록 인식론적 의미론을 수정한다.
2. 코드 주석으로부터 파생된 릴리스 정책의 의미론을 명시적으로 정의한다.
3. 프로그램 지향적 속성인 **안전성(safety)**이 인식론적 **보안성(security)**을 함의함을 증명한다.

2. 방법론

저자는 Rocq 증명 보조기(구 Coq)를 사용하는 형식 검증 접근 방식을 채택한다. 방법론은 다음과 같다:

• 프로그램 모델: 특정 보안 수준을 가진 입력 핸들러를 포함하는 작은 명령형 반응형 언어이다. 프로그램은 입력 스트림을 소비하고 출력을 생성한다.
• 주석(Annotations): 프레임워크는 관계적 단언(relational assertions, assert)과 가정(assumptions, assume)을 활용하여 정보 흐름 요구사항을 지정한다. 이러한 주석은 기본 비간섭(non-interference) 정책에서 벗어나는 조건부 흐름을 허용한다.
• 인식론적 의미론: 보안은 관찰자의 지식 관점에서 정의된다. 레벨 $\ell$의 관찰자는 자신의 가시적 관측값(레벨 $\ell' \sqsubseteq \ell$에서의 입력 및 출력)과 일치하는 가능한 입력 이력(input histories)의 집합을 안다.
• 릴리스 정책 ($RP_\ell$): 코드의 assume 문으로부터 파생되며, 관찰자가 배울 수 있도록 허용된 입력 리스트의 집합으로 정의된다. 이 정책은 "주요(major)" 사전 실행(실제 실행)과 "부차적(minor)" 사전 실행(서로 다른 입력을 가진 가능한 실행들) 사이의 **정렬(alignments)**을 통해 해석된다.
• 안전성 조건: 주요 실행을 가능한 모든 부차적 실행과 비교할 때 "실패"(단언 실패, 정렬 실패)의 부재 또는 특정 "피아트(fiats)"(가정 피아트, 발산 피아트)의 존재로 정의되는 프로그램 지향적 속성이다.
• 에이전트형 AI 지원: 정형화 과정은 Claude Code라는 에이전트형 AI 코딩 어시스턴트의 도움을 받아 개발되었다. AI는 LaTeX 정의를 Rocq 사양으로 번역하고 증명 구축을 돕도록 유도되었으나, 논리적 오류를 수정하고, 정의를 정교화하며, 증명 전략을 관리하기 위해 상당한 인간의 큐레이션이 필요했다.

3. 주요 기여

A. 교정된 인식론적 의미론

본 논문은 인식론적 의미론의 수정된 정형화를 제시한다. 주요 기술적 수정 사항은 다음과 같다:

• 릴리스 정책 정의: 릴리스 정책 $RP_\ell(gs)$의 정의를 관측된 이벤트 트레이스뿐만 아니라 사전 실행(finite execution prefixes)에 대한 술어로 교정하였다. 이는 특정 주석 지점에서 주요 사전 실행과 부차적 사전 실행을 정렬시키는 **반정합성(semi-conformance)**을 통해 정의된다.
• 진전 미민감 보안(Progress-Insensitive Security): 프레임십워크는 진전 미민감 보안 정의를 채택한다. 발산(divergence)을 처리하기 위해 진전 지식(progress knowledge, $k_\ell^\to$) 개념을 활용하며, 이를 통해 발산 자체가 숨겨진 입력에 대한 정보를 누설하지 않는 한 보안 보장이 유지되도록 한다.
• 잘 규정된 프로그램: 저자는 "보일러플레이트 주석"(핸들러 시작 시의 가정 및 출력 전의 단언)을 도입하여, 관찰 가능한 동작을 변경하지 않으면서 기본 정책을 효율적으로 인코딩하고 정형화를 간소화한다.

B. 안전성은 보안성을 함의한다

중심적인 이론적 결과는 정리 2이다: 모든 레벨 $\ell$에 대하여, $\ell$에 대해 안전한 모든 사전 실행은 $\ell$에 대해 보안하다.

• 안전성은 단언/정렬 실패의 부재와 임의의 대안 입력 리스트에 대한 유효한 피아트(가정 또는 발산)의 존재로 정의된다.
• 증명은 프로그램이 안전하다면, 관찰자가 배우는 입력의 집합($k_\ell$)이 릴리스 정책($RP_\ell$)과 진전 지식의 교집합 내에 존재함을 보여준다.
• 이 결과는 복잡한 모든 실행의 런타임 모니터링 대신 프로그램 주석의 관계적 검증을 통해 보안을 강제하는 접근 방식의 타당성을 입증한다.

C. 기계 검증된 확인

수정된 정의와 주요 정리를 포함한 전체 개발 과정이 Rocque에서 기계 검증되었다. 이는 CN 논문의 수정 사항이 근본적으로 건전함을 확인해 줄 뿐만 아니라, 원래의 인간 작성 스케치에서 놓쳤던 증명의 미묘한 세부 사항들을 밝혀냈다.

D. 에이전트형 AI 사용 경험

본 논문은 정형화 과정에서 에이전트형 AI(Claude Code)의 사용을 기록한다. 저자는 AI가 비사소한 인프라와 일상적인 증명을 생성할 수 있었지만, 다음과 같은 작업에서 인간의 감독이 필요했음을 언급한다:

• 결함이 있는 정리(lemma)의 정형화 수정 (예: Lemma 3).
• "발산 피아트(divergence fiat)" 정의의 논리적 간극 식별 및 수정.
• equality 대신 prefix를 사용하도록 지식($k_\ell$)의 정의를 정교화 (이는 AI가 발견한 반례에 의해 필요해진 변화임).
• AI가 불필요하게 가정을 강화하거나 불필요한 결정 가능성 가설을 도입하는 것을 방지.

4. 결과

• 형식적 정확성: 기계 검증된 증명은 수정된 안전성 조건이 반응형 프로그램 모델에 대해 인식론적 보안 속성을 올바르게 함의함을 확인한다.
• CN의 결함 해결: 실행의 정렬 및 릴리스 정책의 정의와 관련된 2018년 CN 증명의 구체적인 결함들이 해결되었다.
• AI 지원 정형화의 실현 가능성: 본 연구는 인간 전문가가 도구를 능동적으로 가이드하고, 논리적 오류를 수정하며, 전체적인 증명 구조를 관리할 때, 에이전트형 AI가 복잡한 수학적 사양을 기계 검증된 증명으로 번역하는 데 효과적으로 기여할 수 있음을 보여준다.

5. 의의 및 주장

본 논문은 다음과 같이 겸손하지만 중요한 기여를 주장한다:

• 통합 프레임워크: 인식론적 논리와 관계적 주석을 사용하여 표현력이 풍부한 흐름 정책을 표현하고 검증하기 위한 교정된 일반 프레임워크를 제공한다.
• 실용적 검증: 안전성(런타임 모니터링과 귀납적 증명에 용이한 속성)이 보안성을 함의함을 보여줌으로써, 본 연구는 고수준 정책 사양과 실행 가능한 프로그램 속성 사이의 간극을 메운다.
• 기계 검증의 신뢰성: 본 연구는 이상적인 환경에서의 이론적 발전에서도 기계 검증이 왜 필요한지를 강조한다. 이는 인간의 검토가 놓칠 수 있는 미묘한 오류를 드러내기 때문이다.
• 형식 방법론에서의 AI: 본 연구는 에이전트형 AI를 활용한 상당한 규모의 형식적 개발에 대한 구체적인 사례 연구를 제공하며, 효율성 증대의 잠재력과 논리적 엄밀성을 보장하기 위한 인간 전문 지식의 결정적 필요성을 동시에 강조한다.

저자는 안전성 조건의 구성적 증명 규칙(compositional proof rules) 개발이 여전히 미해결 과제로 남아 있으며, 현재의 작업은 기초적인 의미론과 주요 함의 정리에 집중하고 있음을 명시한다. 본 논문은 기계 검증된 정형화 분야의 선구적인 역할을 한 David Basin에게 헌정되었다.