Google은 보안 운영 체제 KataOS의 코드를 열었습니다.

Google은 임베디드 하드웨어를 위한 안전한 운영 체제를 만드는 것을 목표로 하는 KataOS 프로젝트와 관련된 개발을 발견했다고 발표했습니다. KataOS 시스템 구성 요소는 Rust로 작성되었으며 seL4 마이크로커널 위에서 실행됩니다. 이에 대한 신뢰성에 대한 수학적 증거가 RISC-V 시스템에서 제공되어 코드가 공식 언어에 지정된 사양을 완전히 준수함을 나타냅니다. 프로젝트 코드는 Apache 2.0 라이센스에 따라 공개됩니다.

이 시스템은 RISC-V 및 ARM64 아키텍처 기반 플랫폼에 대한 지원을 제공합니다. 하드웨어 위에서 seL4와 KataOS 환경의 작동을 시뮬레이션하기 위해 개발 과정에서 Renode 프레임워크가 사용됩니다. 참조 구현으로 KataOS와 OpenTitan 플랫폼 기반의 보안 칩을 결합한 Sparrow 소프트웨어 및 하드웨어 컴플렉스가 제안되었습니다. 제안된 솔루션을 사용하면 논리적으로 검증된 운영 체제 커널을 OpenTitan 플랫폼 및 RISC-V 아키텍처를 사용하여 구축된 신뢰할 수 있는 하드웨어 구성 요소(RoT, Root of Trust)와 결합할 수 있습니다. 향후 KataOS 코드 외에도 하드웨어 구성 요소를 포함한 다른 모든 Sparrow 구성 요소를 공개할 계획입니다.

이 플랫폼은 특별한 수준의 보호와 장애 유무 확인이 필요한 기계 학습 및 기밀 정보 처리용 애플리케이션을 실행하도록 설계된 특수 칩의 애플리케이션을 염두에 두고 개발되고 있습니다. 이러한 애플리케이션의 예로는 사람의 이미지와 음성 녹음을 조작하는 시스템이 있습니다. KataOS는 신뢰성 검증을 사용하여 시스템의 한 부분에 오류가 발생하더라도 오류가 시스템의 나머지 부분, 특히 커널과 중요한 부분으로 확산되지 않도록 보장합니다.

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

추가 보호를 위해 마이크로커널을 제외한 모든 구성 요소는 해제 후 메모리 액세스, 널 포인터 역참조 및 버퍼 오버런과 같은 문제를 일으키는 메모리 오류를 최소화하는 안전한 프로그래밍 기술을 사용하여 기본적으로 Rust에서 개발되었습니다. seL4 환경의 애플리케이션 로더, 시스템 서비스, 애플리케이션 개발을 위한 프레임워크, 시스템 호출에 접근하기 위한 API, 프로세스 관리자, 동적 메모리 할당을 위한 메커니즘 등이 Rust로 작성되었습니다. 검증된 어셈블리는 seL4 프로젝트에서 개발한 CAmkES 툴킷을 사용합니다. CAmkES용 구성 요소는 Rust에서도 만들 수 있습니다.

Rust는 참조 확인, 객체 소유권 및 객체 수명 추적(범위)을 통해 컴파일 타임에 메모리 안전을 강화하고 런타임 시 메모리 액세스의 정확성을 평가합니다. Rust는 또한 정수 오버플로에 대한 보호 기능을 제공하고, 사용하기 전에 변수 값을 초기화하도록 요구하며, 기본적으로 불변 참조 및 변수 개념을 사용하고, 논리적 오류를 최소화하기 위해 강력한 정적 유형 지정을 제공합니다.

출처 : opennet.ru