어려운 말을 쉬운 말로.

NoWayOS의 전체 툴체인을 담은, 버전이 고정된 컨테이너 이미지입니다. Rust 툴체인, Microkit SDK, QEMU, 검사 도구가 들어 있습니다. 모든 make 타깃이 이 안에서 실행되므로, 여러분의 컴퓨터에는 Podman과 make(그리고 Raspberry Pi 5를 다룰 Python 3.11)만 있으면 됩니다.

부여받지 않은 것에 접근하려 하는 시스템으로, seL4가 이를 막아야 합니다. 일부러 권한 부여를 넓힌 변형은 반드시 실패해야 하며, 이로써 테스트가 실패할 수 있음을 보여 줍니다.

공격자가 장치를 공격하는 데 이용해 볼 수 있는 모든 것. 코드, 서비스, 인터페이스, 입력이 여기에 속합니다. 코드와 기능이 적을수록 공격 표면도 줄어듭니다.

위험한 일을 처음부터 넣지 않았기 때문에 그런 일을 할 수 없는 장치를 만드는 것. NoWayOS의 접근 방식입니다.

systems/NAME.grants. 시스템이 부여하는 모든 것을 한 줄에 사실 하나씩 적은 파일입니다. 우선순위, 예산, 메모리, 장치, 인터럽트, 채널이 들어갑니다. 시스템 기술서와 권한 부여 파일이 어긋나면 빌드가 실패합니다.

빌드할 때 글꼴을 글자별 이미지로 미리 그려 둔 것. 덕분에 장치는 글꼴 파일을 해석하지 않고도 텍스트를 그립니다.

systems/NAME.expect. 시스템이 순서대로 출력해야 하는 줄과, 어디에든 나타나면 테스트를 실패시키는 텍스트를 담은 파일입니다. 같은 파일로 QEMU에서도, Raspberry Pi 5에서도 시스템을 검사합니다.

부팅 시점부터 세는 시간으로, 따로 설정하지 않으며 절대 거꾸로 가지 않습니다. NoWayOS의 모든 타임아웃은 이 시간을 쓰며, 벽시계 시간과 절대 섞이지 않습니다.

가능한 한 작게 유지한 커널로, 드라이버, 네트워킹, 화면은 커널 밖에서 저마다의 구획에 담겨 실행됩니다. seL4가 그 예입니다.

버퍼 끝을 넘어 읽거나 해제된 메모리를 다시 사용하는 것 같은 실수입니다. Microsoft와 Google은 각각 자사의 심각한 보안 버그 중 약 70%가 이런 종류라고 밝혔습니다. 안전한 Rust는 이런 버그를 원천적으로 배제합니다.

인증된 출처에서 얻는 날짜와 시각입니다. NoWayOS는 이를 다른 타입으로 두어 단조 시간과 분리합니다.

제조사가 서명하지 않은 소프트웨어는 장치가 시작을 거부하는 것. NoWayOS에서는 프로덕션 하드웨어에서 지원할 계획이며, 아직 구현되지 않았습니다.

Microkit 시스템의 격리된 한 부분. 자기만의 메모리를 가지며, 명시적으로 부여받은 케이퍼빌리티만 보유하는 프로그램입니다. NoWayOS의 봉인된 구획이 바로 이것입니다.

메시지를 검증하기 전에 공유 메모리 밖으로 복사한다는 규칙입니다. 그래서 보낸 쪽이 검사와 사용 사이에 메시지를 바꿀 수 없습니다. 이중 페치를 막습니다.

설정을 바꿔 범용 장치를 더 안전하게 만드는 것. 기능은 여전히 남아 있으며, 버그 하나가 모든 설정을 우회할 수 있습니다.

다른 부분의 폴트를 받아 보고하고, 시스템을 깨끗이 다시 시작하는 보호 도메인입니다.

시스템의 모든 보호 도메인, 메모리 영역, 채널, 인터럽트를 선언하는 Microkit XML 파일입니다. 이 파일이 곧 시스템의 보안 설계이므로, 이 파일의 변경은 보안 설계의 변경으로 검토합니다.

