신뢰성 높은 시스템 구축을 위한 오픈소스 마이크로커널 Muen 1.0 출시

1.0년 간의 개발 끝에 분리 커널을 개발하는 Muen 86 프로젝트가 출시되었으며, 정식 신뢰성 검증을 위한 수학적 방법을 사용하여 소스 코드에 오류가 없음이 확인되었습니다. 커널은 x64_2014 아키텍처에 사용할 수 있으며 높은 수준의 안정성과 무장애 보장이 필요한 미션 크리티컬 시스템에서 사용할 수 있습니다. 프로젝트의 소스 코드는 Ada 언어와 해당 언어의 검증 가능한 방언 SPARK 3로 작성되었습니다. 코드는 GPLvXNUMX 라이센스에 따라 배포됩니다.

분리 커널은 서로 분리된 구성 요소의 실행을 위한 환경을 제공하는 마이크로 커널이며, 그 상호 작용은 주어진 규칙에 따라 엄격하게 규제됩니다. 격리는 Intel VT-x 가상화 확장 사용을 기반으로 하며 비밀 통신 채널의 구성을 차단하는 보안 메커니즘을 포함합니다. 파티셔닝 커널은 다른 마이크로커널보다 더 최소화되고 정적이므로 오류를 일으킬 수 있는 상황의 수가 줄어듭니다.

커널은 하이퍼바이저와 유사한 VMX 루트 모드에서 실행되며 다른 모든 구성 요소는 게스트 시스템과 유사한 VMX 비루트 모드에서 실행됩니다. 장비에 대한 액세스는 Intel VT-d DMA 확장 및 인터럽트 재매핑을 사용하여 이루어지며, 이를 통해 Muen에서 실행되는 구성 요소에 대한 PCI 장치의 보안 바인딩을 구현할 수 있습니다.

Muen의 기능에는 멀티 코어 시스템, 중첩된 메모리 페이지(EPT, Extended Page Tables), MSI(Message Signaled Interrupts) 및 메모리 페이지 속성 테이블(PAT, Page Attribute Table)에 대한 지원이 포함됩니다. Muen은 또한 Intel VMX 선점형 타이머를 기반으로 하는 고정 라운드 로빈 스케줄러, 성능에 영향을 주지 않는 컴팩트 런타임, 충돌 감사 시스템, 규칙 기반 정적 리소스 할당 메커니즘, 이벤트 처리 시스템 및 공유 메모리 채널을 제공합니다. 실행 중인 구성요소 내에서의 통신.

64비트 기계어 코드, 32비트 또는 64비트 가상 머신, Ada 및 SPARK 64 언어의 2014비트 애플리케이션, Linux가 포함된 가상 머신, Muen 기반의 MirageOS 기반 독립형 "유니커널"을 사용하여 구성 요소 실행을 지원합니다.

Muen 1.0 릴리스에서 제공되는 주요 혁신 사항은 다음과 같습니다.

• 프로젝트의 모든 측면을 문서화하는 커널(장치 및 아키텍처), 시스템(시스템 정책, Tau0 및 툴킷) 및 구성 요소에 대한 사양이 포함된 문서가 게시되었습니다.
• 시스템 이미지를 구성하고 Muen에서 실행되는 표준 서비스를 개발하기 위한 미리 만들어진 검증된 구성 요소 세트를 포함하는 Tau0(Muen System Composer) 툴킷이 추가되었습니다. 제공되는 구성 요소에는 AHCI(SATA) 드라이버, 장치 관리자(DM), 부트로더, 시스템 관리자, 가상 터미널 등이 포함됩니다.
• muenblock Linux 드라이버(Muen 공유 메모리 위에서 실행되는 블록 장치의 구현)가 blockdev 2.0 API를 사용하도록 변환되었습니다.
• 기본 구성 요소의 수명 주기를 관리하기 위한 도구를 구현했습니다.
• 무결성을 보호하기 위해 SBS(Signed Block Stream) 및 CSL(Command Stream Loader)을 사용하도록 시스템 이미지를 변환했습니다.
• SPARK 2014 언어로 작성된 검증된 AHCI-DRV 드라이버가 구현되었으며 이를 통해 ATA 인터페이스 또는 개별 디스크 파티션을 지원하는 드라이브를 구성 요소에 연결할 수 있습니다.
• MirageOS 및 Solo5 프로젝트의 유니커널 지원이 향상되었습니다.
• GNAT Community 2021 릴리스에 대해 Ada 언어 툴킷이 업데이트되었습니다.
• 지속적인 통합 시스템이 Bochs 에뮬레이터에서 QEMU/KVM 중첩 환경으로 이전되었습니다.
• Linux 구성 요소 이미지는 Linux 5.4.66 커널을 사용합니다.

출처 : opennet.ru