보안

제 할 일만 합니다.

NoWayOS 장치는 할 일에 필요 없는 것은 빼고, 남은 것은 구획마다 봉인합니다. 이 페이지는 그 바탕이 무엇인지, 무엇이 증명되었고 무엇이 아직 증명되지 않았는지, 그리고 무엇을 여러분이 제대로 갖춰야 하는지 설명합니다.

빠진 것

NoWayOS 이미지에는 애플리케이션, 그 애플리케이션이 쓰는 드라이버, 그리고 seL4 마이크로커널이 들어 있습니다. 브라우저 엔진도, 윈도 시스템도, 셸도, 패키지 관리자도, 사용자 계정도 없습니다. 처음부터 넣지 않았으니 악용하거나 패치하거나 잘못 설정할 대상도 없습니다. NoWayOS는 불필요한 소프트웨어와 서비스를 줄이도록 설계되었습니다. 할 일에 필요하지 않으면 이미지에 넣지 않습니다.

이름의 뜻이 바로 이것입니다. 처음부터 넣지 않은 것은 악용할 길도 없습니다. 이는 무엇이 없는지에 관한 말이지, 아무 문제도 생기지 않는다는 약속이 아닙니다. 들어 있는 것에는 여전히 버그가 있을 수 있습니다. 저희가 주장하는 것은 그 양이 훨씬 적다는 것, 그리고 버그가 자기 구획 안에 머문다는 것입니다.

범용 시스템을 잠그는 것은 설정에 의한 보안입니다. 잠가 둔 기능은 여전히 존재하고, 버그 하나가 모든 설정을 우회할 수 있습니다. NoWayOS는 구조에 의한 보안을 지향합니다. 그런 기능은 애초에 없었습니다.

결함을 가두는 방식

각 부분은 자기만의 메모리를 가진 저마다의 보호 도메인에서 실행되며, 시스템 기술서가 부여한 케이퍼빌리티만 보유합니다. seL4가 이를 강제합니다.
모든 권한 부여는 시스템의 권한 부여 파일에 나열되며, 기술서가 파일에 없는 것을 부여하거나 그 반대인 경우 빌드가 실패합니다. 권한 부여를 넓히는 변경은 보안 변경으로 검토합니다.
부분 사이의 메시지는 고정 크기 레코드이며 검사하기 전에 공유 메모리 밖으로 복사되므로, 보낸 쪽이 검사를 통과한 레코드를 바꿀 수 없습니다.
입력은 검사하기 전까지 적대적인 것으로 간주합니다. 외부 입력을 다루는 모든 파서는 퍼징을 거치고 절대 패닉하지 않도록 만들어졌으며, 애플리케이션은 키, 포인터, 터치 이벤트만 볼 뿐 장치 프로토콜은 보지 않습니다.
슈퍼바이저는 폴트를 일으킨 부분을 멈추고 시스템을 깨끗이 다시 시작합니다. 폴트가 반복되면 장치는 콜드 스타트 전까지 페일세이프 상태에 머뭅니다.

seL4의 증명이 다루는 것과 다루지 않는 것

seL4는 약 10,000줄 규모의 마이크로커널로, 정확성과 보안에 관한 기계 검사 증명을 갖추고 있습니다. 이 증명은 보기 드문 성취이며, 특정 플랫폼의 특정 구성에 대해 성립합니다. 정확한 입장은 다음과 같습니다.

NoWayOS는 seL4 마이크로커널 위에서 실행됩니다. seL4는 저희 하드웨어의 특정 구성에 대해 정확성과 보안에 관한 기계 검사 증명을 갖추고 있습니다. NoWayOS는 seL4의 혼합 임계성 구성을 사용하며, 이 구성의 증명은 진행 중입니다.

