seL4, ARM 64비트에서 기밀성 증명까지 완성…보안 격리 수학적으로 마무리

운영체제 커널의 보안을 광고 문구가 아니라 수학적 정리로 보증하려는 시도가 하나의 분기점을 지났다. seL4 마이크로커널의 정형 검증을 담당하는 Proofcraft가 ARM 64비트(AArch64) 아키텍처에서 커널이 기밀성(confidentiality)을 강제한다는 증명을 완료했다고 밝혔다. 이는 seL4 위에서 동작하는 애플리케이션이 권한 없이 다른 정보를 알아내지 못한다는 사실을, 코드 수준에서 형식적으로 입증한 것이다. 앞서 완료된 기능적 정확성(functional correctness)과 무결성(integrity) 증명에 이번 기밀성 증명이 더해지면서, AArch64에서 seL4가 그 위의 애플리케이션들을 보안적으로 격리한다는 전체 증명 스택이 마무리됐다. 이 작업은 영국 NCSC의 지속적인 지원으로 이뤄졌다.

격리가 실무에서 뜻하는 것

보안 격리라는 표현은 추상적으로 들리지만, 실무에서의 의미는 구체적이다. seL4가 보장하는 격리는 중요도가 낮은 애플리케이션이 공격당하더라도 그 피해가 중요 애플리케이션으로 전파되어 이를 무력화하는 상황을 막는다. 하나의 하드웨어 위에 신뢰 수준이 서로 다른 소프트웨어를 함께 올려야 하는 환경—차량, 항공, 방산, 산업 제어 같은 임베디드 영역—에서 이는 핵심 요구사항이다. 기능적 정확성이 '커널이 명세대로 동작한다'는 것을 증명한다면, 무결성과 기밀성 증명은 각각 '권한 없는 데이터 수정'과 '권한 없는 정보 획득'이라는 두 방향의 정보 흐름을 커널이 차단한다는 것을 보증한다. 다만 이런 증명은 항상 명시된 가정(assumption) 아래에서 성립한다는 점을 유의해야 한다. 하드웨어가 명세대로 동작한다는 전제나 부채널 같은 특정 위협 모델의 범위는 증명 자체가 아니라 그 경계 조건에 달려 있다.

검증 도구 관점에서도 진전이 있었다. LICS(제41회 Logic in Computer Science 심포지엄, 리스본)에서 발표된 논문 'The Algebra of Iterative Constructions'는 고정점(fixed point)의 반복적 구성을 위한 대수적 추상화와 추론 원리를 다룬다. 클레이니 고정점 정리로 대표되듯 고정점은 프로그램 의미론에서 반복적으로 등장하는 주제인데, 이 대수는 그런 정리들을 간결하게 표현하고 증명 보조 도구에서 효율적으로 구현할 수 있게 한다. 실제로 이 논문의 Isabelle/HOL 구현은 고도로 자동화되어 있으며, Isabelle/HOL은 Proofcraft가 seL4 검증에 사용하는 바로 그 도구다. 이 협업은 2025년 아테네에서 열린 IFIP WG 2.3 회의에서 Gerwin Klein과 Benjamin Kaminski 사이에 즉흥적으로 시작됐다고 한다.

MCS 검증과 스케줄링의 유연화

또 하나 오래 기다려온 성과는 혼합 임계(mixed-criticality) 시스템을 지원하는 MCS 구성의 검증이다. MCS는 seL4에 추가된 가장 큰 신규 기능으로, 커널 구현과 API 전반에 걸친 광범위한 변경을 수반해 검증 난도가 높았다. Proofcraft는 이번에 처음으로 MCS를 포함한 seL4의 기능적 정확성 검증을 RISC-V 아키텍처에서 완료했다. 기능적 정확성은 seL4 검증 스택에서 가장 크고 중심이 되는 증명이며, 이 결과는 DARPA PROVERS 프로그램의 일환으로 ARM 64비트로 이식될 예정이다. 자동차 같은 실시간 혼합 임계 응용에서 MCS가 실질적으로 활용되려면 이런 아키텍처 이식이 뒤따라야 한다는 점에서, RISC-V 완료는 종착점이 아니라 경로의 중간 지점에 가깝다.

정보 흐름 제어의 실용성을 높이는 변경도 나왔다. 이전까지 seL4의 보안 증명, 특히 정보 흐름 강제 증명은 커널에 컴파일되어 들어간 완전 정적 스케줄을 요구했다. 개발자는 시스템 전체 수명 동안 각 도메인에 고정된 시간을 미리 배정해야 했고, 이 경직성 탓에 정보 흐름 제어를 실제로 적용하거나 Microkit 같은 SDK형 개발에 얹기가 어려웠다. Proofcraft는 준정적(semi-static) 도메인 스케줄을 로드할 수 있는 새 런타임 API를 제안했다. 이를 통해 시스템은 실행 중 여러 국면을 거칠 수 있다. 예컨대 부팅 단계에서는 가상머신이 도메인 시간 할당을 넘기지 않고 기동하도록 긴 타임 슬라이스를 주고, 운영 단계에서는 각 도메인이 외부 상호작용에 민첩하게 반응하도록 짧은 슬라이스를 배정하는 식이다. 이 API는 구현·검증을 마치고 seL4 15.0.0에 포함됐다.

병렬로 굴러가는 세 갈래 연구

Proofcraft가 밝힌 그림을 종합하면, 현재 이 회사는 DARPA·독일 Cyberagentur·NCSC가 각각 지원하는 세 개의 대형 프로젝트를 동시에 진행하고 있다. Cyberagentur 쪽에서는 Kry10과 협력하는 ÖvIT 연구 프로그램의 Dyvercon 프로젝트가 있는데, 여기서 Gerwin Klein은 정적 멀티커널 구성으로 증명을 확장하는 작업을 보고했다. 이는 애플리케이션이 성능을 위해 여러 CPU 코어를 활용하되 커널 수준에서는 각 코어마다 별도의 seL4 인스턴스를 돌리는 방식이다. 한편 seL4 증명은 커널이 구동 가능한 ARM 플랫폼 100%에서 지원되어, 사용자가 어떤 지원 플랫폼을 선택하든 검증된 코드베이스를 쓰고 있음을 보장받게 됐다는 점도 함께 정리됐다.

실무자 입장에서 이 소식들의 무게는 '완성'이라는 단어에 있지 않다. 정형 검증은 특정 아키텍처, 특정 구성, 명시된 가정이라는 좌표계 안에서만 성립하며, seL4의 성과는 그 좌표를 하나씩 늘려온 누적의 결과다. AArch64 보안 증명 스택 완결, RISC-V에서의 MCS 기능 정확성, 준정적 스케줄링의 릴리스는 각각 다른 축의 진전이고, 이들이 하나의 배포판에서 동시에 충족되는 지점은 아직 조율 중이다. 고신뢰 커널 도입을 검토하는 팀이라면 자사 타깃 아키텍처와 필요한 구성(MCS, 멀티커널, 정보 흐름 제어)이 어느 증명 좌표에 놓여 있는지를 먼저 확인하는 것이 현실적인 출발점이다. Proofcraft는 9월 1~3일 밴쿠버에서 열리는 2026 seL4 서밋을 실버 스폰서로 후원한다.