💻 computer science

Misquoted No More: Securely Extracting F* Programs with IO

이 논문은 관계적 인용(relational quotation)과 검증된 구문 생성(verified syntax generation)을 결합하여, I/O 및 정제 타입(refinement types)을 포함하는 얕게 임베디드된(shallowly embedded) F* 프로그램을 깊게 임베디드된(deeply embedded) 계산 체계로 안전하게 추출함으로써, 임의의 적대적 연결(adversarial linking)에 대한 보안을 보장하기 위해 강건한 관계적 하이퍼속성 보존(Robust Relational Hyperproperty Preservation, RrHP)에 대한 기계 검증된 증명을 제공하는 프레임워크인 SEIO*를 소개한다.

원저자: Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter

게시일 2026-07-20

📖 5 분 읽기🧠 심층 분석

CC BY 4.0

원저자: Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

보이지 않는 안전망

당신이 완벽한 가상의 세계에서, 물리 법칙이 항상 당신의 예측대로만 움직이는 곳에서 멋진 자율주행 자동차를 설계한 마스터 설계자라고 상상해 보십시오. 당신은 자동차가 절대 충돌하지 않고, 멈춰야 할 때 멈추지 않으며, 항상 도로 규칙을 준수할 것임을 수학적으로 증명할 수 있는 아주 정밀한 특수 언어로 청사진을 작성했습니다. 이것이 컴퓨터 과학자들이 말하는 "형식 검증(formal verification)"입니다. 이는 마치 모든 볼트와 전선 하나하나를 100% 확신할 수 있는 꿈속에서 자동차를 만드는 것과 같습니다.

하지만 여기 함정이 있습니다. 그 꿈의 세계는 실제 도로 위에 존재하지 않습니다. 실제로 자동차를 운전하려면, 당신의 완벽한 청사진을 실제 엔진과 타이어가 이해할 수 있는 언어(예: C 또는 OCaml)로 번역해야 합니다. 이 번역 과정을 "추출(extraction)"이라고 합니다. 문제는 이 번역기(변환을 수행하는 컴퓨터 프로그램)가 완벽하지 않을 수 있다는 점입니다. 번역기가 볼트를 하나 빠뜨리거나, 전선을 꼬아버리거나, 규칙을 오해할 수도 있습니다. 만약 실제 세계의 자동차가 번역 과정에서의 실수로 만들어졌다면, 당신의 완벽한 안전 증명은 무용지물이 됩니다. 자동차는 서류상으로는 안전해 보일지 몰라도 현실에서는 충돌할 수 있습니다.

오랫동안 과학자들은 자동차를 만든 후 메카닉이 설계도와 일치하는지 검사하는 것처럼, 사후에 번역기의 작업 내용을 확인하여 이를 해결하려고 노력해 왔습니다. 하지만 이 논문은 더 똑똑한 방법을 소개합니다. 완성된 자동차를 단순히 검사하는 대신, 번역 과정 도중에 "안전 인증서"를 구축하여, 설령 번역기가 실수를 하더라도 실제 자동차가 꿈의 자동차와 수학적으로 완-벽한 쌍둥이임을 증명하는 것입니다. 그들은 이를 "안전한 추출(secure extraction)" 프레임워크라고 부르며, 이는 당신의 디지털 창조물이 외부의 검증되지 않은 코드와 섞이더라도 안전하게 유지되도록 설계되었습니다.

이 논문의 핵심 아이디어: "관계적 인용(Relational Quotation)"이라는 마술

이 논문의 저자인 컴퓨터 과학자 팀은 SEIO★(Secure Extraction of IO-star)라고 불리는 새로운 프레임워크를 구축했습니다. 그들의 목표는 고도로 보안이 강화된 소프트웨어(암호화 도구 등)를 작성하는 데 사용되는 언어인 **F★**의 "번역 문제"를 해결하는 것이었습니다. F★ 프로그램은 종종 "얕게 임베디드(shallowly embedded)"되어 있는데, 이는 추상적인 스타일로 작성되어 증명하기에는 매우 좋지만 컴퓨터가 실제 코드로 변환하기에는 어렵다는 것을 의미하는 세련된 표현입니다.