어떤 보안 속성이 성립하려면 올바르게 동작해야 하는 모든 것. NoWayOS 시스템에서는 seL4 커널, Microkit 로더와 모니터, 그리고 그 속성이 의존하는 보호 도메인입니다.

소프트웨어가 주기적으로 갱신하지 않으면 보드를 재설정하는 하드웨어 타이머입니다. NoWayOS의 워치독 보호 도메인은 다른 모든 부분이 하트비트에 응답하는 동안에만 이를 갱신합니다.

장치가 어떤 소프트웨어로 시작했는지를 원격 서비스에 암호학적으로 증명하는 것. 부팅 때 무엇을 불러왔는지 보여 줄 뿐, 그 뒤에 일어난 모든 일을 보여 주지는 않습니다. NoWayOS에서는 프로덕션 하드웨어에서 지원할 계획이며, 아직 구현되지 않았습니다.

명시된 크기까지의 모든 입력에 대해 어떤 속성이 성립함을 보이는 증명입니다. NoWayOS는 Kani를 사용해 메시지 디코더를 이 방식으로 증명합니다.

코드가 공유 메모리의 데이터를 검사한 뒤 다시 읽는 바람에, 그 사이에 상대편이 데이터를 바꿀 수 있게 되는 버그입니다. 복사 후 검사로 막습니다.

소프트웨어가 명세를 충족한다는 것을 컴퓨터로 검사한 수학적 증명입니다. seL4는 특정 구성에 대해 이를 갖추고 있습니다. NoWayOS 자체의 코드는 그 대신 Rust, 격리, 테스트, 유계 증명에 의존합니다.

Microkit에서 두 보호 도메인 사이에 선언한 연결로, 알림(데이터 없는 신호이며 인터럽트도 여기에 속합니다)과 보호된 프로시저 호출에 쓰입니다.

seL4에서 커널 객체 하나와 그에 대한 권리를 지정하는, 위조할 수 없는 토큰입니다. 문 하나만 여는 출입 카드와 같습니다. 보호 도메인은 자신의 케이퍼빌리티가 지정한 것만 건드릴 수 있습니다.

재설정과 달리, 전원이 꺼진 상태에서 시작하는 것. NoWayOS 장치를 페일세이프 상태에서 되돌리는 방법은 콜드 스타트뿐입니다.

레이아웃이 명시된 고정 크기 레코드로, 공유 메모리를 통해 보호 도메인 사이에 전달되고 받을 때 검사됩니다. 복사 후 검사를 참고하십시오.

생성한 입력 수백만 개로 파서를 테스트해, 그중 하나가 크래시를 일으키거나 검사를 깨뜨릴 때까지 계속하는 방법입니다. 외부 입력을 다루는 NoWayOS의 모든 파서에는 퍼즈 타깃이 있습니다.

폴트가 계속될 때 NoWayOS 장치가 들어가는 상태입니다. 콜드 스타트 전까지 슈퍼바이저, 워치독, 그리고 가능한 경우 디스플레이만 계속 동작합니다.

보호 도메인이 커널이 허용하지 않는 일을 하거나 패닉할 때 seL4가 보고하는 것. 해당 부분은 폴트 핸들러가 조치할 때까지 멈춘 채로 있습니다.

스케줄링 예산과 주기를 갖춘 seL4 구성으로, Microkit이 이를 빌드합니다. AArch64 증명은 진행 중이므로, 현재 seL4의 완료된 증명 범위 안에 있는 NoWayOS 이미지는 없습니다.

소프트웨어 자재 명세서를 위한 개방형 표준 형식입니다. NoWayOS는 모든 워크스페이스와 모든 시스템 이미지에 대해 이 형식의 명세서를 작성합니다. SBOM을 참고하십시오.

Raspberry Pi의 USB-시리얼 어댑터입니다. Raspberry Pi 5의 디버그 커넥터에 연결하면 부팅 로그를 전달하고 테스트 이미지를 올립니다.

운영체제 그래픽 스택이 없는 장치를 위한 Rust 2D 그래픽 라이브러리입니다. NoWayOS의 사용자 인터페이스는 이것으로 그립니다.

