QEMU에서 첫 시스템 만들기

Rust 보호 도메인 하나로 QEMU에서 seL4를 부팅하고, 시스템을 정의하는 세 파일을 읽고, 선을 넘는 부분을 seL4가 막는 모습을 지켜본 뒤, 사용자 인터페이스를 클릭해 봅니다.

NoWayOS 시스템은 장치를 이루는 부분인 보호 도메인들의 집합으로, seL4 위에서 함께 부팅됩니다. 모든 시스템은 먼저 개발 컨테이너 안의 QEMU에서 부팅하고 자신의 출력을 스스로 검사합니다. 이 페이지에서는 가장 작은 시스템을 부팅한 다음, 더 많은 것을 보여 주는 시스템 몇 개를 부팅합니다.

hello 부팅하기

make qemu-test SYSTEM=hello

이 명령은 hello 시스템을 빌드하고, 권한 부여를 검사하고, QEMU에서 seL4를 헤드리스로 부팅한 뒤 출력을 지켜봅니다. 시스템이 출력해야 하는 모든 줄이 순서대로 나타나고, 금지된 내용은 하나도 나타나지 않으면 통과합니다.

직접 부팅해서 지켜보려면 make qemu SYSTEM=hello를 실행하십시오. QEMU는 Ctrl-A를 누른 다음 x를 눌러 종료합니다.

시스템을 정의하는 세 파일

각 시스템은 pds/의 Rust 코드 옆, systems/에 있는 세 파일로 이루어집니다.

hello.system 파일은 Microkit 시스템 기술서입니다. 시스템이 가진 모든 보호 도메인, 메모리 영역, 채널, 인터럽트를 담습니다. hello에는 보호 도메인 하나만 있고 다른 것은 없습니다.

<system>
 <protection_domain name="hello" priority="1" stack_size="0x10000">
 <program_image path="nowayos-hello.elf" />
 </protection_domain>
</system>

hello.grants 파일은 시스템이 부여하는 모든 것을 한 줄에 사실 하나씩 나열합니다. 기술서가 여기에 없는 것을 부여하거나, 기술서가 부여하지 않는 것이 여기에 나열되어 있으면 빌드가 실패합니다. 그래서 시스템이 할 수 있는 일이 바뀌면 검토 과정에서 항상 드러납니다.

system demo
role hello app

pd hello priority=1 budget=1000 period=1000

hello.expect 파일은 시스템이 순서대로 출력해야 하는 줄과, ! 뒤에 적어 어디에 나타나든 즉시 테스트를 실패시키는 텍스트를 나열합니다.

NOWAYOS: rust pd starting
NOWAYOS: hello from rust

!MON|ERROR
!seL4(CPU
!panicked

같은 기대 출력 파일로 Raspberry Pi 5에서도 보드의 시리얼 로그를 통해 시스템을 검사합니다.

보호 도메인 자체

pds/hello/src/main.rs가 프로그램 전체입니다. rust-sel4의 Microkit 예제가 보여 주는 최소 형태를 따릅니다. init은 시작할 때 한 번 실행되고, 시스템이 채널을 주었다면 핸들러가 알림을 받았을 것입니다.

#![no_std]
#![no_main]

use sel4_microkit::{Handler, Infallible, debug_println, protection_domain};

#[protection_domain]
fn init() -> HelloPd {
 debug_println!("NOWAYOS: rust pd starting");
 debug_println!("NOWAYOS: hello from rust");
 HelloPd
}

struct HelloPd;

impl Handler for HelloPd {
 type Error = Infallible;
}

힙이 없고(메모리를 할당하면 링크가 실패합니다), unsafe도, 장치도 없습니다. 출력이 되는 것은 디버그 빌드이기 때문일 뿐입니다. 릴리스 커널에는 디버그 콘솔이 없습니다.

seL4가 부분을 멈추는 모습 보기

make qemu-test SYSTEM=isolation-test

탐침 보호 도메인 두 개가 각각 부여받지 않은 일을 시도합니다. 하나는 자신에게 매핑되지 않은 메모리를 읽고, 다른 하나는 읽기만 허용된 페이지에 씁니다. seL4는 각각을 폴트로 멈추고, 옆에 있던 보호 도메인은 아무 영향 없이 계속 실행됩니다. 테스트의 마지막 줄이 이를 알려 줍니다.

NOWAYOS: isolation-test: 2 of 2 forbidden accesses faulted and were contained; bystander still running

더 해 볼 시스템

시스템	보여 주는 것
`ipc-demo`	두 보호 도메인이 공유 링으로 타입 지정 레코드를 주고받습니다. 형식이 잘못된 레코드는 거부됩니다
`timer-demo`	타이머 보호 도메인이 두 클라이언트에 응답하고, 각각의 타임아웃을 마감 순서대로 전달합니다
`supervisor-test`	슈퍼바이저가 폴트를 받아 보드를 재설정하고, 다음 부팅에서는 메모리가 새로 초기화되어 있습니다
`ui-demo`	사용자 인터페이스의 스크립트 세션. 모든 프레임의 해시를 검사합니다

각 시스템은 make qemu-test SYSTEM=NAME으로, 전체 시스템은 make qemu-test-all로 실행합니다.

사용자 인터페이스 클릭해 보기

make qemu SYSTEM=ui-interactive VNC=1

QEMU의 화면은 여러분 컴퓨터의 localhost:5900에서 VNC로 제공되며, 그 실행에만 쓰이는 비밀번호가 출력됩니다. macOS에서는 vnc://localhost:5900을 열고(Finder에서 이동 > 서버에 연결) 데모 화면을 클릭해 보십시오.

빌드가 각 이미지 옆에 남기는 것

build/BOARD/SYSTEM/(여기서는 build/qemu_virt_aarch64/hello/ 등)의 loader.img 옆에 다음이 생깁니다.

sel4-config.txt: 이미지의 seL4 구성과, 그 구성이 seL4의 증명 범위 안에 있는지 여부. 디버그 빌드는 범위 밖이라고 분명히 밝힙니다. 보안을 참고하십시오.
sbom.cdx.json: 이미지의 CycloneDX 소프트웨어 자재 명세서. 커널, 로더, 각 보호 도메인과 그 안의 크레이트를 저마다 해시와 함께 담습니다.
글꼴과 아이콘 라이선스처럼, 이미지에 포함된 것들의 라이선스 파일.