플랫폼: seL4의 AArch64 검증 구성 목록에는 Raspberry Pi 5와 NXP의 i.MX8M Mini, Plus, Quad가 올라 있습니다.
스케줄링: Microkit은 seL4의 혼합 임계성(MCS) 커널을 빌드하며, 이 커널의 AArch64 증명은 진행 중입니다. 따라서 현재 seL4의 완료된 증명 범위 안에 있는 NoWayOS 이미지는 없습니다.
코어: 증명은 단일 코어 커널을 대상으로 합니다. 여러 코어를 쓰는 이미지는 증명 범위 밖에 있으며, 스스로 그렇게 밝힙니다.
커널 위: Microkit의 도구와 NoWayOS의 보호 도메인, 드라이버는 seL4의 증명 범위에 포함되지 않습니다. 이들의 보증은 Rust, 격리, 검토, 테스트, 그리고 NoWayOS 자체의 유계 증명에서 나옵니다.

모든 이미지는 옆에 있는 sel4-config.txt에 자신의 구성을 기록합니다. hello 시스템의 개발 빌드 기록이 스스로에 대해 말하는 내용은 이렇습니다.

system: hello
board: qemu_virt_aarch64
configuration: debug
sdk: Microkit 2.3.1
status: development build: a debug kernel, with printing and debug interfaces, outside seL4's proofs
status: outside seL4's completed proofs: a mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress
status: outside seL4's proofs: a platform that is not on seL4's AArch64 verified list

커널이 검증 구성의 모든 옵션과 일치하는 이미지라 해도, 여기서는 “검증됨”이라고 부르지 않습니다. 기록은 사실을 밝히고, 사실이면 충분합니다.

증거, 그리고 각각의 명령

이 페이지의 모든 주장에는 증거가 따르고, 모든 증거는 누구나 개발 컨테이너에서 실행할 수 있는 명령에서 나옵니다. make ci는 이를 순서대로 실행하고, make ci CI_SCOPE=full은 모든 증명과 퍼즈 타깃을 실행합니다. 각 항목은 검사와 증거에서 설명합니다.

주장	증거	실행하기
모든 권한 부여가 기록되어 있습니다.	각 시스템의 권한 부여 파일. 빌드할 때마다 시스템 기술서와 대조해 검사합니다.	`make qemu-test SYSTEM=hello`
어떤 부분도 부여받지 않은 것에는 접근할 수 없습니다.	탐침이 부여받지 않은 읽기와 쓰기를 시도하고 seL4가 이를 막아야 하는 격리 테스트, 그리고 일부러 권한 부여를 넓혀 반드시 실패해야 하는 변형.	`make qemu-test SYSTEM=isolation-test`
메시지 디코더의 속성은 한도 내 모든 입력에서 성립합니다.	모든 메시지 레코드 디코더에 대한 Kani 증명, 그리고 증명이 실패할 수 있음을 보여 주는 변이 검사.	`make kani`
외부 입력 파서는 악의적인 입력을 견뎌 냅니다.	신뢰할 수 없는 입력을 다루는 모든 파서마다 퍼즈 타깃이 있습니다. 한 번 고친 크래시는 회귀 테스트가 됩니다.	`make fuzz`
unsafe 코드는 승인된 곳에만 있습니다.	unsafe 코드를 쓸 수 있는 소수의 크레이트와 파일을 담은 허용 목록. make ci가 이를 강제하며, 해당 크레이트에는 Miri를 실행합니다.	`make unsafe-audit`
모든 구성 요소가 파악되어 있습니다.	모든 워크스페이스와 모든 시스템 이미지의 CycloneDX 소프트웨어 자재 명세서. 구성 요소마다 해시가 있습니다.	`make image-sbom SYSTEM=hello`
라이선스와 보안 권고를 검사합니다.	모든 워크스페이스에 cargo-deny를 실행해 라이선스, 출처, 금지된 크레이트, 알려진 보안 권고를 검사합니다.	`make deny`
코드에 비밀 정보가 없습니다.	소스 트리와 모든 커밋을 오프라인으로 스캔해 키와 자격 증명을 찾습니다.	`make secrets`
각 이미지의 seL4 구성이 기록되어 있습니다.	모든 이미지 옆에 있는 sel4-config.txt, 그리고 기록의 기준값이 고정된 Microkit SDK와 일치하는지 확인하는 검사.	`make sel4-config-check`

이미지 하나의 증거 읽기

