보안형 시스템

Security type system

컴퓨터 과학에서, 유형 시스템은 변수나 함수와 같은 컴퓨터 프로그램의 다양한 컴포넌트에 유형 속성(int, boolean, char 등)을 할당하기 위해 사용되는 일련의 규칙을 포함하는 구문 프레임워크로 설명될 수 있다.보안 유형 시스템은 정보 흐름 제어를 통해 컴퓨터 프로그램의 보안에만 초점을 두고 유사한 방식으로 작동합니다.따라서 프로그램의 다양한 구성 요소에는 보안 유형 또는 라벨이 할당됩니다.이러한 시스템의 목적은 궁극적으로 주어진 프로그램이 유형 시스템 규칙에 부합하고 비간섭을 충족하는지 검증하는 것입니다.보안 유형 시스템은 언어 기반 보안 분야에서 사용되는 많은 보안 기술 중 하나로 정보 흐름 및 정보 흐름 정책과 밀접하게 연결되어 있습니다.

간단히 말하면, 보안형 시스템은 프로그램에 어떠한 종류의 기밀성 또는 무결성 위반이 있는지, 즉 프로그램이 정보 흐름 정책에 부합하는지 여부를 검출하기 위해 사용될 수 있다.

단순한 정보 흐름 정책

간단한 기밀 정보 흐름 정책을 설명하는 Hasse 다이어그램.

A와 B의 두 사용자가 있다고 가정합니다.프로그램에는 다음 보안 클래스(SC)가 도입됩니다.

  • SC = {∅, {A}, {B}, {A,B}}여기서 is는 빈 세트입니다.

정보 흐름 정책은 정책이 읽기 또는 쓰기 작업을 허용하는지 여부에 따라 정보가 흐를 수 있는 방향을 정의해야 합니다.이 예에서는 읽기 조작(비밀 유지)을 고려합니다.다음 플로우가 허용됩니다.

  • → = {({A}, {A}), ({B}, {B}), ({A,B}, {A,B}), ({A,B}, {A}), ({A,B}, {B}), ({A}, ∅), ({B}, ∅), ({A,B}, ∅)}

이것은 슈퍼셋(⊇)이라고도 할 수 있습니다.즉, 정보가 보다 엄격한 수준의 기밀성을 향해서 흐를 수 있습니다.조합 연산자( 「」)는, 시큐러티 클래스가 다른 시큐러티 클래스에 대해서 읽기 조작을 실행하는 방법을 나타낼 수 있습니다.예를 들어 다음과 같습니다.

  • {A} ⊕ {A,B} = {A}: 양쪽에서 읽을 수 있는 유일한 보안 클래스{A}그리고.{A,B}이{A}.
  • {A} ⊕ {B} = ∅- 둘 다{A}도 아니다{B}양쪽에서 읽을 수 있다{A}그리고.{B}.

이것은, 시큐러티 클래스간의 교차로( 「」)라고도 할 수 있습니다.

정보 흐름 정책은 Hasse 다이어그램으로 나타낼 수 있습니다.정책도 격자로 해야 합니다.즉, 가장 큰 하한과 가장 작은 상한(보안 클래스 간에는 항상 조합이 있습니다).무결성의 경우, 정보는 반대 방향으로 흐르기 때문에 정책이 반전됩니다.

보안 유형 시스템의 정보 흐름 정책

정책이 적용되면 소프트웨어 개발자는 프로그램 구성 요소에 보안 클래스를 적용할 수 있습니다.보안형 시스템의 사용은 보통 유형 시스템 규칙에 따라 정보 흐름 검증을 수행할 수 있는 컴파일러와 결합됩니다.심플화를 위해서, 전 항에서 설명한 정보 플로우 정책과 함께, 매우 간단한 컴퓨터 프로그램을 데모로서 사용할 수 있습니다.심플 프로그램은 다음 의사 코드로 제공됩니다.

if y{A} = 1 then x{A,B} := 0 else x{A,B} := 1

