변경할 때마다 저희 빌드를 직접 공격합니다

어떤 보안 테스트에든 불편한 질문이 하나 있습니다. 그 테스트는 실패한 적이 있습니까? 한 번도 실패한 적 없는 테스트가 통과하는 이유는 시스템이 건전해서일 수도 있고, 테스트가 아무것도 보지 못해서일 수도 있습니다. 밖에서 보면 둘은 완전히 똑같아 보입니다.

그래서 NoWayOS는 보안을 테스트하는 데서 그치지 않습니다. 변경할 때마다 보안을 공격하고, 그 공격이 막히는지 확인합니다.

내 것이 아닌 것에 손을 뻗기

NoWayOS 시스템의 각 부분은 seL4 위의 자기 구획에서 실행되며, 부여받은 것만 가집니다. 격리 테스트는 그 경계를 넘는 프로브를 일부러 보냅니다. 어떤 프로브는 받은 적 없는 주소를 읽습니다. 어떤 프로브는 읽기만 허용된 페이지에 씁니다. 사용자 인터페이스가 가진 것과 정확히 같은 것을 가진 프로브는, 인터페이스가 읽기만 할 수 있는 디스플레이 제어 페이지에 쓰려고 합니다. 네트워크 클라이언트가 가진 것과 정확히 같은 것을 가진 또 다른 프로브는 네트워크 드라이버의 메모리에 쓰려고 합니다.

seL4는 이 모두를 막아야 하고, 관계없는 부분은 아무 영향 없이 계속 실행되어야 합니다.

실패하도록 만든 테스트

여기에 반전이 있습니다. 사용자 인터페이스의 격리 테스트 옆에는 권한 부여 하나를 일부러 넓힌 변형이 있습니다. 인터페이스의 대역에게 디스플레이의 비공개 페이지를 주는 것입니다. 이 변형의 테스트는 반드시 실패해야 합니다. 만약 통과한다면 격리 테스트는 아무것도 보지 못하는 것이고, 빌드가 그렇게 알려 줍니다.

같은 생각이 나머지 검사에도 이어집니다. 부분 사이 메시지의 모든 디코더에는 패닉, 오버플로, 범위 밖 읽기를 일으키지 않는다는, 모델 검사기 Kani의 유계 증명이 있습니다. 그런 다음 뮤테이션 검사가 디코더를 일부러 망가뜨려, 증명이 이를 알아차린다는 것을 보입니다. 외부 입력의 모든 파서는 적대적인 데이터로 퍼징합니다.

이 모두가 모든 변경이 통과해야 하는 게이트인 make ci의 일부입니다. 격리 테스트는 매번 실행되고, 증명이나 퍼징은 그것이 다루는 코드가 바뀔 때마다 다시 실행됩니다.

손이 닿지 않는 게이트

게이트는 그것을 바꿀 수 있는 손만큼만 강합니다. 그래서 NoWayOS에 대한 모든 기여가 통과해야 하는 검사는 별도의 공개 저장소인 Defence Agent에 정의되어 있습니다. 게이트를 건드리는 풀 리퀘스트는 메인테이너가 볼 수 있도록 표시됩니다.

Defence Agent는 자기 자신도 같은 방식으로 테스트합니다. 리뷰어가 놓칠 만한 것을 하나씩 숨긴, 심어 둔 풀 리퀘스트 스무 개입니다. 주석 안에 숨겨진 오른쪽에서 왼쪽으로 쓰는 텍스트, 닮은꼴 키릴 문자로 바꿔 넣은 글자 하나, git 저장소에서 직접 가져오는 의존성, 신뢰할 수 없는 코드를 실행하게 될 워크플로가 있습니다. 이들은 모두 잡혀야 하고, 실제 과거 변경 세 건은 통과해야 합니다.

형용사가 아니라 증거

이 가운데 어느 것도 장치를 “해킹 불가능”하게 만들지 않습니다. 그런 것은 없으며, 저희는 결코 그렇게 말하지 않겠습니다. 대신 증거를 드립니다. 무엇을 시도했고 무엇이 막혔는지의 기록, 그리고 그것을 보여 주는 명령입니다. 실제 이미지 하나의 증거나 게이트 자체를 읽어 보십시오.