DSDC-MAC 모델[13]은 직무분리와 데이터 컬러링을 이용해서, 주체(Subject)인 user에게 그리고 객체(object)인 data에게 보다 세분화된 접근제어를 제공하여 기밀성과 무결성을 동시에 보장하는 정책을 지원한다. 보안 정책에 따라 주체(User)와 객체(Object)에 대해 직무를 분리하고, 이렇게 분류된 주체별로 data의 보안 등급에 따른 color를 부여하였다. 부여된 color별로 보안키를 매칭(matching)하여 주체가 객체(혹은 데이터)를 접근 또는 접근하지 못하도록 제어한다. 이를 통해, MAC 모델 기반 기밀성과 무결성의 동시 지원시 보안 정책간 충돌을 방지할 수 있다. <그림 1>에서 처럼, DSDC-MAC 모델의 구조는 보안 등급 정책(SLP), 직무분리 정책, Data-Coloring 규칙이 적용된 주체(S), 보안키(SK), 객체(O)와의 연관 관계를 중심으로 구성되었다. <그림 1>은 [13]의 DSDC-MAC 모델에 대해서, 속성, 연산과 스테레오타입을 제거하고 관계명과 다중성을 새로이 추가하여 작성한 것이다. 그 이유는 Z 명세의 복잡성을 줄이고 스테레오 타입을 Z로 표현할 수 없기 때문이다.

모델, 메타모델 혹은 프레임워크가 가진 구문과 의미를 정형적으로 명세하기 위한 언어 중에 Z 언어[14]가 있다. Z는 범용적 ISO 표준 언어로서 증명(proof)을 위한 좋은 기능을 제공하며, Z의 state 스키마가 메타모델을 표현한 클래스 모델의 class와 동일한 구조를 갖으며, 정적 속성(property)을 갖고 있어 상호 직접적 변환을 할 수 있다. Z로 명세된 Z 스키마의 구문적 및 의미적 검사를 도구로Z/EVES Tool[17]이 널리 이용되고 있다. [16, 18-19]에서 제시된 프레임워크 혹은 메타모델을 대상으로 Z 언어로 변환, 명세하고, 이 Z 스키마 명세를 Z/EVES 도구를 사용해서 검사를 보였다.

제시한 DSDC-MAC 모델을 기반해서 구현 시스템의 아키텍처를 설계한 것이 <그림 2>이다.

접근제어의 동작과정에 대해서, 주체인 사용자와 data인 객체간을 연결하는 보안키는 사용자가 보안키 관리자로부터 승인받아 배부 받는다. 데이터베이스 관리시스템(DBMS: Data Base Management System) 혹은 시스템 관리자는 필요시 해당 객체의 주체인 사용자에게 대여요청 후, 승인받아 데이터에 대한 접근을 수행한다. 주요 핵심모듈로 보안키 접속 모듈, 보안키 인증 시스템내에 존재하는 보안키 통제 관리 모듈, DBMS 내에서 처리하는 보안컬러-데이터 매칭 모듈이 있다. DBMS 내에는 데이터 컬러링된 객체들이 보관되어 사용자가 해당되는 접근 권한을 가진 보안키로 접근시에 인증 절차를 거쳐 읽기, 쓰기 등의 접근이 이루어진다. 이러한 보안 구조를 가지는 DBMS와 연계되는 응용 소프트웨어(application software)들은 연동을 위한 보안키 접속 모듈을 추가하여야 한다. 이에 따른 응용 소프트웨어의 변경 비용이 발생할 것이나, 보안키 인증 시스템에서 간단한 에이전트 형식으로 개발을 한다면 그 비용은 최소화시킬 수 있을 것이다.

DSDC-MAC 모델 구현 시스템에서 주요 모듈의 세부적 처리 기능은 다음과 같다.

Security_Key Access Module은 응용 소프트웨어 개발시에 포함해야 하는 모듈로, 사용자가 가진 보안키에 대한 인증 값을 보안키 통제 관리 모듈에 전송하여 인증을 받아서, 사용자가 해당 보안컬러가 적용된 데이터에 접근하는 권한을 수행할 수 있도록 하는 기능을 제공한다. 사용자 ID & Password 인증 방식과 연계하여 2차 인증 수단(이중 시건 장치)으로서 보안키가 이용되도록 적용되어야 한다.

