RISC-V는 RV4 프로세서에서 seL64 마이크로 커널을 확인했습니다.

RISC-V 재단은 마이크로 커널의 작동 원리 시스템의 seL4 명령어 세트 아키텍처 RISC-V. 검증 프로세스가 seL4의 신뢰성에 대한 수학적 증거로 축소되어 공식 언어로 지정된 사양을 완전히 준수 함을 나타냅니다.

안정성 테스트를 통해 seL4를 RISC-V 프로세서 기반의 미션 크리티컬 시스템에서 사용할 수 있습니다. RV64, 더 높은 수준의 신뢰성이 필요하며 실패를 보장하지 않습니다.

seL4 커널을 기반으로 실행되는 소프트웨어 개발자는 시스템의 한 부분에서 오류가 발생하더라도이 오류가 시스템의 나머지 부분, 특히 중요한 부분으로 확산되지 않을 것임을 완전히 확신 할 수 있습니다.

seL4 정보

seL4 아키텍처 사용자 공간에서 커널 리소스를 관리하기 위해 부품을 제거하는 것으로 유명합니다. 사용자 리소스와 같은 리소스에 대해 동일한 액세스 제어 방법을 사용합니다.

마이크로 커널 높은 수준의 추상화를 제공하지 않습니다. 이미 파일, 프로세스, 네트워크 연결 등을 관리 할 준비가되었지만 대신 물리적 주소 공간에 대한 액세스를 제어하는 ​​최소한의 메커니즘 만 제공합니다., 인터럽트 및 프로세서 리소스.

컴퓨터와 상호 작용하기위한 높은 수준의 추상화 및 컨트롤러는 사용자 수준에서 수행되는 작업의 형태로 마이크로 커널 위에 별도로 구현됩니다.

마이크로 커널에서 사용 가능한 리소스에 대한 이러한 작업의 액세스는 규칙 정의를 통해 구성됩니다.

RISC-V는 개방적이고 유연한 시스템을 제공합니다. 기계 지침의 공제없이 임의의 애플리케이션을위한 마이크로 프로세서를 생성 할 수 있습니다. 사용 조건을 부과하지 않습니다.

RISC-V를 사용하면 완전히 개방 된 프로세서 및 SoC를 만들 수 있습니다. 현재 RISC-V 사양을 기반으로 다양한 무료 라이선스 (BSD, MIT, Apache 2.0)에 따라 여러 회사와 커뮤니티에서 이미 생산 된 마이크로 프로세서 코어, SoC 및 칩의 수십 가지 변형을 개발하고 있습니다.

RISC-V 지원은 Glibc 2.27, binutils 2.30, gcc 7 및 Linux 4.15 커널이 출시 된 이후로 이루어졌습니다.

seL4 마이크로 커널 테스트 정보

처음에 마이크로 커널은 seL4는 32 비트 ARM 프로세서 용으로 확인되었습니다., 그리고 x86 64 비트 프로세서의 경우 이후.

RISC-V 개방형 하드웨어 아키텍처와 개방형 마이크로 커널의 조합은 seL4는 새로운 수준의 보안을 달성 할 것입니다., 향후 하드웨어 구성 요소도 완전히 검증 될 수 있으므로 독점 하드웨어 아키텍처로는 달성 할 수 없습니다.

seL4를 확인할 때 하드웨어가 올바르게 작동하고 있다고 가정해야합니다 (즉, 지정된대로). 이는 모든 하드웨어에 적용되는 것은 아니지만 애초에 명확한 사양이 있다고 가정합니다. 

그러나 그러한 사양이 존재하고 공식적인 경우 (즉, 속성에 대한 수학적 추론을 지원하는 수학적 형식주의로 작성), 그것이 실제로 하드웨어의 동작을 포착하는지 어떻게 알 수 있습니까? 

현실은 우리가 이것이 사실이 아니라는 것을 꽤 확신 할 수 있다는 것입니다. 하드웨어는 둘 다 버그가 있다는 점에서 소프트웨어와 다르지 않습니다.

그러나 개방형 ISA를 보유하면 로열티가없는 것 이상의 이점이 있습니다. 하나는 오픈 소스 하드웨어 구현을 허용한다는 것입니다.

seL4를 확인할 때 장비가 표시된대로 작동하고 사양이 시스템의 동작을 완전히 설명한다고 가정하지만 실제로 장비에는 오류가 없으며 이는 추측 실행 메커니즘에서 정기적으로 발생하는 문제로 잘 입증됩니다. .

개방형 하드웨어 플랫폼으로 변경 사항 통합 간소화 예를 들어, 타사 채널을 통해 가능한 모든 누출 채널을 차단하는 보안과 관련하여 소프트웨어로 솔루션을 찾는 것보다 하드웨어로 문제를 제거하는 것이 훨씬 더 효율적입니다.

마지막으로 그것에 대해 더 알고 싶다면 다음 링크.