- seL4는 보안·안전이 중요한 임베디드 및 사이버-물리 시스템을 겨냥한 OS 마이크로커널로, 하드웨어 자원을 격리·다중화하지만 완전한 범용 OS는 아님
- 커널 모드 코드를 약 10 kSLOC로 줄여 TCB와 공격 표면을 축소하고, 파일 시스템·네트워크·드라이버 같은 OS 서비스는 사용자 모드로 밀어냄
- 코드 수준 형식 검증을 갖춘 세계 최초 OS 커널이며, 올바르게 구성된 시스템에서는 기밀성·무결성·가용성 같은 보안 속성까지 커널이 보장함
- capability 기반 접근 제어, WCET 분석, 혼합 중요도 실시간 시스템 지원, 하이퍼바이저 기능을 조합해 세밀한 격리와 실시간성을 함께 다룸
- seL4 API는 매우 낮은 수준이라 복잡한 시스템은 직접 만들기 어렵고, 정적 아키텍처가 맞는 경우 Microkit 같은 프레임워크를 쓰는 방식이 현실적임
seL4가 맡는 범위
- seL4는 운영체제의 낮은 수준 핵심부인 마이크로커널임
- OS는 프로세서의 더 높은 권한 실행 모드인 커널 모드에서 하드웨어와 자원을 제어함
- 애플리케이션은 사용자 모드에서 실행되며, OS가 허용한 방식으로만 하드웨어에 접근함
- 마이크로커널은 높은 권한에서 실행되는 코드를 최소화한 OS 핵심부임
- seL4는 1990년대 중반까지 거슬러 올라가는 L4 마이크로커널 계열에 속함
- seL4는 seLinux와 관련 없음
- seL4는 완전한 OS가 아니라 하드웨어 자원을 안전하게 다중화하고 격리하는 낮은 수준 커널임
- 파일 시스템, 네트워크 스택, 디바이스 드라이버 같은 일반 OS 서비스는 커널 안에 있지 않음
- 이런 서비스는 사용자 모드 프로그램으로 제공되어야 함
마이크로커널 구조와 공격 표면 축소
- 리눅스 같은 모놀리식 커널은 파일 저장, 네트워킹 같은 OS 서비스를 커널 모드 코드로 제공함
- 커널 모드 코드는 시스템 자원에 제한 없이 접근할 수 있어, 버그가 권한 상승이나 임의 코드 실행으로 이어지면 전체 시스템이 손상될 수 있음
- 리눅스 커널은 약 20 MSLOC 규모이며, 수만 개의 버그가 있을 수 있다고 추정됨
- seL4 같은 잘 설계된 마이크로커널은 커널 모드 코드를 약 10 kSLOC 수준으로 줄임
- 이는 리눅스 커널보다 세 자릿수 규모로 작음
- TCB가 줄어들면서 공격 표면도 함께 줄어듦
- 대부분의 OS 서비스는 커널 밖으로 빠지고, 마이크로커널은 하드웨어 주변의 얇은 래퍼처럼 동작함
- 핵심 제공 기능은 프로그램 간 격리와 안전한 호출 메커니즘임
- 서비스는 커널 안이 아니라 별도 샌드박스에서 실행되는 사용자 모드 프로그램이 됨
- 알려진 리눅스 침해 사례 중 치명적 사례를 분석한 연구에서, 마이크로커널 설계는 29% 를 완전히 제거하고 추가 55% 를 더 이상 치명적으로 분류되지 않을 정도로 완화할 수 있었음
PPC, capability, 세밀한 권한 제어
- seL4는 보호된 프로시저 호출(PPC) 메커니즘을 제공함
- 역사적 이유로 IPC라는 용어가 남아 있지만, IPC라는 표현은 오해를 낳아 나쁜 설계로 이어질 수 있음
- PPC는 한 프로그램이 다른 샌드박스에 있는 프로그램의 함수를 안전하게 호출하게 함
- 마이크로커널은 PPC에서 입력과 출력을 전달하고 인터페이스를 강제함
- 원격 함수는 내보낸 진입점에서만 호출될 수 있음
- 적절한 capability를 받은 명시적으로 허가된 클라이언트만 호출 가능함
- capability는 시스템의 특정 자원에 접근할 수 있게 하는 접근 토큰임
- 어떤 엔티티가 어떤 자원에 접근할 수 있는지 매우 세밀하게 제어함
- 최소 권한 원칙 또는 최소 권한성 원칙(POLA)을 지원함
- 리눅스나 Windows 같은 주류 시스템의 접근 제어 방식으로는 이런 수준의 최소 권한 달성이 불가능함
- seL4는 capability 기반이면서 형식 검증된 세계 유일의 OS로, 이 조합 덕분에 세계에서 가장 안전한 OS라는 방어 가능한 주장을 갖는다고 평가됨
형식 검증과 보안 보장
- seL4는 구현 정확성에 대한 형식적·수학적·기계 검증된 증명을 제공함
- 이 증명은 커널이 명세와 관련해 매우 강한 의미에서 “버그 없음”을 뜻함
- seL4는 코드 수준에서 이런 증명을 갖춘 세계 최초 OS 커널임
- 구현 정확성 외에도 seL4는 보안 강제에 대한 추가 증명을 제공함
- 올바르게 구성된 seL4 기반 시스템에서 커널은 기밀성, 무결성, 가용성을 보장함
- 검증 체인은 seL4의 핵심 차별점임
- 보안·안전 중요 시스템에서 커널이 신뢰 기반이 되려면 구현과 보안 속성에 대한 강한 보증이 필요함
실시간성과 혼합 중요도 시스템
- seL4는 최악 실행 시간(WCET)에 대한 완전하고 건전한 분석을 거친 OS 커널임
- 커널이 적절히 구성되면 모든 커널 연산은 시간상 경계가 있음
- 그 경계도 알려져 있음
- 이런 특성은 하드 실시간 시스템 구축의 전제 조건임
- 엄격히 제한된 시간 안에 이벤트에 반응하지 못하면 치명적인 시스템을 대상으로 함
- seL4는 혼합 중요도 실시간 시스템(MCS)도 지원함
- 신뢰도가 낮은 코드가 같은 플랫폼에서 함께 실행되더라도 중요한 활동의 시간성을 보장해야 하는 환경을 대상으로 함
- 기존 MCS OS가 쓰는 엄격하고 유연하지 않은 시간·공간 파티셔닝과 달리, seL4는 자원 활용을 유지하는 유연한 모델을 제공함
하이퍼바이저로 쓰는 seL4
- seL4는 마이크로커널이면서 하이퍼바이저이기도 함
- seL4 위에서 가상 머신을 실행할 수 있음
- 가상 머신 안에서는 Linux 같은 일반 게스트 OS를 실행할 수 있음
- 게스트와 애플리케이션은 seL4가 강제하는 통신 채널에 따라 서로 통신할 수 있음
- 네이티브 애플리케이션과도 통신 가능함
- Linux VM을 시스템 서비스 제공 수단으로 활용할 수 있음
- 예시 구성에서는 별도 VM에서 실행되는 여러 Linux 인스턴스로부터 네트워킹과 스토리지 같은 서비스를 빌려옴
seL4 위에서 시스템을 만드는 방법
- seL4 API는 다른 마이크로커널과 비교해도 매우 낮은 수준임
- 하드웨어를 안전하게 관리하는 데 필요한 최소 추상화만 제공함
- seL4는 “운영체제의 어셈블리어”에 비유됨
- 복잡한 시스템을 seL4 위에 직접 만드는 방식은 적절하지 않음
- 더 높은 수준의 프레임워크가 서비스 구현 코드에 집중하게 하고, 하드웨어 복잡성과 시스템 통합을 자동화해야 함
- seL4에는 세 가지 주요 오픈소스 컴포넌트 프레임워크가 있음
- Microkit: protection domain 중심의 소수 추상화로 seL4 API를 단순화하고, 별도 컴파일 모듈과 커널 바이너리를 통합해 부팅 가능한 이미지를 만드는 SDK를 제공함
- CAmkES: Microkit의 전신이며 정적 아키텍처 시스템을 위한 컴포넌트 프레임워크지만, SDK가 없어 빌드 과정이 더 불편하고 오버헤드가 큼
- Genode: 여러 마이크로커널을 지원하고 x86 플랫폼용 서비스와 드라이버가 풍부하며 정적 아키텍처를 강제하지 않지만, seL4의 모든 보안·안전 기능을 활용하지 못하고 보증 스토리가 없음
- 정적 시스템 아키텍처가 요구사항에 맞는 한, seL4 기반 시스템 구축에는 Microkit이 권장됨
- 정적 아키텍처는 모듈 집합과 통신 구조를 시스템 구성 시점에 정의하는 모델임
- 이 모델은 자동차와 항공기 같은 복잡한 사이버-물리 시스템을 포함해 대부분의 임베디드 시스템 요구에 맞는 것으로 봄