보통 이러한 추상적인 프로그램을 실제 코드로 바꿀 때, 무거운 작업을 수행하기 위해 "메타프로그램(다른 프로그램을 작성하는 프로그램)"을 사용해야 합니다. 기존 방식은 위험했습니다. 메타프로그램이 새로운 코드를 작성한 다음, 그 코드가 올바르다는 증명까지 쓰려고 시도하는 방식이었습니다. 만약 증명에 실패하면 처음부터 다시 시작해야 했습니다. 만약 증명을 통과하더라도, 메타프로그램이 증명을 쓰는 과정에서 버그를 몰래 심어놓지 않았다고 믿어야 했습니다. 이는 마치 학생에게 숙제를 채점하게 하고 그 학생이 부정행위를 하지 않기를 바라는 것과 같았습니다.

저자들의 획기적인 기술은 **관계적 인용(Relational Quotation)**이라 불리는 기법입니다. 메타프로그램에게 최종 코드와 증명을 모두 쓰라고 요구하는 대신, 훨씬 더 단순한 일을 시킵니다. 바로 **타입 유도(typing derivation)**를 작성하는 것입니다. 이것을 단계별 레시피 카드로 생각하십시오. "1단계: 이 재료를 가져온다. 2단계: 저 재료와 섞는다"라고 적힌 카드입니다. 이 레시피 카드는 실제로 요리를 하는 것이 아니라, 재료들이 특정 요리로 만들어질 수 있음을 증명할 뿐입니다.

여기 영리한 점이 있습니다:

메타프로그램 (레시피 작성자): 검증되지 않은 메타프로그램은 원래의 추상 프로그램을 보고 이 "레시피 카드(타입 유도)"를 생성합니다. 레시피 카드는 원래 프로그램의 구조를 그대로 따르기 때문에 작성하기가 매우 쉽습니다.
검사 (검사관): F★ 언어 자체가 이 레시피 카드를 검사합니다. "이 레시피가 원래의 프로그램을 정확히 설명하고 있는가?"라고 묻는 것입니다. 만약 메타프로그램이 실수를 하여 수프를 만들어야 할 것에 케이크 레시피를 썼다면 검사는 실패합니다. 하지만 레시피가 일치한다면, F★ 언어는 그 레시피가 유효하다는 것을 100% 확신합니다.
검증된 단계 (마스터 셰프): 레시피 카드가 검증되면, 수학적으로 완벽함이 증명된 다른 함수(완전히 검증된 "마스터 셰프")가 그 레시피를 받아 최종 요리(실제 코드)를 만듭니다. 레시피가 원래 프로그램과 일치한다는 것이 증명되었고, 셰프가 레시피에 적힌 대로 정확히 요리한다는 것이 증명되었으므로, 최종 요리는 원래의 프로그램과 완벽한 쌍둥이임이 보장됩니다.

이 접근 방식은 검증되지 않은 메타프로그램에 두어야 하는 "신뢰"를 최소화합니다. 우리는 메타프로그램이 레시피를 쓰는 것까지만 신뢰할 뿐, 요리를 하거나 숙제를 채점하는 것은 신뢰하지 않습니다. 가장 어려운 부분인 "음식이 안전한지 증명하는 일"은 검증된 마스터 셰프가 수행합니다.

"안전한 컴파일"이라는 초능력

이 논문은 단순히 코드가 올바른지 확인하는 데 그치지 않고, 한 걸음 더 나아가 그것이 보안상 안전한지를 보장합니다. 현실 세계에서 당신의 검증된 프로그램은 검증되지 않은 다른 코드(예: 해커가 작성했거나 다른 팀의 엉성한 코드)와 연결될 수 있습니다. 이러한 "적대적(adversarial)" 코드는 당신의 프로그램 규칙을 깨뜨리려 시도합니다.

저자들은 자신들의 SEIO★ 프레임워크가 **강건한 관계적 하이퍼속성 보존(Robust Relational Hyperproperty Preservation, RrHP)**이라는 매우 강력한 보안 규칙을 만족함을 증명합니다. 이를 이해하기 위해 당신의 검증된 프로그램을 요새라고 상상해 보십시오.

기존 방법들은 "요새의 벽이 튼튼하므로 안전하다"라고 말할 수 있습니다.
이 논문은 "해커가 뒷문으로 몰래 들어오려 하거나, 경비원을 속이려 하거나, 게임의 규칙을 바꾸려 해도, 당신의 요새는 여전히 당신이 설계한 대로 작동할 것이다"라고 말합니다.