증거가 어떤 모습인지 보려고 무언가를 빌드할 필요는 없습니다. 실제 이미지 하나의 증거를 모두 실었습니다. 2026년 11월 1일 QEMU용으로 빌드한, 클릭할 수 있는 사용자 인터페이스 ui-interactive입니다.

소프트웨어 자재 명세서(CycloneDX 1.5): seL4 커널과 Microkit 로더부터 모든 보호 도메인의 모든 크레이트까지 62개 구성 요소를 저마다 SHA-256과 함께 담았습니다.
seL4 구성 기록: 실행하는 커널을 seL4의 검증 구성과 옵션별로 대조하고, 증명 범위를 벗어나는 지점을 분명히 밝힙니다.
시스템 기술서: Microkit이 빌드하는 그대로의 모든 보호 도메인, 메모리 영역, 인터럽트, 채널.
권한 부여 파일: 같은 권한 부여를 한 줄에 사실 하나씩 적은 것으로, 빌드가 기술서와 대조해 검사합니다.
이 이미지가 그리는 화면. 테스트를 실행할 때마다 이 승인된 이미지와 픽셀 단위로 비교합니다.

여러분의 몫으로 남는 것

NoWayOS는 플랫폼이지, 인증받은 제품이 아닙니다. 안전한 장치는 어떻게 배포하고 운영하느냐에도 달려 있으며, 그 부분은 장치를 만들고 운영하는 쪽의 몫입니다.

물리적 보안. 꽂아 넣은 장치 하나, 전원 케이블에 닿은 손 하나로도 장치는 여전히 작동을 멈출 수 있습니다. 외함, 포트, 전원은 NoWayOS 위에 만드는 제품의 설계에 속합니다.
각 시스템이 부여하는 것. NoWayOS는 시스템과 권한 부여 파일이 일치하는지 검사합니다. 그 권한 부여가 할 일에 적절한지는 설계상의 결정이며, 설계 결정으로서 검토해야 합니다.
네트워크와 백엔드. 장치는 시스템이 허용한 목적지에만 연결합니다. 그 서비스가 받은 것을 어떻게 다루는지는 해당 서비스가 지켜야 할 몫입니다.
키와 업데이트. 안전하게 되돌릴 수 있는 서명된 업데이트는 설계되었지만 아직 구현되지 않았습니다. 서명 키를 누가 보관하고 릴리스를 어떻게 승인할지는 운영상의 결정입니다.
인증. NoWayOS에서 실행되는 규제 대상 제품은 각자 인증을 받습니다. NoWayOS는 그 인증에 필요한 증거를 제공하도록 설계되었으며, NoWayOS 자체는 인증받지 않았습니다.

아직 구현되지 않은 것

보안 부팅과 원격 증명은 하드웨어 신뢰 루트를 갖춘 프로덕션 하드웨어의 몫입니다. 둘 다 구현되지 않았습니다.
장치에서 적용하는 서명된 업데이트. 업데이트 레코드와 그 검사는 있지만, 장치에서 업데이트를 적용하는 경로는 아직 없습니다.
Raspberry Pi 5는 개발 보드이며, 보안을 강화한 장치가 아닙니다. 보드를 손에 쥔 사람은 소프트웨어를 바꿔 끼울 수 있고, 이 보드에서는 아직 USB 장치의 메모리 접근이 제한되지 않습니다.

여기서 찾을 수 없는 말

저희는 NoWayOS를 “해킹 불가능”하다거나 “변조 방지”, “방탄”이라고 부르지 않으며, “공격 표면 제로”를 주장하지도 않습니다. 그런 것은 세상에 없고, 그런 말을 보았다면 읽기를 멈추는 게 옳습니다. 이 페이지의 주장은 그보다 작으며, 저마다 증거가 따릅니다.

취약점 신고

취약점은 공개 이슈가 아니라 비공개로 신고해 주십시오. 각 저장소의 SECURITY.md에 설명된 대로, 저장소 Security 탭의 GitHub 비공개 취약점 신고 기능을 이용하거나 security@nowayos.com으로 이메일을 보내 주십시오. 각 부분이 저마다의 구획에서 실행되므로, 결함은 수정되는 동안 그 자리에 머물도록 설계되어 있습니다.