Security_Key Control Management Module은 사용자가 가지는 보안키에 대한 통제 및 관리 기능을 제공한다. 이것은 DBMS 내에 보안키 관리 모듈로 혹은 외부에 별도 모듈로 구현할 수 있다. 이 모듈은 응용 소프트웨어 내의 보안키 접속 모듈로부터 입력된 사용자의 보안키 입력 값을 인증하여 정당한 권한 수행을 할 수 있도록 통제하는 기능과 보안키 위임 신청 및 승인과 관련된 관리 기능을 수행한다. 또한, Security Color-Data Matching Module과 연계하여 DB에 접근할 수 있다.

Security Color-Data Matching Module은 DBMS에 포함되어야 하는 핵심이 되는 기능으로, 데이터 컬러링 Rules에 따라 Database의 각 Field 등에 대한 보안컬러를 정의하고, 각각의 보안컬러와 보안키를 매칭하는 기능을 수행한다. 또한 별도의 정책 저장소(Policy Repository)에 저장된 ACL, ACM 그리고 ACP와 SLP, SoD P에 따라 세부적인 접근 제어 기능을 수행한다. 즉, 인증된 사용자의 보안키별로 권한(조회, 쓰기, 수정, 삭제)을 수행하도록 제어한다. JOIN 또는 VIEW 수행 시에도 데이터와 보안컬러에 대한 일관성을 유지한다.

<그림 2>의 DSDC-MAC 구현 시스템의 설계 모델에서, 어떻게 기능 모듈들이 상호작용해서, 직무 분리된 사용자(주체)가 보안키를 배부 받아, 데이터 컬러링된 DB(data)에 접근 제어하는 절차를 표현한 것이 <그림 3>이다.

<그림 3>에서, 과정 1~3은 사용자가 보안키 관리자로부터 해당 레벨에 맞는 보안키를 할당받고, 보안키 접속모듈이 포함된 응용 소프트웨어 서버는 과정 4~5와 같이 ID와 PW를 기반으로 1차 인증과정을 거치고, 사용자의 보안키 값을 이용해 과정 6~7과 같이 보안키 통제모듈을 통해 2차 인증을 실시한다. 이후 사용자의 검색 질의가 있으면, 과정 8~9와 같이 응용 소프트웨어의 보안키 접속 모듈은 보안키 인증 시스템으로 해당 값을 전송하고, 보안키 인증 시스템은 과정 10~14와 같이 자체 무결성 검증 과정을 거쳐 해당 사용자의 보안컬러 레벨과 접근 제어 정책과의 비교, 분석을 통해 결정된 접근 권한을 통보받게 된다. 이 과정에 대한 결과 값은 접근제어 정책 저장소에 저장되게 되고, 추후 검토 데이터로 활용된다. 이렇게 할당된 접근권한을 바탕으로 과정 15~17과 같이 DBMS 내 보안컬러-데이터 매칭 모듈은 보안컬러와 객체와의 접근권한에 대한 무결성 검증을 거쳐 DB로 메시지를 전달하고, 과정 18~19에서 최종적으로 질의 결과를 클라이언트에게 전달하게 된다.

[13]의 적용 사례에서 제시된 HRMS MAC model을 가지고 단원 3.1에서 제시한 DSDC-MAC 구현시스템의 아키텍처인 <그림 2>를 적용해서 구현 시스템을 설계한 것이 <그림 4>이다.

<그림 2>에서 설명한 바와 같이, 사용자, 즉 주체는 해당직무 및 보안등급에 맞는 보안키(예, SK_G_t₁ , SK_B_t₁)를 보안키 관리자로부터 수령하고, HRMS에 접속하여 보안키를 인증 받은 후 보안키에 적합한 데이터에 접근한다. 이때, 데이터 접근시에는 Security Color-Data Matching module을 통해 Security policy repository의 정책 적용을 받는다.

본 단원에서는 Z 언어를 사용하여 DSDC-MAC 모델을 정형적으로 명세한다. 즉, 모델을 표현한 시각적 명세 표기의 클래스 다이어그램을 정형적 명세 표기로의 구문적 및 의미적 변환, 명세를 다룬다. 정형명세는 [15-16]에서 제시한 클래스 메타 모델과 Z간의 변환 규칙에 의해서 DSDC-MAC 모델의 구문과 정적 의미(Static Semantics)에 대해 Z 스키마로 명세한다.