저자들은 두 개의 "논리적 관계(logical relations)"를 사용하여 이를 증명하는데, 이는 마치 양방향 거울과 같습니다. 한 거울은 실제 코드가 추상적 코드가 할 수 있는 모든 것을 수행하는지 확인합니다. 다른 거울은 실제 코드가 추상적 코드가 할 수 없는 일을 하지 않는지 확인합니다. 이 두 가지를 모두 증명함으로써, 그들은 실제 코드가 아무리 엉망인 코드와 결합되더라도 원래의 코드를 완벽하고 안전한 그림자로서 유지함을 보여줍니다.

실제로 수행한 것 (그리고 하지 않은 것)

팀은 이 프레임워크를 전체적으로 F★ 언어 내부에서 구축했으며, 컴퓨터를 사용하여 증명의 모든 단계를 확인했습니다. 그들은 단순히 추측하거나 시뮬레이션한 것이 아니라, 수학적으로 증명했습니다.

작동하는 것: 그들은 파일 입출력(I/O, 파일 읽기 및 쓰기)을 처리하고 "정제 타입(refinement types, 예: '이 숫자는 양수여야 한다'와 같이 추가 규칙이 있는 타입)'을 사용하는 프로그램을 성공적으로 추출했습니다. 이러한 복잡한 기능들을 사용하더라도 추출이 안전하게 유지됨을 보여주었습니다.
여전히 진행 중인 과제: 논문은 현재 시스템이 재귀적(recursive) 함수(자기 자신을 호출하는 함수)나 완전한 "의존 타입(dependent types, 타입이 값에 의존하는 경우)"을 가장 자연스러운 방식으로 다루지는 못한다고 인정합니다. 재귀를 위해 이터레이터(반복문)를 사용하는 우회 방법을 사용해야 했습니다. 또한 메타프로그램이 특정 안전 검사를 어디에 배치할지 결정할 때 때때로 "추측"해야 하며, 이것이 다소 투박할 수 있다고 언급했습니다.
결론: 그들이 세상의 모든 프로그래밍 문제를 해결한 것은 아니지만, 완벽한 증명의 세계와 실제 코드의 혼란스러운 세계 사이에 훨씬 더 안전한 다리를 놓았습니다. 레시피 작성 단계와 요리 단계를 분리함으로써, 레시피 작성자를 완전히 신뢰하지 않고도 강력한 보안 보장을 얻을 수 있다는 것을 증명했습니다.

요약하자면, SEIO★는 프로그래머가 자신의 완벽하게 검증된 아이디어를 실제 세계의 소프트웨어로 변환할 때 수학적으로 보장된 안전망을 가질 수 있게 해주는 새로운 도구입니다. 이를 통해 번역 과정이 불완전하더라도 최종 결과물이 외부 세계의 혼돈으로부터 안전하도록 보장합니다.

기술 요약: Misquoted No More: IO를 통한 F★ 프로그램의 안전한 추출

1. 문제 정의

F★는 모나드(monad)를 사용하여 효과(예: I/O)를 표현하는 얕은 임베딩(shallowly embedded) 방식으로 작성된 프로그램을 작성하고 검증하는 데 널리 사용되는 증명 지향 언어입니다. 일단 검증되면, 이러한 프로그램들은 일반적으로 실행을 위해 OCamel이나 C와 같은 주류 언어로 추출됩니다. 그러나 현재 이 추출 과정은 검증되지 않았으며 신뢰 컴퓨팅 기반(TCB)의 일부를 구성합니다.

핵심 과제는 얕게 임베딩된 프로그램을 추출하는 데 필요한 "인용(quotation)" 단계에 있습니다. 인용은 얕게 임베딩된 프로그램(효과가 모나딕 타입으로 표현된 프로그램)을 대상 언어의 구체적인 표현인 깊게 임베딩된 구문 트리(deeply embedded syntax tree)로 변환하는 과정을 포함합니다. 이 인용 메타프로그램을 검증하는 것은 메타 이론의 기계적 구현이 필요하며, Rocq와 같은 성숙한 시스템에서도 인용을 검증하는 것은 여전히 미해결 과제로 남아 있습니다.

