애플리케이션에서 이미지까지
NoWayOS 장치는 설정하는 것이 아니라 빌드하는 것입니다. 네 단계를 거치면 여러분의 코드가 한 가지 일을 하는 장치가 되며, 단계마다 확인할 수 있는 결과물이 남습니다.
애플리케이션 작성
Rust로, 하나 이상의 보호 도메인으로 작성합니다. 화면은 NoWayOS의 작은 선언형 UI 코어로 만들거나, React로 디자인한 뒤 Screen Compiler로 빌드할 때 변환합니다.
시스템 기술
Microkit 시스템 기술서는 모든 보호 도메인, 메모리 영역, 채널, 인터럽트를 선언합니다. 그 옆의 권한 부여 파일에는 시스템이 부여하는 모든 것이, 기대 출력 파일에는 실행할 때 반드시 출력해야 하는 내용이 나열됩니다.
systems/hello.system systems/hello.grants systems/hello.expect빌드
개발 컨테이너 안에서 빌드합니다. 빌드는 권한 부여를 기술서와 대조해 검사한 뒤, 소프트웨어 자재 명세서와 seL4 구성 기록을 곁들여 이미지를 기록합니다.
make image SYSTEM=hello부팅하고, 스스로 검사하게 하기
먼저 QEMU에서: 시스템은 헤드리스로 부팅하며, 기대 출력 파일에 나열된 모든 줄을 순서대로 출력해야 하고 그 파일이 금지하는 내용은 하나도 출력해서는 안 됩니다. 그다음 Raspberry Pi 5에서 같은 파일과 대조해 검사합니다.
make qemu-test SYSTEM=hello
봉인된 구획
NoWayOS 시스템의 각 부분(화면, 입력, 네트워크, 여러분의 애플리케이션)은 seL4 마이크로커널 위에서 저마다의 보호 도메인으로 실행됩니다. 보호 도메인은 자기만의 메모리를 가지며, 시스템 기술서가 부여한 케이퍼빌리티만 보유합니다. 케이퍼빌리티는 문 하나만 여는 출입 카드와 같습니다. seL4가 이를 강제하므로 각 부분은 받은 것에만 접근하며, 한 부분의 버그는 그 부분 안에 머물도록 설계되어 있습니다.
- 슈퍼바이저는 다른 부분의 폴트를 받아, 폴트를 일으킨 부분을 멈추고 시스템을 깨끗한 상태로 다시 시작합니다. 폴트가 계속되면 장치는 페일세이프 상태에 들어가며, 콜드 스타트로만 되돌아옵니다.
- 워치독 보호 도메인은 다른 모든 부분이 하트비트에 응답하는 동안에만 하드웨어 워치독을 갱신합니다.
- 역할은 각 부분이 받을 수 있는 것을 제한합니다. 빌드는 어떤 부분의 역할이 절대 가져서는 안 되는 권한 부여를 거부합니다. 화면을 그리기만 해야 하는 부분에 장치를 주는 경우가 그렇습니다.
검사 전에 복사하는 타입 지정 메시지
보호 도메인은 레이아웃이 명시된 고정 크기의 버전 관리 레코드로 대화하며, 이 레코드는 공유 메모리 위의 단일 생산자 링으로 전달됩니다. 모든 레코드는 검사하기 전에 공유 메모리 밖으로 복사되므로, 보낸 쪽이 검사와 사용 사이에 내용을 바꿀 수 없습니다.
외부 입력을 다루는 모든 파서는 퍼징을 거치고 절대 패닉하지 않도록 만들어졌으며, 모든 메시지 디코더에는 Kani 모델 검사기로 만든 유계 증명이 있습니다.
브라우저 없는 네이티브 화면
사용자 인터페이스는 작은 선언형 코어입니다. 레이아웃, 포커스, 히트 테스트를 제한된 메모리 안에서 처리하고, Rust 라이브러리 embedded-graphics로 그리며, 바뀐 부분만 다시 그립니다. 텍스트는 빌드할 때 미리 그려 둔 글리프 아틀라스에서 가져오므로, 장치는 글꼴 파일을 해석할 일이 없습니다. 애플리케이션은 키, 포인터, 터치 이벤트만 볼 뿐, USB를 비롯한 어떤 장치 프로토콜도 보지 않습니다.
디자이너는 계속 React로 작업할 수 있습니다. Screen Compiler는 지원하는 부분 집합에 맞춰 작성된 화면을 빌드할 때 Rust로 변환하며, 부분 집합을 벗어나는 것은 비슷하게 흉내 내는 대신 거부합니다.
들어 있는 것
| 영역 | NoWayOS가 제공하는 것 |
|---|---|
| 런타임 | Microkit과 rust-sel4 기반의 보호 도메인 패턴, 폴트가 난 부분을 멈추고 시스템을 깨끗이 다시 시작하며 폴트가 반복되면 페일세이프 상태로 들어가는 슈퍼바이저, 워치독 |
| 메시지 | 전송 레이아웃이 명시된 타입 지정 레코드, 공유 메모리 위의 단일 생산자 링 |
| 드라이버 | 디스플레이(QEMU의 ramfb, Raspberry Pi 5의 프레임버퍼), 입력(virtio, USB 키보드·마우스·태블릿), 네트워크(virtio-net, Pi 5의 이더넷), USB 호스트(xHCI), UART, 타이머, Pi 5의 팬 |
| 네트워킹 | DHCP와 TCP를 갖추고 시스템이 허용한 목적지에만 연결하는 smoltcp 기반 IP 스택, rustls와 RustCrypto 기반의 TLS 1.3 클라이언트 |
| 시간과 신뢰 | 절대 섞이지 않는 별개 타입으로 다루는 단조 시간과 벽시계 시간, ECDSA P-256 서명 검사, 서명된 업데이트의 레코드, 상태 검사를 거친 하드웨어 난수원에서 얻는 시드 |
| 사용자 인터페이스 | 레이아웃, 포커스, 히트 테스트를 갖추고 메모리 사용이 제한된 선언형 UI 코어, embedded-graphics 기반 렌더러, 미리 그려 둔 글리프 아틀라스와 아이콘 |
| 도구 | 개발 컨테이너, 제품 저장소가 빌드에 쓰는 make 프래그먼트, 권한 부여·unsafe·라이선스·비밀 정보 검사, SBOM과 릴리스 증거 도구, QEMU와 Raspberry Pi 실행기 |
하드웨어
| 어디서 | 역할 |
|---|---|
| QEMU (AArch64) | 모든 시스템이 개발 컨테이너 안의 이곳에서 먼저 부팅하고, 자신의 출력을 스스로 검사합니다 |
| Raspberry Pi 5 | 누구나 살 수 있는 저렴한 레퍼런스 보드. 현재 사용자 인터페이스, USB 입력, 타이머, 워치독이 이 보드에서 동작합니다 |
| NXP i.MX8 | 하드웨어 신뢰 루트를 갖춘, 프로덕션용으로 계획한 하드웨어. 아직 지원하지 않습니다 |
NoWayOS는 Apple 실리콘(arm64) 컴퓨터에서 개발됩니다. x86-64에서도 개발 이미지의 패키지 버전은 고정되고 검토되었지만, 그곳에서 이미지를 처음부터 끝까지 빌드하고 테스트해 보지는 아직 않았습니다.
기반 기술
NoWayOS는 다른 이들의 작업 위에 서 있으며, 이를 밝혀 둡니다. seL4, Microkit, rust-sel4, seL4 Device Driver Framework의 네트워크 큐, smoltcp, rustls, RustCrypto, embedded-graphics.