기술 요약: 논리 기반 프로그래밍을 이용한 권한 부여용 정책 기술 언어

문제 정의

현대의 정보 시스템은 규모가 점점 커지고 복잡해짐에 따라 모든 취약점을 제거하는 것이 불가능해지고 있습니다. 결과적으로, 공격을 지연시키고 피해를 국소화하기 위해 시스템을 엄격하게 다층적으로 분할하는 방어 심층(Defense-in-Depth) 전략이 채택되고 있습니다. 이 전략의 효과는 **세밀한 강제 접근 제어(Mandatory Access Control, MAC)**에 달려 있습니다. 그러나 세밀한 MAC를 구현하는 데는 상당한 어려움이 따릅니다. 즉, 접근 제어 규칙의 양이 방대해진다는 점입니다.

SELinux와 같은 기존 구현체들은 개별적인 접근 제어 규칙을 직접 나열함으로써 정책을 기술합니다. 입도가 높아질수록 정책 기술의 규모가 거대해지며, 이는 전용 검증 도구 없이는 정책의 전체적인 동작을 파악하기 어렵게 만듭니다. 또한, 기존의 정책 기술 언어(예: SDSI, SPKI, PolicyMaker)는 애플리케이션 특화된 술어(predicate)를 정의하거나, 다층 방어 시나리오에서 효율적인 정책 관리에 필요한 구조적 복잡성을 처리할 수 있는 유연성이 부족한 경우가 많습니다. 핵심 문제는 논리적 정당성을 유지하면서도 구조적 추상화를 지원하고, 거대한 정책을 간결하게 기술할 수 있는 정책 기술 언어가 부재하다는 것입니다.

방법론

저자들은 논리 기반 프로그래밍, 구체적으로는 Datalog(Prolog의 부분 집합)를 사용하여 구현된 정책 기술 언어를 제안합니다. 이 방법론은 세 가지 주요 구성 요소로 이루어집니다.

1. 언어 설계

이 언어는 정책을 **선언적 문장(Declarative Statements, DS)**의 집합으로 정의하며, **권한 부여 질의(Authorization Queries, Q)**를 허용합니다.

• 구문: 이 언어는 술어 논리에 기반하여 영어와 유사한 구문을 사용합니다. 주요 술어는 다음과 같습니다:
  • is permitted to / is forbidden to: 주체(subject)와 객체(object) 사이의 접근 권한을 정의합니다.
  • moves to: 동작에 의해 트리거되는 주체의 상태 전이를 정의합니다.
  • inherits: 속성이 다른 속성으로부터 권한을 상속받을 수 있도록 합니다.
• 형식적 의미론(Formal Semantics): 이 언어는 사실(fact)을 도출하기 위한 형식적 추론 규칙을 정의합니다.
  • 추론 규칙 (a): 변수 항이 상수(constant)로 치환될 때, 조건부 문장에서 특정 사실을 자동으로 도출합니다.
  • 추론 규칙 (b): 다른 속성으로부터 상속받는 속성에 대한 권한을 자동으로 도출하여, 계층적 권한 전파를 가능하게 합니다.
• 구현: 이 언어는 Datalog 프로그램으로 변환됩니다. 선언적 문장은 Datalog 절(clause)이 되며, 권한 부여 질의는 무한 루프를 방지하기 위해 잘 정립된 의미론(well-founded semantics)과 테이블드 술어(tabled predicates)를 지원하는 XSB Datalog 시스템을 사용하여 이 절들에 대해 평가됩니다.

2. 구조적 기술 방법

정책 기술의 복잡성을 해결하기 위해 저자들은 두 가지 구조적 기법을 제안합니다.

• 요소의 계층화: 역할 기반 접근 제어(RBAC)와 유사하게, 추상적인 속성(예: 역할) 아래에 접근 제어 규칙을 그룹화합니다. 규칙은 변수(예: x tagged MANAGER)에 대해 정의되며, 특정 주체가 해당 속성을 부여받을 때 확장됩니다.
• 권한 부여 절차의 구조화: 작업 기반 접근 제어(TBAC)와 유사하게, 권한 부여 절차를 서브루틴화합니다. moves to 술어를 통해 언어가 상태 전이(예: PREPARE_PHASE에서 COMMIT_PHASE로 이동)를 추상화할 수 있게 하여, 복잡한 트랜잭션 흐름을 간결하게 기술할 수 있습니다.

