seL4 마이크로커널은 RISC-V 아키텍처에 대해 수학적으로 검증되었습니다.

RISC-V 재단 보고 마이크로커널의 작동 검증에 대해 셀4 RISC-V 명령어 세트 아키텍처를 사용하는 시스템에서. 확인은 다음과 같습니다. 수학적 증명 seL4 작동의 신뢰성은 공식 언어에 지정된 사양을 완벽하게 준수함을 나타냅니다. 신뢰성 증명 당신이 사용할 수 있습니다 향상된 수준의 신뢰성을 요구하고 오류 없음을 보장하는 RISC-V RV4 프로세서 기반 미션 크리티컬 시스템의 seL64. seL4 커널 위에서 실행되는 소프트웨어 개발자는 시스템의 한 부분에 오류가 발생하더라도 이 오류가 시스템의 나머지 부분, 특히 중요한 부분으로 확산되지 않을 것임을 완전히 확신할 수 있습니다.

seL4 마이크로커널은 처음에는 32비트 ARM 프로세서용으로 검증되었고 나중에는 64비트 x86 프로세서용으로 검증되었습니다. 개방형 RISC-V 하드웨어 아키텍처와 개방형 seL4 마이크로커널의 결합은 독점 하드웨어 아키텍처에서는 달성할 수 없는 하드웨어 구성 요소도 향후 완전히 검증할 수 있기 때문에 새로운 수준의 보안을 달성할 수 있다는 점에 주목합니다.

seL4를 검증할 때 장비가 명시된 대로 작동하고 사양이 시스템의 동작을 완전히 설명한다고 가정하지만 실제로 장비에는 오류가 없습니다. 이는 예측 실행 메커니즘에서 정기적으로 나타나는 문제를 통해 명확하게 입증됩니다. 지침. 개방형 하드웨어 플랫폼을 사용하면 보안 관련 변경 사항을 더 쉽게 통합할 수 있습니다. 예를 들어 가능한 모든 부채널 누출을 차단하는 경우 소프트웨어에서 해결 방법을 찾는 것보다 하드웨어에서 문제를 제거하는 것이 훨씬 더 효율적입니다.

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

RISC-V는 로열티나 사용에 따른 문자열을 요구하지 않고 임의의 애플리케이션용으로 마이크로프로세서를 구축할 수 있는 개방적이고 유연한 기계 명령 시스템을 제공합니다. RISC-V를 사용하면 완전히 개방형 SoC 및 프로세서를 만들 수 있습니다. 현재 다양한 무료 라이센스(BSD, MIT, Apache 2.0)에 따라 다양한 회사 및 커뮤니티의 RISC-V 사양을 기반으로 합니다. 개발 중 수십 가지의 마이크로프로세서 코어, SoC 및 이미 생산된 칩 변형. RISC-V 지원은 Glibc 2.27, binutils 2.30, gcc 7 및 Linux 커널 4.15 릴리스부터 제공되었습니다.

출처 : opennet.ru