인증된 추출에 대한 기존 접근 방식은 메타프로그램이 추출된 코드와 정당성 증명을 모두 생성하고 이를 타입 체크하는 **번역 검증(translation validation)**에 크게 의존합니다. 이는 TCB를 줄여주기는 하지만, 메타프로그램이 유효한 증명을 생성해야 한다는 점에 여전히 의존하며, 이 과정에서 오류가 발생하거나 잘못된 증명이 생성될 수 있습니다. 또한, 기존 연구는 주로 정확성(기능적 동작의 보존)에 초점을 맞추고 있으며 보안성에는 집중하지 않습니다. 추출된 코드가 검증되지 않은 적대적 코드와 결합될 때, 원래 검증된 프로그램의 형식적 보증이 훼손되어 부적절성(unsoundness)이나 보안 침해가 발생할 수 있습니다.

2. 방법론

저자들은 I/O 및 세분화 타입(refinement types)을 가진 얕게 임베딩된 F★ 프로그램을 깊게 임베딩된 단순 타입 $\lambda$ -calculus( $\lambda_{io}$ )로 추출하기 위한 프레임워크인 **SEIO★**를 소개합니다. 이 방법론은 번역 검증에 대한 의존도를 최소화하기 위해 추출 과정을 두 가지 별개의 단계로 나눕니다.

단계 1: 관계적 인용 (번역 검증)
직접 대상 코드를 생성하는 대신, 이 프레임워크는 메타프로그램을 사용하여 원래의 얕게 임베딩된 프로그램에 대한 **타입 유도(typing derivation)**를 생성합니다.

관계적 타입 관계: 저자들은 추출되는 F★의 부분 집합(IO★라고 불림)을 특징짓는 타입 관계를 정의합니다. 이 관계는 구문적 표현이 아니라 "열린 F★ 값"(평가 환경에서 값으로의 함수)에 대해 작동하여, 얕은 임베딩에서의 자유 변수를 처리할 수 있게 합니다.
메타프로그램: 단순한 메타프로그램이 소스 프로그램의 구조를 순회하며 그에 대응하는 타입 유도를 구성합니다.
검증: 생성된 유도는 F★에 의해 타입 체크됩니다. 타입 관계가 의존 타입(dependent types)을 사용하기 때문에, 타입 체커는 해당 유도가 원래의 프로그램과 구문적 및 의미론적으로 일치하는지 검증합니다. 이 단계가 번역 검증에 의존하는 유일한 부분입니다.

단계 2: 검증된 구문 생성
유효한 타입 유도를 얻고 나면, 순수하고 검증된 F★ 함수가 유도를 재귀적으로 순회하여 대상 $\lambda_{io}$ 구문을 생성합니다.

타입 유도가 의존 타입을 통해 소스 프로그램과 구조적으로 연결되어 있기 때문에, 구문 생성 함수는 원래 프로그램과 의미론적으로 연관된 코드를 생성함이 보장됩니다.
이 단계는 F★ 내에서 완전히 검증되므로, 코드 생성 단계에서 번역 검증을 수행할 필요가 없습니다.

논리적 관계를 통한 보안 보증
보안을 증명하기 위해, 저자들은 소스(IO★) 언어와 대상( $\lambda_{io}$ ) 언어 사이의 두 가지 교차 언어 논리적 관계를 정의합니다.

대상-대상-소스(Target-to-Source): 대상 프로그램을 소스 프로그램과 연관시켜, 모든 대상 동작이 그에 대응하는 소스 동작을 가짐을 보장합니다.
소스-대상(Source-to-Target): 소스 프로그램을 대상 프로그램과 연관시켜, 모든 소스 동작이 그에 대응하는 대상 동작을 가짐을 보장합니다.

이 관계들은 I/O 연산이 이벤트(trace)를 생성하는 트레이스 생성 의미론(trace-producing semantics) 상에서 정의됩니다. 저자들은 SEIO★가 Abate 등의 연구[1]에서 정의된 가장 강력한 보안 컴파일 기준인 **강건한 관계적 하이퍼속성 보존(Robust Relational Hyperproperty Preservation, RrHP)**을 만족함을 증명합니다. RrHP는 임의의 적대적 컨텍스트에 대한 완전 추상화(full abstraction, 관찰 동등성 보존)와 트레이스 속성 및 하이퍼속성(예: 비간섭성)의 보존을 의미합니다.