3. 평가 전략

저자들은 이 언어를 평가하기 위해 실험적 시스템을 구축했습니다.

• 유효성(Validity): 기존 SELinux 정책을 제안된 언어로 변환했습니다. SELinux 커널 메커니즘에서 생성된 접근 벡터(Access Vectors)와 Datalog 구현에서 생성된 접근 벡터를 15,100,162개의 질의 조합에 대해 비교했습니다.
• 표현력(Expressiveness): 기존 SELinux 정책의 소스 코드 라인 수 및 리스팅 페이지 수를 제안된 언어의 C-List 스타일 및 ACL 스타일 구현과 비교했습니다.

주요 기여

1. 논리 기반 정책 언어: 접근 제어 규칙을 논리 프로그램으로 표현하여 속성 상속과 권한 부여 절차의 서브루틴과 같은 구조화를 가능하게 하는 언어를 제안했습니다.
2. 형식적 의미론 및 추론 규칙: 속성 계층 및 조건부 전이에 기반하여 권한을 자동 도출할 수 있는 형식적 의미론과 추론 규칙을 정의했습니다.
3. Datalog 구현: 대규모 데이터 교환을 처리할 수 있는 규칙 기반 시스템으로 정책 언어를 변환하는 XSB를 이용한 구체적인 구현을 제공했습니다.
4. MAC를 위한 구조적 추상화: RBAC 및 TBAC와 같은 접근 제어 모델을 구조적으로 기술하는 방법을 제시하여, 모든 개별 규칙을 명시적으로 나열할 필요성을 줄였습니다.

결과

• 유효성: SELinux와의 비교에서, 제안된 언어는 테스트된 15,100,162개의 질의 중 **99.95%**에 대해 동일한 접근 응답(Access Vectors)을 생성했습니다. 나머지 약 0.05%의 불일치는 시스템 운영 중 동적으로 생성되는 컨텍스트와 관련된 질의로, 이는 핵심 권한 로직 외부의 인자 전달 메커니즘에 의존합니다. 저자들은 이 언어가 논리적으로 올바르게 작동한다고 결론지었습니다.
• 표현력 (기술 감소량):
  • 기존 SELinux 정책 소스는 6,524행 및 133페이지를 포함했습니다.
  • 제안된 언어 (C-List 스타일)는 이를 335행 및 95페이지로 줄였습니다.
  • 제안된 언어 (ACL 스타일)는 이를 356행 및 96페이지로 줄였습니다.
  • 이는 소스 코드 라인 수에서 약 95%, 리스팅 페이지 수에서 약 **28%**의 감소를 나타냅니다.

의의 및 주장

본 논문은 제안된 언어가 다층 방어 전략에서의 정책 기술 복잡성을 성공적으로 해결한다고 주장합니다. 논리 프로그래밍을 통해 추상화 수준을 높임으로써 다음과 같은 효과를 얻을 수 있습니다:

• 간결한 정책 기술: 복잡한 정책을 기술하는 데 필요한 코드 양을 획기적으로 줄여 관리를 용이하게 합니다.
• 논리적 정당성: 권한 부여 결정이 수학적, 논리적으로 도출되도록 보장하여 검증을 용이하게 합니다.
• 유연성: 평면적인 규칙 나열 방식의 언어로는 표현하기 어려운 동적 조건(예: "멈춰진 상태" 또는 "오염된 상태") 및 복잡한 상태 전이를 기술할 수 있게 합니다.

저자들은 이 언어가 정책 전체의 *개요(overview)*를 개선하지만, 개별 규칙의 가독성은 직접적인 요소 지정(SELinux와 같은) 방식보다 낮을 수 있다고 언급했습니다. 따라서 이 언어는 엄격하게 정의된 적은 수의 무관한 규칙보다는, 많은 공유 접근 절차나 유연한 구조화가 필요한 방대한 수의 규칙을 가진 시나리오에 특히 적합합니다.

저자들이 밝힌 향aw work(향후 과제)에는 접근 제어의 조건으로서 정책 검증과 같은 애플리케이션의 실현, 메타 규칙을 통한 규칙 변경 관리, 그리고 성능과 보안을 개선하기 위해 Datalog 처리 시스템을 OS 커널에 직접 임베딩하는 것 등이 포함됩니다.