여기서 보안 클래스가 할당된 변수 y에 대해 동등성 검사가 이루어집니다.{A}. 보안 클래스가 낮은 변수x ({A,B})는 이 체크의 영향을 받습니다.이것은 수업에서 정보가 새고 있다는 것을 의미한다.{A}수업하다{A,B}이는 기밀성 정책에 위배됩니다.이 누출은 보안 유형 시스템에서 감지해야 합니다.

예

보안 유형 시스템을 설계하려면 변수에서 보안 유형 또는 클래스로 매핑을 만드는 기능(보안 환경이라고도 함)이 필요합니다.이 함수는 다음과 같이 δ라고 할 수 있습니다.Γ(x) = τ,어디에x변수입니다.τ보안 클래스 또는 유형입니다.보안 클래스는 다음 표기를 사용하여 프로그램 구성 요소에 할당됩니다('판정'이라고도 함).

  • 유형은 다음과 같이 읽기 작업에 할당됩니다.Γ ⊢ e : τ.
  • 유형은 쓰기 작업에 다음과 같이 할당됩니다.Γ ⊢ S : τ cmd.
  • 모든 유형의 상수를 할당할 수 있습니다.

다음 상향식 표기법을 사용하여 프로그램을 분해할 수 있습니다.가정1... 가정n/추정.일단 프로그램이 사소한 판단으로 분해되고, 이것에 의해 유형이 쉽게 결정되면, 프로그램의 덜 사소한 부분에 대한 유형이 도출될 수 있다.정의된 유형 시스템 "규칙"에 따라 "지정자"에 대해 허용된 유형이 도출될 수 있는지 여부를 확인하기 위해 각 "숫자"는 별도로 간주됩니다.

규칙.

보안 유형 시스템의 주요 부분은 규칙입니다.프로그램을 어떻게 분해해야 하는지, 유형 검증을 어떻게 해야 하는지 등을 말합니다.이 장난감 프로그램은 조건부 테스트와 두 가지 가능한 변수 할당으로 구성됩니다.이들 2개의 이벤트에 대한 규칙은 다음과 같이 정의됩니다.

할당:
Γ(x) = τ1, Γ ⊢ a : τ2
Γ ⊢ x := a : τ1 cmd
여기서 다음 조건이 유지되어야 합니다.τ2 ⊑ τ1
조건부 테스트:
Γ ⊢ t : τ, Γ ⊢ S1 : τ1 cmd, Γ ⊢ S2 : τ2 cmd
Γ ⊢ if t then S1 else S2: τ1 ⊓ τ2 cmd
여기서 다음 조건이 유지되어야 합니다.τ ⊑ τ1, τ2

위의 간단한 프로그램에 이를 적용하면 다음과 같은 결과를 얻을 수 있습니다.

3 Γ(y) = {A} Γ(x) = {A,B} cmd, Γ ⊢ 0 : {A,B} Γ(x) = {A,B} cmd, Γ ⊢ 1 : {A,B}
2 Γ ⊢ y = 1 : {A} Γ ⊢ x := 0 : {A,B} cmd Γ ⊢ x := 1 : {A,B} cmd
1 Γ ⊢ if y = 1 then x := 0 else x := 1 : Not typeable

유형 시스템은 보안 클래스의 읽기 작업을 수행하는 행 2에서 정책 위반을 감지합니다.{A}그 후 보안 클래스의 2개의 쓰기 조작이 실행됩니다.{A,B}좀 더 공식화된 말로 하자면{A} ⋢ {A,B}, {A,B}(조건부 테스트의 규칙에서).따라서 프로그램은 "입력할 수 없음"으로 분류됩니다.

건전성

보안유형 시스템의 건전성은 비공식적으로 다음과 같이 정의될 수 있다: If programP타이핑이 잘 되어 있습니다.P는 비간섭을 충족합니다.

레퍼런스

추가 정보

  • Dennis Volpano, Cynthia Irvine 및 Geoffrey Smith, A Sound Type System for Secure Flow Analysis, Journal of Computer Security, 1996.
  • Fred B. Schneider, Greg Morrisett, Robert Harper, 언어 기반 보안 접근법
  • 안드레이 사벨펠트, 앤드류 C마이어, 언어 기반 정보 흐름 보안.