검사와 증거

make ci가 무엇을 실행하고 각 검사가 무엇을 보여 주는지, 모든 크레이트가 지키는 기본 규칙, 이미지의 seL4 기록과 자재 명세서를 읽는 방법, 그리고 관문을 빠르게 유지하는 방법.

NoWayOS는 주장을 많이 하지 않으며, 각 주장을 직접 실행할 수 있는 검사로 뒷받침합니다. 이 페이지에서는 각 검사가 무엇을 보여 주고 무엇을 보여 주지 않는지 설명합니다.

명령 하나로 전부

make ci

make ci는 전체 관문을 순서대로 실행합니다. 비밀 정보 스캔, 린트, 테스트, 문서, 데모, no_std 빌드, 라이선스와 보안 권고 검사, 글리프 아틀라스, 자재 명세서, 퍼징과 Kani 증명, 그리고 시스템 검사와 QEMU 부팅입니다. 모든 단계를 통과해야만 변경이 통과합니다.

각 검사가 보여 주는 것

명령	보여 주는 것
`make test`	단위, 속성, 문서, 골든 이미지 테스트. 코드가 테스트가 말하는 대로 동작하고, 모든 화면이 승인된 그대로 그려짐을 보여 줍니다
`make lint`	rustfmt와 clippy. 경고를 오류로 취급합니다
`make nostd`	모든 장치 크레이트가 표준 라이브러리 없이 베어 메탈(`aarch64-unknown-none`)용으로 빌드됩니다
`make deny`	모든 워크스페이스가 지켜야 하는 기준선, 이어서 cargo-deny. 라이선스, 출처, 금지된 크레이트, 알려진 보안 권고를 검사합니다
`make secrets`	소스 트리와 모든 커밋을 오프라인으로 스캔해 키와 자격 증명을 찾습니다
`make fuzz`	모든 퍼즈 타깃을 libFuzzer로 빌드해, 생성된 입력으로 각각 `FUZZ_SECONDS`(10초) 동안 실행합니다
`make kani`	Kani의 유계 증명. 가장 긴 레코드 길이까지의 어떤 입력에 대해서도 각 레코드 디코더가 패닉, 오버플로, 범위 밖 읽기를 일으키지 않음을 증명하며, 각 증명이 실패할 수 있음을 보여 주는 변이 검사를 곁들입니다
`make unsafe-audit`	`unsafe` 코드가 승인 목록이 허용하는 곳에만 있습니다
`make pds-miri`	Miri가 `unsafe`가 허용된 크레이트의 테스트를 실행해 정의되지 않은 동작을 검사합니다
`make sbom`	모든 워크스페이스의 CycloneDX 자재 명세서
`make image-sbom SYSTEM=NAME`	이미지와 그 자재 명세서. 커널, 로더, 모니터, 모든 보호 도메인과 각각에 든 크레이트, 그리고 그 해시
`make sel4-config-check`	기록된 seL4 검증 상태가 고정된 Microkit SDK에 해당하는 것과 일치합니다
`make qemu-test-all`	모든 시스템이 자신이 나열한 각 구성으로 QEMU에서 부팅하고, 기대 출력 파일이 말하는 내용을 출력합니다

유계 증명은 명시된 입력 크기까지의 증명이지, 있을 수 있는 모든 입력에 대한 증명이 아닙니다. 퍼징은 크래시를 찾아내지만, 크래시가 없다는 것을 보여 줄 수는 없습니다. 테스트는 테스트한 경우만 보여 줍니다. 각각은 실제로 보여 주는 만큼의 가치가 있습니다.

모든 크레이트가 지키는 기본 규칙

이것은 지침이 아니라, 모든 워크스페이스에 적용되는 린트와 검사입니다.

unsafe 금지. 단, 하드웨어나 메모리에 직접 접근하는, 승인된 짧은 목록의 크레이트와 파일은 예외입니다. 목록에 추가하려면 명시된 이유와 검토가 필요합니다.
외부 입력으로 인한 패닉 금지: 라이브러리 코드에서 unwrap, expect, panic!을 쓰지 않고, 검사하지 않은 인덱싱이나 산술 연산도 쓰지 않으며, 린트의 모든 예외에는 이유를 밝힙니다.
장치 크레이트는 no_std이며 아무것도 할당하지 않습니다. 릴리스 빌드에서도 오버플로 검사를 유지하며, 패닉이 나면 계속 진행하지 않고 해당 부분을 멈춥니다.
파서는 너무 큰 입력을 복사하기 전에 거부하고, 타입 지정 오류를 반환하며, 속성 테스트와 퍼즈 타깃을 갖춥니다.
어디에도 비밀 정보 금지. 개발용 키조차 안 됩니다. 테스트 키는 테스트를 실행할 때 만들어지며 절대 저장하지 않습니다.

이미지 기록 읽기

모든 이미지는 build/BOARD/SYSTEM/에 기록되며, 옆에 기록 두 개가 함께 생깁니다.

sel4-config.txt 파일은 이미지, 해시, 보드, Microkit SDK, 커널을 밝힌 다음, 이미지가 seL4의 증명에 비추어 어디에 있는지 이유마다 status: 줄 하나로 말하고, 이를 결정하는 각 커널 옵션을 검증 구성의 값과 나란히 나열합니다. 디버그 커널은 개발 빌드입니다. 멀티코어 커널이나 혼합 임계성 커널, 또는 seL4 목록에 없는 보드는 seL4의 증명 범위 밖입니다. 모든 옵션이 일치하는 커널이라도 결코 “검증됨”이라고 부르지 않습니다. 기록은 사실을 밝히고 거기서 멈춥니다.

sbom.cdx.json 파일은 이미지의 CycloneDX 소프트웨어 자재 명세서입니다. 이미지가 무엇으로 이루어졌는지를 각 보호 도메인의 크레이트 하나하나까지, 저마다 sha256과 함께 담습니다.

관문을 빠르게 유지하기

증명과 퍼징 전체는 오래 걸리므로, 평소의 make ci는 변경이 영향을 미치는 곳에서만 Kani, 퍼징, Miri를 실행합니다. 변경을 그에 의존하는 모든 크레이트까지 따라가며, 마지막으로 통과한 뒤 입력이 바뀌지 않은 검사는 건너뜁니다. make ci CI_SCOPE=full은 캐시 없이 전부 실행하며, make kani, make fuzz, make pds-miri는 항상 전체를 실행합니다.

Kani는 자원을 가장 많이 먹는 단계입니다. 증명 작업마다 약 10 GB의 메모리가 주어지며, KANI_JOBS로 동시에 실행할 작업 수를 정합니다. make kani가 메모리 부족으로 실패하면 Podman 가상 머신에 메모리를 더 주거나 KANI_JOBS=1로 설정하십시오.