▲

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

 (sel4.systems)
1P by GN⁺ 10일전 | ★ favorite | 댓글과 토론
  • 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는 기능적 정확성, 보안, 성능이 입증된 세계에서 가장 안전한 마이크로커널임
  • 검증된 보안 모델과 혼합 중요도 시스템 지원으로 다양한 분야에서 실용적으로 사용 가능
  • 기존 시스템의 보안 강화 및 성능 향상 가능 → 보안 및 성능의 균형을 이룬 혁신적인 마이크로커널