💻 computer science

Security Engineering in IIIf, Part II -- Shadowing the IIIf

이 논문은 모건(Morgan)의 "섀도우(Shadow)" 개념을 도입하여 정보 흐름 보안(Information Flow Security)을 정형화함으로써 Isabelle Insider and Infrastructure 프레임워크(IIIf)의 보안 공학을 확장하고, 이를 통해 정제 역설(refinement paradox)을 해결하며 비행 레이더 시스템 예시를 통해 입증된 안전한 정제의 조건들을 확립한다.

원저자: Florian Kammüller

게시일 2026-06-30

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Florian Kammüller

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

개요: "플라이트 레이더(Flight Radar)" 문제

당신이 스마트폰으로 공개된 항공기 위치 추적 앱을 보고 있다고 상상해 보세요. 지도 위에서 비행기들이 움직이는 것이 보입니다. 보통 이런 것은 해롭지 않습니다. 하지만 만약 비행기가 갑자기 특정 구역 주변에서 이상하게 지그재그로 우회한다면 어떻게 될까요?

현실 세계에서 비행기는 단순히 재미를 위해 직선으로만 비행하지 않습니다. 만약 비행기가 비밀 군사 기지나 VIP의 위치 주변을 갑자기 피해서 비행한다면, 그 "우회하는 움직임"은 하나의 단서가 됩니다. 앱에는 비밀 기지가 표시되지 않더라도, 비행기의 이동 패턴을 통해 당신은 위험 구역이 정확히 어디인지 알 수 있게 됩니다.

이것이 바로 이 논문이 다루는 문제입니다: 시스템의 행동에서 발생하는 부수적인 효과를 통해 어떻게 비밀 정보가 "유출"되는 것을 막을 것인가?

등장인물과 배경

시스템 (IIIf): 이것은 디지털 도시를 위한 거대하고 매우 엄격한 규칙책이라고 생각하면 됩니다. 시스템은 누가 어디에 있는지, 어떤 규칙을 따르는지, 그리고 사물이 어떻게 움직이는지를 추적합니다. 저자들은 이 규칙책을 매우 엄격하게 작성하기 위해 "Isabelle"이라는 강력한 컴퓨터 도구를 사용했으며, 이를 통해 컴퓨터가 그 규칙이 올바르다는 것을 증명할 수 있도록 했습니다.
공격자 (Eve): Eve는 시스템이 대중에게 보여주는 모든 것(예: 지도상의 비행기 위치)을 볼 수 있지만, 비밀(예: 비밀 기지의 위치)은 알 수 없도록 되어 있는 참견하기 좋아하는 관찰자입니다.
비밀 (Critical Location): 이것은 시스템이 보호하려고 하는 "금지 구역"입니다.

문제: "정제 역설 (Refinement Paradox)"

저자들은 정제 역설이라 불리는 까다로운 상황을 설명합니다.

당신이 보안이 철저한 시스템(추상적 버전, Abstract version)을 설계했다고 가정해 봅시다. 당신은 Eve가 비밀을 알아낼 수 없음을 컴퓨터로 증명했습니다. 아주 좋습니다!
그런데 시스템을 더 개선하거나 더 상세하게 만들기로 결정합니다(정제된 버전, Refined version). 예를 들어, 비행기의 속도를 보여주는 것과 같은 새로운 기능을 추가할 수 있습니다.

역설: 설령 당신의 새로운 기능이 무해해 보일지라도, 그것이 의도치 않게 새로운 "유출"을 만들어낼 수 있습니다.

비유: 당신이 금고 안에 비밀 쪽지를 숨기고 있다고 상상해 보세요. 당신은 금고가 안전하다는 것을 증명했습니다. 그러다 금고에 작고 장식적인 손잡이를 하나 달기로 합니다. 당신은 잠금장치를 바꾸지 않았지만, 이제 금고를 흔들면 내부의 쪽지 위치에 따라 손잡이가 다르게 달그락거립니다. 갑자기 그 손잡이가 비밀을 폭로하게 된 것입니다.

논문의 예시에서, 만약 시스템이 비행기의 실제(숨겨진) 경로 대신 공개된 경로를 기반으로 속도를 계산한다면, 비행기가 비밀 구역을 피할 때마다 속도 수치가 이상하게 나타날 것입니다. Eve는 그 이상한 속도를 보고 비밀 구역이 어디인지 즉시 알게 됩니다. 시스템은 "더 상세해졌지만", 보안성은 오히려 낮아졌습니다.

