AArch64 아키텍처용 seL4 마이크로커널에 대한 형식적인 보안 검증이 완료되었습니다.

ARM64 명령어 세트 아키텍처를 사용하는 시스템에서 seL4 마이크로커널의 신뢰성과 보안성에 대한 형식적인 수학적 검증 작업이 완료되었습니다. 검증은 seL4 동작의 정확성에 대한 수학적 증명으로 구성되며, 이는 형식 언어로 정의된 사양을 완벽하게 준수함을 보여줍니다. 이러한 신뢰성 증명을 통해 높은 수준의 보안과 오류 없는 작동을 요구하는 ARM64 프로세서 기반의 미션 크리티컬 시스템에서 seL4를 사용할 수 있게 되었습니다.

seL4 마이크로커널은 초기에는 32비트 ARM 프로세서용으로 검증되었고, 이후 64비트 x86 및 RISC-V 프로세서용으로 검증되었습니다. 검증은 시스템의 한 부분에서 오류가 발생하더라도 시스템의 나머지 부분과 핵심 구성 요소로 확산되지 않도록 보장합니다. 보안 측면에서 검증은 커널이 적절한 수준의 애플리케이션 격리를 제공하고, 권한 없이 정보에 접근하는 것을 방지하며, 보조 애플리케이션이 손상되더라도 핵심 애플리케이션으로 공격이 확산되지 않도록 보장하는지 확인합니다.

마이크로커널 seL4의 아키텍처는 사용자 공간에서 커널 자원을 관리하기 위한 부분을 제거하고 이러한 자원에 대해 사용자 자원과 동일한 액세스 제어 수단을 적용한다는 점에서 주목할 만합니다. 마이크로커널은 파일, 프로세스, 네트워크 연결 등을 관리하기 위한 즉시 사용 가능한 고급 추상화를 제공하지 않으며 대신 물리적 주소 공간, 인터럽트 및 프로세서 리소스에 대한 액세스를 제어하기 위한 최소한의 메커니즘만 제공합니다. 하드웨어와 상호 작용하기 위한 고수준 추상화 및 드라이버는 사용자 수준 작업의 형태로 마이크로커널 위에 별도로 구현됩니다. 마이크로커널에서 사용할 수 있는 리소스에 대한 이러한 작업의 액세스는 규칙 정의를 통해 구성됩니다.

출처 : opennet.ru