NXP의 산업용 Arm 프로세서 제품군으로, NoWayOS가 프로덕션 하드웨어로 계획하고 있습니다. 아직 지원하지 않습니다.

한도까지의 모든 입력에 대해 속성을 증명하는 Rust용 모델 검사기입니다. NoWayOS는 이를 사용해 메시지 디코더가 패닉, 오버플로, 범위 밖 읽기를 일으키지 않음을 증명합니다.

시스템 기술서에 선언된 보호 도메인으로 구성하는 정적 seL4 시스템을 위한, seL4 재단의 프레임워크입니다.

정의되지 않은 동작을 찾아내는 Rust용 인터프리터입니다. NoWayOS는 unsafe 코드가 허용된 소수의 크레이트에 이를 실행합니다.

오픈 소스 머신 에뮬레이터입니다. 모든 NoWayOS 시스템은 하드웨어에 올라가기 전에 여기서 부팅하고 자신의 출력을 스스로 검사합니다.

NoWayOS가 레퍼런스 하드웨어로 쓰는 저렴한 보드입니다.

안전한 코드에서는 메모리 안전성 버그가 원천적으로 배제되는 프로그래밍 언어입니다. NoWayOS 자체의 코드는 처음부터 끝까지 Rust입니다.

Microkit 보호 도메인을 작성하는 크레이트를 포함한, seL4 재단의 Rust 지원입니다.

Rust로 작성된 TLS 라이브러리입니다. NoWayOS의 TLS 1.3 클라이언트는 RustCrypto와 함께 이를 바탕으로 만들어졌습니다.

소프트웨어 자재 명세서. 소프트웨어를 이루는 모든 구성 요소와 버전의 목록입니다. NoWayOS는 모든 워크스페이스와 모든 시스템 이미지에 대해 CycloneDX 형식으로 작성합니다.

지원 부분 집합에 맞춰 TSX로 작성한 React 화면을 NoWayOS 사용자 인터페이스용 Rust로 변환하는, NoWayOS의 빌드 시점 도구입니다. 부분 집합을 벗어나는 것은 비슷하게 흉내 내지 않고 거부합니다.

seL4 Device Driver Framework. 공유 메모리 큐를 사용하는 Microkit 드라이버의 참조 설계입니다. NoWayOS의 네트워크 큐는 이를 따릅니다.

seL4 재단이 관리하는 약 10,000줄 규모의 마이크로커널로, 특정 구성에 대해 정확성과 보안에 관한 기계 검사 증명을 갖추고 있습니다. NoWayOS는 그 위에서 실행됩니다.

모든 NoWayOS 이미지 옆에 작성되는 기록입니다. 이미지의 seL4 구성과, 그 구성이 seL4의 완료된 증명 범위 안에 있는지를 담습니다.

무엇이든 실행하도록 만든 뒤 한 가지로 잠근 운영체제가 아니라, 한 장치의 한 가지 일을 위해 만든 운영체제입니다. 세 가지를 갖춰야 Single Purpose OS입니다. 한 가지 일을 위해 만들어졌고(이미지에는 애플리케이션, 그것이 쓰는 드라이버, 커널만 있고 다른 것은 없습니다), 내부가 구획마다 봉인되어 있으며(각 부분은 저마다의 구획에서 부여받은 것에만 접근합니다), 풀이 과정을 보여 줍니다(안에 무엇이 있는지에 대한 증거가 함께 제공됩니다). 설정에 의한 보안 시스템을 앱 하나에 잠그는 키오스크 모드와는 다릅니다. NoWayOS는 Single Purpose OS, 다른 할 일이 없는 컴퓨터입니다.

실행 중에 메모리를 할당하지 않는 Rust TCP/IP 스택입니다. NoWayOS의 네트워크 스택은 이를 바탕으로 만들어졌습니다.

컴파일러가 메모리 안전성을 검사할 수 없는 Rust 코드입니다. 검사가 강제하는, 검토를 거친 짧은 목록의 크레이트를 제외하면 모든 NoWayOS 크레이트에서 금지됩니다.