해결책: "섀도우 (Shadow, 그림자)"

이를 해결하기 위해 저자들은 수학자 모건(Morgan)에게서 영감을 받은 **섀도우(Shadow)**라는 개념을 도입합니다.

섀도우란 무엇인가?
섀도우를 비밀 정보에 대한 **"가능성의 주머니 (Bag of Possibilities)"**라고 생각하세요.

시작 단계에서 섀도우는 비밀이 존재할 수 있는 모든 가능한 위치를 담고 있는 거대한 주머니입니다. 공격자는 완전히 혼란스러운 상태이며, 비밀이 어디에 있는지 전혀 알 수 없습니다.
시스템이 작동하는 동안, 섀도우는 계속 커다란 상태를 유지해야 합니다. 만약 섀도우가 줄어든다면, 이는 공격자가 새로운 정보를 알아냈음을 의미합니다.

목표: 보안이 확보된 시스템이란 섀도우가 결코 줄어들지 않는 시스템입니다. 섀도우가 동일한 크기를 유지한다면, 공격자의 무지는 보존됩니다. 그들은 여전히 처음과 다름없이 아무것도 모르는 상태입니다.

그들이 플라이트 레이더를 고친 방법

저자들은 이 "섀도우" 개념을 자신들의 플라이트 레이더 시스템에 적용했습니다.

유출: 원래의 보안이 취약한 버전에서는 비행기의 움직임이 비밀 위치를 드러냈습니다. 비행기의 경로를 바탕으로 특정 위치를 배제할 수 있게 되면서 섀도우가 줄어들었습니다.
해결책: 그들은 "숨기기" 메커니즘을 추가했습니다. 비행기가 비밀 구역을 피해야 할 때, 시스템은 실제 경로를 비밀 상자(critpos 구성 요소)에 기록하지만, 공개 지도에는 마치 비밀 구역을 통과하여 직선으로 비행한 것처럼 표시합니다.
결과: 공개 지도가 정상적으로 보이기 때문에, 공격자의 "가능성의 주머니"(섀도우)는 결코 작아지지 않습니다. 공격자는 여전히 비밀 구역이 어디든 있을 수 있다고 생각하게 됩니다.

"마법 같은" 증명

이 논문은 두 가지 주요 작업을 수행합니다.

동등성 (Equivalence): 그들은 "섀도우가 줄어들지 않는 것"이 "비간섭성(Non-Interference, 비밀이 공개적으로 보이는 것에 영향을 주지 않는다는 뜻의 전문 용어)"과 정확히 같다는 것을 증명했습니다. 이는 "주머니가 가득 차 있는 것"이 "아무도 사과를 훔치지 않은 것"과 같다는 것을 증명하는 것과 같습니다.
업그레이드를 위한 안전 규칙: 그들은 미래의 업그레이드(정제)가 보안을 유지할 수 있는지 확인하는 규칙(정리 2)을 만들었습니다.
- 규칙: 새로운 기능을 추가할 때, 그 기능이 비밀에 의존하는지 확인해야 합니다. 만약 새 기능이 비밀에 의존한다면, 섀도우는 줄어들 것이고, 그 업그레이드는 안전하지 않습니다.
- 핵심: 만약 새 기능이 비밀과 완전히 독립적이라면, 섀도우는 큰 상태를 유지하며, 업그레이드는 안전합니다.

요약

이 논문은 시스템을 더 상세하게 만드는 과정에서 의도치 않게 비밀이 유출되는 문제를 해결합니다. 그들은 공격자가 알고 있는 것을 추적하기 위해 "섀도우"(가능성의 주머니)를 사용합니다. 섀도우가 가득 차 있다면 시스템은 안전합니다. 그들은 새로운 기능을 추가할 때 특정한 규칙을 따른다면, 비밀을 실수로 흘리지 않고도 시스템을 업그레이드할 수 있다는 것을 증명했습니다.

요약하자면: 그들은 시스템에 새로운 기능을 추가할 때마다 그 기능이 실수로 대중에게 비밀을 속삭이지 않도록 체크하는 수학적인 "보안 요원"을 만든 것입니다.

