분리 커널

Separation kernel

분리 커널은 분산 환경을 시뮬레이션하는 데 사용되는 보안 커널의 일종이다.이 개념은 1981년 논문에서 존 러쉬비에 의해 소개되었다.[1]러시비는 분리 커널을 "범용 다용도 사용자 시스템에 다층적 보안 운영을 제공"하고자 했던 크고 복잡한 보안 커널의 개발과 검증에서 발생한 어려움과 문제에 대한 해결책으로 제안했다.러시비에 따르면, "분리 커널의 임무는 물리적으로 분산된 시스템이 제공하는 것과 구별할 수 없는 환경을 만드는 것이다. 각 체제는 별도의 고립된 기계인 것처럼 보여야 하며, 정보는 알려진 외부 통신선을 따라 한 기계에서 다른 기계로만 흐를 수 있다.그러므로 분리 커널을 증명해야 하는 속성 중 하나는 명시적으로 제공된 것 외에 정권 간 정보 흐름을 위한 채널이 없다는 것이다."

분리 커널의 변종인 파티셔닝 커널은 하나의 프로세서로, 여러 가지 기능을 통합하는 방법으로 상업적 항공 커뮤니티에서 인정을 받았다.이 장르의 상업용 실시간 운영 체제 제품은 항공기 제조사가 안전 중요 항전 애플리케이션용으로 사용해 왔다.

2007년 미국 국가안보국(NSA)의 정보보호국([2]Information Assurance Directorate of the NSA)은 가장 적대적인 위협 환경에서 사용하기에 적합한 분리 커널에 대한 보안 요구사항 규격인 분리 커널 보호 프로파일(SKPP)을 발간했다.SKPP는 공통 기준[3] 유사하게 Rushby의 개념 분리 커널의 기초적 특성을 제공하는 현대 제품군을 설명한다.그것은 분리 커널의 구축과 평가를 위한 보안 기능 및 보증 요구사항을 정의하면서 개발자가 선택할 수 있는 권한은 어느 정도 제공한다.

SKPP는 분리 커널을 "하드웨어 및/또는 펌웨어 및/또는 소프트웨어 메커니즘으로 정의하며, 주된 기능은 다중 파티션을 설정, 격리 및 분리하고 피사체와 해당 파티션에 할당된 내보내기 리소스 간의 정보 흐름을 제어하는 것이다."또한 분리 커널의 핵심 기능 요구사항은 다음과 같다.

  • 모든 리소스(CPU, 메모리 및 장치 포함)의 무단 액세스 방지
  • 평가 보안 기능(TSF)이 사용하는 내부 리소스와 대상자가 사용할 수 있는 내보낸 리소스의 분리.
  • 내보낸 리소스의 파티셔닝 및 분리.
  • 파티션 간 및 내보낸 리소스 간 정보 흐름 조정.
  • 감사 서비스.

분리 커널은 자신이 통제하는 모든 내보낸 자원을 파티션에 할당한다.명시적으로 허용된 정보 흐름을 제외하고 파티션은 격리된다.한 칸막이에 있는 피사체의 동작은 다른 칸막이에 있는 피사체로부터 격리된다(viz, 다른 칸막이에 있는 피사체에 의해 감지되거나 전달될 수 없다).파티션과 흐름은 구성 데이터에 정의되어 있다.'파티션'과 '주체'는 직교 추상화라는 점에 유의하십시오.그것의 수학적 창조에 의해 나타나는 '파티션'은 시스템 실체의 설정-이론적 그룹화를 제공하는 반면, '주체'는 시스템의 개별 활성 실체에 대해 우리가 추론할 수 있게 해준다.따라서 파티션(수집, 0개 이상의 요소 포함)은 제목(활성 요소)이 아니지만 0개 이상의 대상을 포함할 수 있다.[2]분리 커널은 그것의 호스트된 소프트웨어 프로그램에 높은 보안 분할과 정보 흐름 제어 속성을 제공하며, 변조 방지 및 우회 불가능이다.이러한 기능은 다양한 시스템 아키텍처에 대해 구성 가능한 신뢰할 수 있는 기반을 제공한다.[2]

해결 방법

2011년 정보보안 책임자는 SKPP에 대한 분리 커널을 포함한 특정 운영체제를 더 이상 인증하지 않을 것이다. NSA는 "이 보호 프로파일에 대한 적합성 자체만으로는 국가 보안 정보가 더 큰 맥락에서 적절하게 보호된다는 충분한 확신을 제공하지 못한다"고 언급했다.순응형 제품이 통합되는 시스템".[5]

seL4 마이크로커널은 분리 커널로 구성할 수 있다는 정식 개념 증명을 가지고 있다.[6]이것과 함께 정보의[7] 강제적인 지속은 그것이 높은 수준의 보증의 예라는 것을 암시한다.뮤엔[8] 분리 커널은 x86 머신용으로 공식적으로 검증된 오픈 소스 분리 커널이기도 하다.

참고 항목

참조

  1. ^ John Rushby, "보안 시스템의 설계와 검증", 운영 체제 원리에 관한 제8회 ACM 심포지엄, 페이지 12-21, CA, 12월. (ACM 운영 체제 리뷰, 제15권, 제5호)
  2. ^ a b c 2007년 6월, National Security Agency, Fort George G. Meade, MD. "고강건성이 요구되는 환경의 분리 커널에 대한 미국 정부 보호 프로파일," 버전 1.03.
  3. ^ "정보 기술 보안 평가를 위한 공통 기준," 버전 3.1, CCMB-2006-09-001, 002, 003, 2006년 9월.
  4. ^ http://www.niap-ccevs.org/cc-scheme/st/st_vid10119-st.pdf
  5. ^ https://www.niap-ccevs.org/pp/archived/PP_SKPP_HR_V1.03/
  6. ^ "The L4.verified Proofs". GitHub. 18 November 2021.
  7. ^ https://www.nicta.com.au/publications/research-publications/?pid=646464
  8. ^ https://muen.sk/muen-report.pdf