시스템의 구성 방식

모든 NoWayOS 장치는 하나의 시스템입니다. 빌드하기 전에 선언된 고정된 부분들의 집합이며, 각 부분은 seL4에 의해 서로 봉인되어 분리됩니다. 실행 중에 추가되는 것은 없습니다. 이 페이지에서는 각 요소와 그 연결 방식을 설명합니다.

보호 도메인

보호 도메인은 시스템의 한 부분입니다. 자기만의 메모리를 가지며, 부여받은 케이퍼빌리티만 보유하는 프로그램입니다. seL4에서 케이퍼빌리티는 커널 객체 하나와 그에 대한 권리를 지정하는 위조할 수 없는 토큰으로, 문 하나만 여는 출입 카드와 같습니다. 보호 도메인은 자신의 케이퍼빌리티가 지정하지 않은 것은 아무것도 건드릴 수 없으며, seL4가 이를 강제합니다.

일반적인 시스템에는 관심사마다 보호 도메인이 하나씩 있습니다. 디스플레이 드라이버, 입력 경로, 네트워크 스택, 사용자 인터페이스, 애플리케이션, 타이머, 슈퍼바이저, 워치독입니다. 각각은 시작한 뒤에는 아무것도 할당하지 않는 작은 no_std Rust 프로그램입니다.

시스템 기술서

Microkit 시스템 기술서(systems/NAME.system, XML 파일)는 시스템 전체를 선언합니다. 우선순위, 예산, 스택을 포함한 모든 보호 도메인, 모든 메모리 영역과 그것을 매핑하는 주체, 모든 채널, 모든 인터럽트를 담습니다.

• 기술서는 장치를 이름으로 가리킬 뿐, 주소를 쓰지 않습니다: phys_addr="@NAME". 주소는 platforms/에 있는 보드별 파일에서 저마다 출처와 함께 가져오므로, 같은 기술서로 QEMU용과 Raspberry Pi 5용을 모두 빌드합니다.
• 채널은 두 보호 도메인을 연결하며, 알림(데이터 없는 신호이며 인터럽트도 여기에 속합니다)과 보호된 프로시저 호출(더 높은 우선순위 부분으로의 동기 호출)에 쓰입니다.

기술서가 곧 시스템의 보안 설계이므로, 기술서의 변경은 보안 변경으로 검토합니다.

권한 부여 파일

각 기술서 옆의 systems/NAME.grants는 시스템이 부여하는 모든 것을 한 줄에 사실 하나씩 나열합니다. 우선순위, 예산, 메모리, 장치, 인터럽트, 채널입니다. 둘이 어느 방향으로든 어긋나면 빌드가 실패합니다.

각 보호 도메인에는 역할(ui, input, broker, display, driver, network, security, storage, update, app, supervisor, watchdog, clock, test 중 하나)도 있으며, 빌드는 그 역할이 절대 가져서는 안 되는 권한 부여를 거부합니다. 사용자 인터페이스에 실수로 네트워크 장치가 넘어갈 수 없고, 테스트용 도구가 제품에 몰래 끼어들 수도 없습니다.

타입 지정 메시지

보호 도메인은 타입 지정 메시지로 대화합니다. 레이아웃이 명시된 고정 크기의 버전 관리 레코드로, 공유 메모리 위의 단일 생산자·단일 소비자 링으로 전달됩니다.

• 복사 후 검사. 받는 쪽은 각 레코드를 검증하기 전에 공유 메모리 밖으로 복사하므로, 보낸 쪽이 검사와 사용 사이에 레코드를 바꿀 수 없습니다(이중 페치라고 부르는 버그).
• 디코더는 패닉할 수 없습니다. 각 디코더는 형식이 잘못된 모든 입력에 타입 지정 오류를 반환하며, Kani 유계 증명과 퍼즈 타깃을 갖추고 있습니다.
• 양쪽은 각자의 뷰를 가집니다. 생산자와 소비자는 별도의 메모리 뷰로 링을 보며, 공유 인덱스는 acquire/release 순서를 사용합니다.

입력

애플리케이션은 표준화된 입력 이벤트, 즉 키, 포인터 이동, 터치만 봅니다. 이 이벤트는 화면 범위와 대조해 검사되고 속도가 제한됩니다. 애플리케이션은 USB를 비롯한 어떤 장치 프로토콜도 보지 않습니다. 입력 경로가 자체 보호 도메인에서 모든 바이트를 적대적인 것으로 간주하며 이를 해석합니다.

폴트, 슈퍼바이저, 페일세이프 상태

보호 도메인이 seL4가 허용하지 않는 일을 하거나 패닉하면, seL4는 그 보호 도메인을 멈추고 부모에게 폴트를 보고합니다.

• 슈퍼바이저는 다른 부분들의 부모입니다. 각 폴트를 받아 보고하고, 보드를 재설정해 시스템이 깨끗한 상태로 다시 시작하게 합니다. 슈퍼바이저는 구현되어 있으며 QEMU 테스트 시스템에서 테스트됩니다.
• 페일세이프 상태는 폴트가 계속될 때 장치가 들어가는 상태입니다. 기본값으로는 콜드 스타트 이후 네 번째 재시작, 또는 저장소나 업데이트처럼 보안에 민감한 부분의 두 번째 폴트에서 들어갑니다. 슈퍼바이저, 워치독, 그리고 가능한 경우 디스플레이만 계속 동작하며, 전원이 꺼진 상태에서 시작하는 콜드 스타트만이 장치를 되돌립니다.
• 워치독 보호 도메인은 다른 모든 부분이 하트비트에 응답하는 동안에만 하드웨어 워치독을 갱신합니다. 하나라도 응답을 멈추면 하드웨어가 보드를 재설정합니다.

메모리와 시간

• 메모리는 이미지를 빌드할 때 고정됩니다. 장치 코드는 아무것도 할당하지 않습니다. 모든 버퍼와 큐는 nowayos-bounded에서 가져온 정해진 크기를 가집니다. 유일한 예외인 TLS 클라이언트는 자기만의 고정된 아레나 안에서 동작합니다.
• 절대 섞이지 않는 두 종류의 시간. 단조 시간은 부팅부터 세며 절대 거꾸로 가지 않습니다. 모든 타임아웃이 이를 씁니다. 날짜와 시각인 벽시계 시간은 인증된 출처에서 옵니다. 둘은 서로 다른 Rust 타입이므로, 한쪽이 필요한 자리에 다른 쪽을 넘길 수 없습니다.

자신만의 시스템 빌드하기

여러분 제품의 시스템과 보호 도메인은 nowayos 안이 아니라 그 옆의 별도 저장소에 둡니다. 그 저장소의 Makefile은 SYSTEM_REPO := $(CURDIR)를 설정하고 NoWayOS의 make 프래그먼트를 포함합니다.

SYSTEM_REPO := $(CURDIR)
include ../nowayos/tools/make/container.mk
include ../nowayos/tools/make/system.mk

그러면 make image, make qemu-test, make qemu-test-all과 각종 검사가 NoWayOS의 개발 컨테이너, 보드 파일, 권한 부여 규칙, 검사 도구를 사용해 그 저장소의 systems/와 pds/에서 동작합니다. 변수는 tools/make/system.mk 맨 위에 설명되어 있습니다. Showcase가 정확히 이 방식으로 빌드됩니다.