기술 요약: Isabelle Insider 및 인프라 프레임워크의 섀도잉(Shadowing)

문제 정의
Isabelle Insider 및 인프라 프레임워크(IIIf)는 정제-리스크(Refinement-Risk, RR) 사이클을 활용하여 인간 행위자, 정책, 물리적/논리적 구성 요소를 포함하는 시스템의 보안 엔지니어링을 위한 형식적 기초를 제공한다. IIIf는 표준 안전 속성(예: 도달 가능성)에 대해 추적 기반 정제(trace-based refinement)와 속성 보존을 지원하지만, 정보 흐름 제어(Information Flow Control, IFC)와 관련해서는 결정적인 한계에 직면해 있다. 구체적으로, 고보안(비밀) 상태가 저보안(공개) 관측치에 영향을 미치지 않음을 보장하는 비간섭성(Noninterference, NI) 속성은 정제 과정에서 일반적으로 보존되지 않는다. "정제 역설(refinement paradox)"이라고 알려진 이 현상은, NI를 만족하는 명세가 암시적 흐름(implicit flows)을 통해 정보를 유출하는 정제된 구현체를 생성할 수 있음을 의미한다. IIIf 내의 기존 모델 체킹 접근 방식은 이러한 추적 집합(trace-set) 속성을 검증하기에 불충분하며, 이에 따라 보안 정제를 특징짓고 보장하기 위한 새로운 방법론이 필요하다.

방법론
정제 역설을 해결하기 위해, 본 논문은 Morgan의 "섀도(Shadow)" 개념을 IIIf 프레임워크에 도입한다. 방법론은 다음 단계로 진행된다:

사례 연구 통합: 저자들은 이전에 IIIf에 정식화되었던 비행 레이더 시스템 명세를 실행 예제로 사용한다. 이 시스템은 항공기 위치, 경로, 그리고 임계 지점들을 포함한다. 초기 명세는 항공기가 임계 지점을 우회할 때, 비행 경로의 관측 가능한 불규칙성을 통해 해당 지점의 임계성을 드러냄으로써 어떻게 암시적 정보 흐름이 발생하는지를 보여준다.
비간섭성(NI)의 정식화: NI는 IIIf 내에서 상태 전이에 대한 구별 불가능성(indistinguishability) 관계로 정의된다. 공격자(보안 등급 $a$ 를 가진)에게 두 상태가 구별 불가능하다는 것은 그들의 관측 가능한 구성 요소(보안 라벨이 $\leq a$ 인 것들)가 동일함을 의미한다. NI는 임의의 구별 불가능한 초기 상태들에 대해, 그 이후의 실행 추적들이 여전히 구별 불가능할 때 성립한다.
섀도(Shadow)의 정의: Morgan의 인식 논리(epistemic logic)에서 영감을 받아, "섀도"는 공격자의 관점에서 보안 임계 상태 구성 요소가 가질 수 있는 모든 가능한 값의 집합으로 정의된다.
- 초기화: 섀도 구성 요소는 최대의 무지(maximum ignorance)를 나타내기 위해 해당 타입의 "전체 집합(universe)"으로 초기화된다.
- 축소(Shrinking): 상태 전이 중에 섀도는 전이가 비밀 구성 요소에 대한 정보를 공격자에게 드러낼 때만 "축소"(가능한 값의 집합이 감소)된다.
- 불변량(Invariant): 보안 시스템은 섀도 구성 요소가 실행 중에 축소되지 않는다는 섀도 불변량 $IFC_a$ 를 만족해야 한다. 만약 섀도가 축소된다면, 이는 공격자가 비밀에 대한 지식을 얻었음을 의미하며, NI 위반을 나타낸다.
동등성 증명: 본 논문은 (Higher Order Logic의 타입 양화 제한으로 인해 종이 위에서) 섀도 불변량 $IF_a$ 가 NI( $NI_a$ )와 동등함을 공식적으로 입증한다. 구체적으로, NI의 부정(부적절한 정보 흐름의 존재)은 구성 요소의 섀도가 축소되는 것과 동등함이 입증된다.
보안 정제 특성화: 저자들은 보안 정제 조건을 정의한다. 추상 시스템 $A$ 에서 구체적 시스템 $C$ 로의 정제 맵 $E$ 가 $C$ 의 섀도 구성 요소에 대해 단사(injective)이고 추상 섀도와 호환될 때, 해당 정제는 보안을 보존한다.