세분화 타입 지원
이 프레임워크는 세분화 타입(타입에 대한 논리적 제약)을 지원하도록 확장되었습니다. F★는 SMT 솔버를 사용하여 명시적인 증명 항(proof term)을 생성하지 않고 세분화 증명을 해결하므로, 인용 과정 중에 메타프로그램은 원 가장 약한 전제 조건(weakest preconditions)을 처음부터 다시 계산하고 이를 재증명하여 타입 유도가 유효하게 유지되도록 해야 합니다.

3. 주요 기여

관계적 인용: 의존 타입을 사용하여 얕게 임베딩된 프로그램을 위한 타입 관계를 정의하는 새로운 번역 검증 기술입니다. 이를 통해 메타프로그램 자체를 검증할 필요 없이, 타입 유도를 생성하여 소스 프로그램과 일치함을 타입 체크로 확인할 수 있습니다.
SEIO★ 프레임워크: I/O 및 세분화 타입을 가진 F★ 프로그램을 깊게 임베딩된 $\lambda$ -calculus로 추출하는 완전한 추출 프레임워크입니다.
형식적 보안 컴파일: SEIO★가 임의의 연결된 적대적 코드에 대해 RrHP를 만족한다는 것을 F★에서 기계적으로 검증된 증명으로 보여줍니다. 이는 증명 지향 언어의 추출 프레임워크 중 이러한 강력한 보안 보증을 제공하는 첫 사례입니다.
교차 언어 논리적 관계: 트레이스 생성 의미론을 가진 얕게 임베딩된 언어와 표준 운영 의미론을 가진 깊게 임베딩된 언어 사이의 간극을 메우는 두 가지 비대칭적 논리적 관계의 정의 및 증명입니다.
세분화 타입 지원: 인용 중에 전제 조건을 재계산하고 재검증함으로써 세분화 타입을 처리하는 프레임워크 확장입니다.

4. 결과

저자들은 900개 이상의 최상위 정의를 포함하여 SEIO★를 F★로 구현했습니다.
파일 읽기, 에이전트 호출, 결과 검증을 수행하는 검증된 AI 에이전트용 검증 래퍼(validation wrapper)라는 실행 가능한 예제를 성공적으로 추출했습니다.
프레임워크는 $\lambda_{io}$ 언어로 직접 작성된 다양한 에이전트(정상 및 악성 모두)를 대상으로 테스트되었습니다.
기계 검증된 증명은 추출된 코드가 임의의 검증되지 않은 코드와 결합될 때에도 안전 속성을 보존함을 확인하며 RrHP를 만족합니다.
아티팩트에는 추출된 $\lambda_{io}$ 코드를 Peregrine 프레임워크와 Malfunction을 사용하여 OCaml로 컴파일하는 파이프라인이 포함되어 있어 실제 실행이 가능합니다.

5. 의의 및 주장

본 논문은 다음과 같은 두 가지 핵심적인 방식으로 기술적 진보를 이루었다고 주장합니다.

번역 검증의 최소화: 관계적 인용(typing derivation 생성)에 번역 검증을 국한시키고 이후의 구문 생성 단계를 검증함으로써, 기존의 인증된 추출 작업에 비해 검증되지 않은 메타프로그램에 대한 의존도를 낮추었습니다.
정확성을 넘어선 보안: 기능적 정확성에 초점을 맞춘 기존 연구와 달리, SEIO★는 형식적 보안 컴파일 보증을 제공합니다. 이는 검증된 F★ 프로그램이 임의의 검증되지 않았거나 적대적인 코드와 결합되더라도 보안 속성(예: 비간섭성 및 트레이스 속성)을 유지함을 보장합니다.

저자들은 본 연구가 현재의 기술 수준을 넘어섰다고 언급합니다. 현재의 기술은 증명 지향 언어로부터의 추출에 대해 이와 같이 강력한 보안 컴파일 보증을 제공하지 못하고 있습니다. 저자들은 일반 재귀 함수 및 완전한 의존 타입에 대한 현재의 지원 부족과 같은 한계를 인정하며, 이는 향후 연구 과제로 남겨두었습니다. 논문은 관계적 인용 메타프로그램이 검증되지 않았음에도 불구하고, 그 단순성과 이후 단계의 엄격한 검증 덕분에 전체적인 접근 방식이 견고함을 강조합니다.