# SeL4 마이크로커널 소개 [PDF]

> Clean Markdown view of GeekNews topic #19932. Use the original source for factual precision when an external source URL is present.

## Metadata

- GeekNews HTML: [https://news.hada.io/topic?id=19932](https://news.hada.io/topic?id=19932)
- GeekNews Markdown: [https://news.hada.io/topic/19932.md](https://news.hada.io/topic/19932.md)
- Type: GN+
- Author: [neo](https://news.hada.io/@neo)
- Published: 2025-03-24T20:32:27+09:00
- Updated: 2025-03-24T20:32:27+09:00
- Original source: [sel4.systems](https://sel4.systems/About/seL4-whitepaper.pdf)
- Points: 1
- Comments: 0

## Topic Body

- seL4는 OS 마이크로커널로, 최소한의 코드로 커널 모드를 실행해 하드웨어 자원을 제어하고 보안을 강화함  
- L4 마이크로커널 계열에 속하며, 1990년대 중반부터 개발됨  
- 하이퍼바이저로 동작 가능하여 리눅스와 같은 게스트 OS 실행 지원  
- 세계 최초로 기능적 정확성이 입증된 OS 커널로, 코드 수준에서의 수학적 증명이 완료됨  
- 세밀한 접근 제어를 위해 **Capability(역량)** 기반 보안 모델 사용  
  
### seL4의 구조 및 하이퍼바이저 기능  
- **모놀리식 커널 vs 마이크로커널**  
  - 모놀리식 커널(Linux 등): 커널 코드가 방대해 보안 취약점이 많음 → 약 2000만 줄의 코드 (20M SLOC)  
  - 마이크로커널(seL4): 최소한의 커널 코드 사용 → 약 1만 줄의 코드 (10K SLOC)  
  - 커널 크기 축소 → 보안 강화 및 공격 표면 감소  
- **seL4는 하이퍼바이저 역할 수행**  
  - VM에서 리눅스 같은 완전한 게스트 OS 실행 가능  
  - 각 VM은 독립적으로 실행되며 상호 간섭 불가능 → 강력한 격리 보장  
  - 보호된 프로시저 호출(PPC) → VM 간 보안 통신 가능  
  
### seL4의 검증 및 보안 모델  
- **기능적 정확성 검증**  
  - seL4는 코드 수준에서 수학적으로 기능이 정확함을 증명  
  - 커널의 모든 동작이 사양에 맞게 동작함을 보장  
- **이행 검증(Translation Validation)**  
  - 컴파일러에서 생성된 바이너리 코드가 원래의 C 코드와 정확히 일치하는지 증명  
  - 자동화 도구 체인을 통해 실행  
- **보안 속성 검증**  
  - **기밀성:** 명시적으로 허용된 경우에만 데이터 접근 가능  
  - **무결성:** 명시적으로 허용된 경우에만 데이터 수정 가능  
  - **가용성:** 명시적으로 허용된 경우에만 리소스 사용 가능  
  
### Capability 기반 보안 모델  
- **Capability란?**  
  - 특정 객체에 대한 접근 권한을 부여하는 보안 토큰  
  - 객체 참조 및 접근 권한을 함께 인코딩  
  - 세부적인 접근 제어 가능 → 최소 권한 원칙(Principle of Least Privilege, POLA) 적용  
- **Capability의 장점**  
  - 세밀한 접근 제어 → 권한 최소화 가능  
  - 권한 위임(Delegation) 및 권한 취소 가능  
  - 강력한 보안 모델 → 전통적인 접근 제어 모델(ACL)보다 우수  
- **혼동된 대리인 문제 해결**  
  - 전통적인 ACL 기반 시스템에서는 보안 상태가 주체의 보안 ID에 따라 결정됨  
  - seL4에서는 Capability가 직접 보안 권한을 결정 → 명확한 권한 제어 가능  
  
### 실시간 시스템 및 혼합 중요도 시스템 지원  
- **실시간 시스템 지원**  
  - seL4는 우선순위 기반 스케줄링 지원  
  - 모든 커널 작업의 최악의 실행 시간(WCET) 분석 완료 → 하드 실시간 보장  
- **혼합 중요도 시스템(Mixed-Criticality System, MCS) 지원**  
  - 스케줄링 컨텍스트 기반으로 CPU 자원 할당 및 격리  
  - 높은 우선순위를 가진 작업이 CPU를 독점하지 않도록 제어  
  - 임계 작업과 비임계 작업을 동시에 실행 가능  
  
### 성능 및 효율성  
- **최고 성능의 마이크로커널**  
  - 성능이 중요한 경우에도 보안을 저하시키지 않음  
  - 시스템 호출 및 IPC 비용이 최소화됨 → 경쟁 시스템 대비 5배 이상 빠름  
- **경쟁 시스템 대비 우수한 성능**  
  - Fiasco.OC: seL4 대비 약 2배 느림  
  - Zircon: seL4 대비 약 9배 느림  
  - CertiKOS: seL4 대비 약 5배 느림  
  
### 실세계 적용 및 사이버 레트로핏  
- **실제 사용 사례**  
  - Boeing의 ULB(무인 헬리콥터)에서 성공적으로 적용됨  
  - 보안 강화 및 시스템 안정성 증가 확인  
  
- **기존 시스템의 점진적 보안 강화(Incremental Cyber Retrofit)**  
  - 기존 시스템을 VM에서 실행하면서 점진적으로 모듈화  
  - 보안 강화 및 성능 저하 최소화  
  
### 결론  
- seL4는 기능적 정확성, 보안, 성능이 입증된 세계에서 가장 안전한 마이크로커널임  
- 검증된 보안 모델과 혼합 중요도 시스템 지원으로 다양한 분야에서 실용적으로 사용 가능  
- 기존 시스템의 보안 강화 및 성능 향상 가능 → 보안 및 성능의 균형을 이룬 혁신적인 마이크로커널

## Comments



_No public comments on this page._