주요 기여

IIIf 내 섀도 정식화: 본 논문은 인프라 상태에 대한 "섀도" 구성 요소의 공식적 정의를 IIIf에 확장하여, 비밀 상태 구성 요소에 대한 공격자의 불확실성을 추적할 수 있게 한다.
섀도와 NI의 동등성: 섀도 불변량( $IFC_a$ )이 IIIf 상태 전이 모델의 맥락 내에서 비간섭성( $NI_a$ ) 속성과 동등함을 증명한다.
보안 정제 정리 (정리 2): 주요 기여는 보안 정제를 특성화하는 정리이다. 이는 정제 맵 $E$ 가 구체적 시스템의 섀도 구성 요소 상에서 단사이고 추상 섀도와 호환된다면, 섀도 불변량(따라서 NI)이 추상 시스템에서 구체적 시스템으로 보존된다고 기술한다.
정제 역설의 해결: 본 방법론은 정제 단계가 NI를 위반하는 새로운 정보 흐름을 도입하지 않음을 검증하는 메커니즘을 제공하여, 기존 IIIf RR-사이클의 알려진 결함을 해결한다.

결과

비행 레이더 시스템에의 적용: 저자들은 비행 레이더 사례 연구에 섀도 정의를 적용한다.
- 보안되지 않은 버전(숨김 메커니즘이 없는 경우)에서는, 임계 지점을 우회할 때 임계 위치 구성 요소의 섀도가 축소되어 $IFC_a$ 및 NI 위반을 증명한다.
- 보안된 버전(실제 우회를 숨기기 위해 critpos 구성 요소를 사용하는 경우)에서는 섀도 불변량이 유지되어, 부적절한 흐름이 없음을 확인한다.
정제 분석: 본 논문은 숨겨진 위치를 기반으로 계산된 새로운 구성 요소(예: "속도")를 추가하는 것이 보안을 위반하는 부적절한 정제(insecure refinement)임을 보여준다. 이는 섀도를 축소시켜 정리 2의 단사성/호환성 조건을 위반하기 때문이다. 반대로, 비밀에 의존하지 않고 올바르게 처리되는 구성 요소를 추가하는 것은 보안을 보존함을 보여준다.
메타 이론적 한계: 저자들은 섀도와 NI 사이의 동등성을 추론할 수는 있지만, 모든 인프라 타입에 대한 동등성 정리의 완전한 정식화는 서로 다른 타입의 구성 요소들을 양화해야 하는 Isabelle/HOL의 타입 시스템 제한으로 인해 제한적임을 언급한다.

의의 및 주장
본 논문은 정보 흐름 제어를 통합함으로써 IIIf 프레임워크의 보안 엔지니어링 능력을 확장한다고 주장한다. 그 의의는 다음과 같다:

정제 역설의 해결: 정제 과정 중에 보안 속성(특히 NI)이 보존되도록 보장하는 구체적인 방법론을 제공하며, 이는 기존 프레임워크에서 부족했던 기능이다.
추상화와 구현의 연결: 섀도 개념을 사용함으로써, 프레임워크는 이제 공격자의 "무지(ignorance)"를 공식적으로 추론하고 정제가 의도치 않게 이 무지를 감소시키지(즉, 정보를 유출하지) 않도록 보장할 수 있다.
실질적 검증: 이 접근 방식은 표준 모델 체킹이 실패하는 복잡하고 이질적인 시스템(물리적 측면과 논리적 측면의 결합)의 검증을 가능하게 한다.

저자들은 섀도와 NI 사이의 동등성 증명이 현재 Isabelle/HOL의 타입 이론적 제약으로 인해 "종이 위에서" 확립되었음을 인정하며, 본 방법론이 일반 목적의 프로그래밍 언어 로직보다는 IIIf 인프라 모델에 특화되어 있음을 밝히며 범위를 겸손하게 설정하고 있다. 이 연구는 Morgan의 기초적 개념을 기반으로 하되, 이를 명시적인 행위자와 정책이 있는 상태 전이 시스템에 적응시켜, 기존 IIIf의 행위자 액세스 권한 모델을 활용함으로써 별도의 인식 논리를 사용할 필요 없이 구현하였다.