[15-16]에 제시된 클래스 모델의 Z로의 변환 규칙을 이용해서 <그림 5>의 모델을 대상으로 Z로 정형화하여 명세한다. 이 변환 규칙은 타입 선언하고, 이 타입에 기반해서 클래스 대상의 요소 기반 Z 스키마를 정의하고 클래스들간의 관계에 기반한 Z 스키마를 명세한다[16, 18-19].

Z 명세의 구축 결과로서, 기본타입으로 subject_ID외 11개의 기본 타입을 선언하고, 요소 기반 스키마 명세로 Security_Key외 14개를 정의하고, 그리고 관계 기반 스키마 명세로 Depend_CIU 외 9개를 작성하였다.

이전 단원에서 작성한 Z 명세에 대한 정확성 검사가 필요하다. 왜냐하면, DSDC-MAC 모델이 Z 스키마로 변환, 명세되었고, 이 Z 명세의 구문적 및 정적 시멘틱 속성이 정확함을 보여야 모델이 명확하다는 것을 입증하기기 때문이다. 이를 위해, Z/EVES Tool을 사용하여 Z 명세에 구문적 구조와 속성 등의 정확성 검사가 요구된다. Z/Eves Tool을 사용해서, Z 스키마 명세에 대해 syntax checking, variable range checking 및 consistency type checking을 체킹(checking)한다 [14-16].

Z/EVES 툴을 통한 검사 결과로서, 먼저, 단원 4.1.1의 기본 타입 선언 11개, 자유 타입 5개에 대한 명세에 대해 “syntax”와 “proof” 속성의 검사결과 “Y”로 실행 결과가 나왔다. 이로서 기본 타입과 자유 타입에 대한 오류가 없음을 확인하였다.

다음으로, 단원 4.1.2(<그림 5>)에 대한 요소 기반 Z 스키마 명세에 대해 15개에 대한 모델 검사의 결과를 <그림 7>에서 보여준다.

<그림 7>에서, 왼쪽 상단에 표시된 ‘syntax’는 syntax와 type checking을 보여주는 것으로 ‘Y'로 나타나면 타입간 일치성이 있음을 입증하는 것이다. 반면, ’proof'는 domain checking의 결과를 보여주는 것으로 ‘Y'로 나타나면, 그 명세가 정확함을 의미한다. <그림 7>에서, 포함 관계를 갖는 “Access_Control_Policy” 스키마는 이전에 스키마로 선언된 “Access_Control_List”와 “Access_Contrl Matrix”를 포함하는 것을 술어부에 instance로 명세하였다. 상속 관계에 대해서, “Sec_Level_Policy” 스키마가 앞서 정의한 “Access_Control_ Policy” 스키마를 상속받아 정의됨을 술어부에 기술하였다.

끝으로, 단원 4.1.2(<그림 6>)에 대한 관계 기반 Z 스키마 명세인 10개(의존 6개, 연관 관계 2개, 집합 관계 2개)에 대한 모델 체킹의 결과를 <그림 8>에 나타내었다.

<그림 8>에서, syntax와 proof 부문이 “Y" 의 결과를 보임으로서 명세가 정확함을 알 수 있다. Proof는 reduce에 의해 prove하였다(prove by reduce). 그러나, 의존 관계의 스키마 경우, <그림 5>의 ”DependOn_CIU“ 스키마에서 ”(User≠User’) → (Certi_Id_Password≠Certi_Id_Password’)에 대해 Z/EVES에서 표현할 수 가 없어서 술어부에 의존을 표현하고, 술어부에 대응수와 유일성만을 표현하여 검사하였다.

결과적으로, 이와 같은 모델 체킹을 통해, DSDC-MAC 모델의 구문적 및 정적 시멘틱 측면에서 오류가 없음을 입증할 수 있다. 즉, 클래스간의 관계와 대응 수를 명확하게 명세하고, 검사하여 메타모델의 구문적 구조에서 요소들간 불일치 등의 오류(error) 혹은 충돌(conflict)이 발생하지 않았다.