[운영체제] seL4 소개

아래는 seL4 홈페이지에서 seL4를 소개하는내용을 번역한 것이다.

seL4 백서 첫 페이지

seL4는 고보증(High-Assurance), 고성능(High-Performance)의 운영체제 마이크로커널이다. seL4는 성능저하 없는 정형검증(Formal verification)으로 인해 특별하다. seL4는 안전필수(Safety-Critical) 시스템과 보안필수(Security-Critical) 시스템을 구축하기 위해 신뢰할 수 있는 기반이다. seL4는 seL4 재단이 지원하고 Github에서 오픈소스로 제공된다.

커널이 된다는 것은 소프트웨어 시스템의 핵심에서 소프트웨어 조각이 실행되고 리소스에 대한 모든 액세스를 제어하는 ​​소프트웨어라는 의미이다. sel4는 세밀한 접근제어를 Capability-based security를 통해 제공하고 시스템 컴포넌트 간의 통신을 제어한다. 이것은 소프트웨어 시스템에서 가장 중요한 부분으로 특권모드(Privileged mode)에서 실행된다.
마이크로커널이 된다는 것은 커널이 정책이 없는 최소 코어로 축소되었지만 다양한 시나리오를 지원하는 시스템을 구축하기 위해 신뢰할 수 있는 기반을 구축할 수 있음을 의미한다.

seL4는 L4 마이크로커널 제품군에 속해 있으며 세계에서 가장 진보된 고보증된(hightly assured) 운영체제 커널이다.
seL4의 정형검증은 다른 운영체제와 차별화된 요소이다. 정형검증은 시스템에서 실행 중인 응용 간의 격리를 확실하게 제공하며 이는 시스템의 한 부분이 포함되어 다른 부분이 손상되는 것을 억제하고 더 중요한 부분에 해를 끼치는 등의 잠재적 위험을 방지합니다.

특히, seL4 구현은 명세서를 따라 공식적(수학적)으로 올바른(버그없음) 것이 증명되었으며 강력한 보안 속성을 적용하는 것이 입증되었고  올바르게 작업이 구성된 경우 최악의 실행 시간이 상한선인 것으로 안전히 입증되었다. 이것은 세계 최초로 입증된 운영체제이며 세밀한 Capability-based security와 고성능을 특징으로 하는 유일하게 검증된 운영체제이다. 또한 중요도가 혼합 임계 실시간 시스템(Mixed criticality real-time systems)에 대한 가장 진보된 지원을 포함한다. 이러한 약관의 더 자세한 설명이 필요하다면, 홈페이지의 FAQ 페이지를 방문하라.

2009년에 seL4 커널은 TS(Trustworthy System group)의 획기적인 과학적 결과물이며 고성능 커널이 정형검증의 범위 안에 있다는 것을 보여주었다. 오늘날 seL4는 자동차와 항공, 인프라, 의료 및 방위를 포함한 다양한 영역에서 활발히 사용되는 생태계의 일부가 되었다. 

실제 배포에 적합함을 보여주는 주요 사례는 DARPA가 지원하는 HACMS 프로그램이 있다. 여기서 seL4는 사이버 공격으로부터 자율 헬리콥터를 보호하는 데 사용되었습니다. TS는 seL4 재단의 파트너와 긴밀히 협력하여 seL4를 통해 최신 운영체제를 계속 추진하고 있다. 

홈페이지의 앞으로의 연구 페이지로 가면 TS의 진행 중인 상황과 seL4와 신뢰할 수 있는 시스템(Trustworthy systems)에 대해 알아볼 수 있다.