증명이 약속할 수 있는 것

소프트웨어를 신뢰하는 이유는 대개 테스트를 거쳤기 때문입니다. 누군가 잘못될 수 있는 경우를 떠올리고, 시험해 보고, 소프트웨어가 버텨 내는 것을 확인했습니다. 이 방법은 잘 통합니다. 아무도 떠올리지 못한 경우를 만나기 전까지는 말입니다.

증명은 반대쪽에서 출발합니다. 경우를 시험하지 않습니다. 어떤 명제가 모든 경우에 성립한다는 것을 수학으로 보입니다.

시험해 본 경우가 아니라 모든 경우

작은 약속 하나를 예로 들겠습니다. 이 코드는 버퍼의 끝을 넘어 읽지 않는다는 약속입니다. 테스트는 입력을 천 개, 또는 십억 개 넣어 보고, 그중 어느 것도 코드를 무너뜨리지 못했다고 보고할 수 있습니다. 증명은 종류가 다른 말을 합니다. 코드를 무너뜨리는 입력은 없다는 것입니다. 찾지 못한 것이 아니라, 존재하지 않습니다.

그 대가는 엄밀함입니다. 증명에는 코드가 무엇을 해야 하는지를 정확히 적은 진술, 곧 명세가 필요하고, 코드의 모든 줄을 명세와 잇는 논증이 필요합니다. 실제 소프트웨어에서 그 논증은 사람이 눈으로 확인하기에는 너무 깁니다. 그래서 컴퓨터가 검사합니다.

기계가 검사한 증명

“기계 검사”란 바로 그런 뜻입니다. 증명은 증명 보조기라는 프로그램이 읽을 수 있는 언어로 빠짐없이 작성되고, 그 프로그램이 각 단계를 논리 규칙에 비추어 검사합니다. 구백 번째 쪽에서 지치지 않고, 누구의 말도 그대로 믿지 않습니다.

seL4의 증명은 Isabelle/HOL이라는 증명 보조기에서 이렇게 검사됩니다. 증명은 공개되어 있고, 누구나 다시 실행해 볼 수 있습니다.

seL4의 증명이 말하는 것

seL4는 모든 NoWayOS 시스템이 그 위에서 실행되는 커널입니다. 약 10,000줄의 코드이며, 장치를 완전히 제어하는 유일한 코드입니다. 핵심은 그 크기입니다. 만 줄에 대한 논증은 끝까지 마칠 수 있습니다. 수천만 줄에 대한 논증은 아직 그럴 수 없습니다.

seL4 Foundation은 이 증명들을 층으로 나누어 설명합니다.

• 코드는 명세가 말하는 대로 동작하고, 그 이상은 하지 않습니다. 여기서 커널이 할 수 없는 일의 목록이 따라 나옵니다. 버퍼를 넘치게 하는 것, 널 포인터를 따라가는 것, 메모리를 누수시키는 것, 0으로 나누는 것입니다.
• 실제로 실행되는 프로그램은 증명된 코드와 일치합니다. 둘 사이에는 컴파일러가 있으므로, 또 하나의 증명이 그 출력을 검사합니다.
• 커널은 시스템의 각 부분을 서로 분리해 둘 수 있습니다. 한 부분은 권한을 부여받지 않는 한 다른 부분의 데이터를 변경할 수도, 읽을 수도, 그 부분에 필요한 자원을 빼앗을 수도 없습니다.
• 시스템은 설계된 상태 그대로 시작할 수 있습니다. 시스템 기술서에 적힌 것과 정확히 같은 권한을 가지고 시작합니다.

모든 층이 모든 프로세서와 모든 구성에 대해 완료된 것은 아닙니다. 이 점은 중요하며, 뒤에서 다시 다루겠습니다.

증명이 당연하게 여기는 것

증명의 범위는 그 명제의 범위와 정확히 같고, 증명은 가정 위에 서 있습니다. seL4는 자신의 가정을 적어 둡니다. 하드웨어가 그 모델이 말하는 대로 동작한다는 것, 가장 낮은 수준의 코드 수백 줄이 올바르다는 것, 커널이 시작되기 전에 실행되는 코드가 제 역할을 했다는 것입니다. 기밀성 증명은 타이밍을 다루지 않습니다.

증명은 명세가 올바른 것을 요구하는지에 대해서는 아무 말도 하지 않고, 커널 위의 소프트웨어에 대해서도 아무 말도 하지 않습니다. 증명된 커널은 버그가 있는 프로그램도 충실하게 격리합니다. 버그는 여전히 거기 있습니다. 다만 다른 어떤 것에도 닿지 못할 뿐입니다.

이것은 증명의 약점이 아닙니다. 증명을 가질 만한 가치가 여기에 있습니다. 증명은 무엇을 다루는지 정확히 말하므로, 무엇이 남는지도 정확히 알 수 있습니다.

NoWayOS가 서 있는 자리

있는 그대로 말씀드리겠습니다. NoWayOS는 seL4 위에서 실행되지만, 현재 seL4의 완료된 증명 범위 안에 있는 NoWayOS 이미지는 없습니다. NoWayOS는 seL4의 혼합 임계성 구성을 사용하며, 저희 프로세서에 대한 그 증명은 진행 중입니다. 그리고 seL4의 증명은 NoWayOS 자체의 코드를 다룬 적이 없습니다. 그래서 저희는 NoWayOS를 “정형 검증된” 운영체제라고 부르지 않으며, 앞으로도 그렇게 부르지 않겠습니다.

모든 이미지는 자신이 어디에 서 있는지 밝힙니다. 이미지 옆의 파일 하나가 커널의 구성을 seL4가 증명한 구성과 나란히, 옵션 하나하나 기록합니다. 보안 페이지에서 실제 파일을 보실 수 있습니다.

저희가 직접 만든 더 작은 증명

NoWayOS의 코드는 다른 방법으로 보증을 얻습니다. Rust, 격리, 리뷰, 테스트, 그리고 더 소박한 종류의 증명입니다.

시스템의 부분들 사이를 오가는 메시지의 디코더에는 모두 유계 증명이 있습니다. Kani라는 모델 검사기로 만든 것입니다. 유계 증명은 명시된 크기까지의 모든 입력을 다룹니다. 여기서는 디코더가 받아들이는 가장 긴 레코드까지입니다. 그 한도 안에서는 진짜 증명입니다. 어떤 입력도 디코더에 패닉, 오버플로, 범위 밖 읽기를 일으키지 못합니다. 한도 밖에 대해서는 아무 말도 하지 않습니다. 그래서 한도를 있을 수 있는 가장 긴 입력에 맞추었습니다.

그런 다음 저희는 디코더를 일부러 망가뜨려, 증명이 그것을 알아차리는지 확인합니다. 실패할 수 없는 증명은 실패할 수 없는 테스트보다 나을 것이 없습니다.

있는 그대로의 크기

증명은 어떤 것도 “해킹 불가능”하게 만들지 않습니다. 증명은 하나의 명제를, 모든 경우에, 읽어 볼 수 있는 가정 아래에서 참으로 만듭니다. 명제와 가정을 알면, 무엇을 가졌는지 알 수 있습니다.

그래서 NoWayOS는 그런 증명을 갖춘 커널 위에 만들어졌고, 그 증명이 어디까지 닿는지를 이미지마다 알려 드립니다.