보안 커널의 구조적 명세

전체 운영 체제를 신뢰할 수 있도록 인증하는 것은 실행 가능한 큰 작업이 아닙니다. 대신, 우리는 정보 보안을 제공할 보안 커널을 설계하고 있습니다. 커널의 역할은 보안을 침해하지 않도록 정보 흐름을 모니터링하는 것입니다. 구조적 명세라는 기술을 사용하여 안전한 설계를 장려하며, 이를 통해 보안 커널의 점진적으로 더 상세한 모델이 개발됩니다. 초기 모델 M 0은 컴퓨터 시스템에 적용된 정부의 보안을 공식화하는 추상적 설명입니다. 이후 모델링 단계는 점점 더 많은 세부 정보를 제공하며, 점차적으로 모델이 특정 시스템(이번 경우는 Multics)과 유사해지기 시작합니다. 두 번째 모델 M 1은 트리 구조의 파일 시스템과 에이전트 간 통신 시스템을 정의하고, M 2는 동적 환경에서의 세분화에 관한 세부 사항을 추가합니다. 최종 모델링 수준은 Multics 유사 시스템의 커널을 위한 원시 명령을 명시하고, 구현의 정확성을 확립하기 위해 반드시 증명해야 할 주장들을 정확히 나열할 예정입니다.