상위 질문
타임라인
채팅
관점
L4 마이크로커널 계열
위키백과, 무료 백과사전
Remove ads
L4는 운영체제(OS)의 다양한 유형을 구현하는 데 사용되는 2세대 마이크로커널 제품군이지만, 주로 유닉스 계열, 이식 가능한 운영체제 인터페이스(POSIX) 호환 유형에 사용된다.
L4는 이전 마이크로커널인 L3와 마찬가지로 독일의 컴퓨터 과학자인 요헨 리트케가 초기 마이크로커널 기반 OS의 성능 저하에 대한 응답으로 만들었다. 리트케는 다른 목표보다 고성능을 위해 처음부터 설계된 시스템이 실용적인 마이크로커널을 생산할 수 있다고 생각했다. 1993년에 손으로 코딩된 인텔 인텔 80386 특정 어셈블리어 코드로 그의 원래 구현은 Mach보다 20배 빠르다는 점에서 주목받았다.[2] 2년 후의 후속 출판물[3]은 너무나 영향력이 커서 2015년 ACM SIGOPS 명예의 전당 상을 수상했다. 도입 이후, L4는 크로스 플랫폼으로 개발되었으며 컴퓨터 보안, 격리 및 견고성을 개선했다.
L4Ka::Pistachio(카를스루에 공과대학교에서 리트케와 그의 학생들이 구현), L4/MIPS(뉴사우스웨일스 대학교 (UNSW)), Fiasco(드레스덴 공과대학교 (TU Dresden))를 포함하여 원래 L4 커널 응용 프로그램 이진 인터페이스(ABI) 및 그 후속 제품에 대한 다양한 재구현이 있었다. 이러한 이유로 L4라는 이름은 일반화되었고 더 이상 리트케의 원래 구현만을 지칭하지 않는다. 이제 L4 커널 인터페이스 (컴퓨팅)와 그 다양한 버전을 포함하는 전체 마이크로커널 제품군에 적용된다.
L4는 널리 배포되었다. 오픈 커널 랩스의 한 변종인 OKL4는 수십억 개의 모바일 장치에 탑재되었다.[4][5]
Remove ads
디자인 패러다임
마이크로커널의 일반적인 개념을 명시하면서 리트케는 다음과 같이 말한다.
개념은 커널 외부로 이동하는 것, 즉 경쟁 구현을 허용하는 것이 시스템이 요구하는 기능의 구현을 방해할 경우에만 마이크로커널 내에서 허용된다.[3]
이러한 정신으로 L4 마이크로커널은 몇 가지 기본 메커니즘을 제공한다: 주소 공간(페이지 테이블을 추상화하고 메모리 보호를 제공), 스레드 및 스케줄링(실행을 추상화하고 시간적 보호를 제공), 프로세스 간 통신(격리 경계를 넘는 제어된 통신용).
L4와 같은 마이크로커널 기반 운영체제는 리눅스와 같은 모놀리식 커널 또는 이전 세대 마이크로커널이 내부에 포함하는 서비스를 사용자 공간의 서버로 제공한다. 예를 들어, 보안 유닉스 계열 시스템을 구현하려면 서버는 Mach가 커널 내부에 포함했던 권한 관리를 제공해야 한다.
Remove ads
역사
요약
관점
Mach와 같은 1세대 마이크로커널의 성능 저하는 1990년대 중반에 많은 개발자들이 전체 마이크로커널 개념을 재검토하게 만들었다. Mach에서 사용된 비동기 커널 내 버퍼링 프로세스 통신 개념은 성능 저하의 주요 원인 중 하나로 밝혀졌다. 이는 Mach 기반 운영체제 개발자들이 파일 시스템이나 드라이버와 같은 일부 시간 крити적 구성 요소를 커널 내부로 다시 이동하게 만들었다. 이는 성능 문제를 다소 완화했지만, 진정한 마이크로커널의 최소성 개념을 명백히 위반하고 (주요 장점을 낭비한다).
Mach 병목 현상에 대한 자세한 분석에 따르면, 다른 것들 중에서도 워킹 셋이 너무 크다는 것이 밝혀졌다. IPC 코드는 공간적 지역성이 좋지 않다. 즉, 너무 많은 캐시 미스를 초래하며, 대부분은 커널 내부에 있다.[3] 이 분석은 효율적인 마이크로커널은 성능에 중요한 코드의 대부분이 (1차) 캐시에 (바람직하게는 캐시의 작은 부분에) 들어갈 만큼 작아야 한다는 원칙을 낳았다.
L3
요헨 리트케는 성능과 기계 특정(크로스 플랫폼 소프트웨어와 대조적으로) 설계에 세심한 주의를 기울인 잘 설계된 더 얇은 프로세스 간 통신(IPC) 계층이 실제 성능을 크게 향상시킬 수 있음을 입증하기 시작했다. Mach의 복잡한 IPC 시스템 대신 그의 L3 마이크로커널은 추가 오버헤드 없이 메시지를 간단히 전달했다. 필요한 보안 정책을 정의하고 구현하는 것은 사용자 공간 서버의 의무로 간주되었다. 커널의 역할은 사용자 수준 서버가 정책을 강제할 수 있도록 필요한 메커니즘을 제공하는 것뿐이었다. 1988년에 개발된 L3는 안전하고 견고한 운영체제임이 입증되었으며, 예를 들어 기술 검사 협회에 의해 수년간 사용되었다.
L4
L3를 사용한 경험 끝에 리트케는 Mach의 다른 몇 가지 개념도 잘못 배치되었다는 결론에 도달했다. 마이크로커널 개념을 더욱 단순화하여 그는 주로 고성능을 위해 설계된 최초의 L4 커널을 개발했다. 성능을 극대화하기 위해 전체 커널은 어셈블리어로 작성되었으며, IPC는 Mach보다 20배 빨랐다.[2] 이러한 극적인 성능 향상은 운영체제에서 드문 일이며, 리트케의 작업은 1996년 리트케가 일하기 시작한 IBM, TU Dresden, UNSW를 포함한 여러 대학 및 연구 기관에서 새로운 L4 구현 및 L4 기반 시스템에 대한 작업을 촉발했다. IBM 왓슨 연구소에서 리트케와 그의 동료들은 L4 및 마이크로커널 기반 시스템 전반에 걸쳐 특히 Sawmill OS에 대한 연구를 계속했다.[6]
L4Ka::Hazelnut
1999년에 리트케는 카를스루에 대학교의 시스템 아키텍처 그룹을 맡아 마이크로커널 시스템에 대한 연구를 계속했다. 고성능 마이크로커널이 상위 수준 언어로도 구축될 수 있다는 개념 증명으로, 이 그룹은 IA-32 및 ARM 아키텍처 기반 머신에서 실행되는 커널의 C++ 버전인 L4Ka::Hazelnut을 개발했다. 이 노력은 성공적이었고, 성능은 여전히 허용 가능한 수준이었으며, 이 출시와 함께 커널의 순수 어셈블리어 버전은 사실상 중단되었다.
L4/Fiasco
L4Ka::Hazelnut 개발과 병행하여 1998년에 드레스덴 공과대학교의 운영 체제 그룹 TUD:OS는 L4/Fiasco라는 L4 커널 인터페이스의 자체 C++ 구현 개발을 시작했다. 커널 내 동시성을 허용하지 않는 L4Ka::Hazelnut과 특정 선점 지점에서만 커널 내 인터럽트를 허용하는 후속 L4Ka::Pistachio와는 달리, L4/Fiasco는 낮은 인터럽트 지연을 달성하기 위해 (극히 짧은 원자적 연산을 제외하고) 완전히 선점 가능했다. 이는 L4/Fiasco가 드레스덴 공과대학교에서 개발된 하드 실시간 컴퓨팅이 가능한 운영 체제인 DROPS의 기반으로 사용되기 때문에 필요하다고 간주되었다.[7] 그러나 완전히 선점 가능한 설계의 복잡성으로 인해 Fiasco의 이후 버전은 제한된 수의 선점 지점을 제외하고는 인터럽트가 비활성화된 상태에서 커널을 실행하는 전통적인 L4 접근 방식으로 돌아갔다.
Remove ads
크로스 플랫폼
요약
관점
L4Ka::Pistachio
L4Ka::Pistachio와 Fiasco의 최신 버전이 출시될 때까지 모든 L4 마이크로커널은 기본 CPU 아키텍처에 본질적으로 밀접하게 묶여 있었다. L4 개발의 다음 큰 변화는 더 높은 수준의 이식성에도 불구하고 여전히 고성능 특성을 유지하는 크로스 플랫폼(플랫폼 독립적) API의 개발이었다. 커널의 기본 개념은 동일했지만, 새로운 API는 다중 프로세서 시스템에 대한 더 나은 지원, 스레드와 주소 공간 간의 더 느슨한 연결, 사용자 수준 스레드 제어 블록(UTCB) 및 가상 레지스터의 도입을 포함하여 이전 L4 버전에 비해 많은 중요한 변경 사항을 제공했다. 2001년 초에 새로운 L4 API (버전 X.2 일명 버전 4)를 출시한 후, 카를스루에 대학교의 시스템 아키텍처 그룹은 고성능과 이식성 모두에 중점을 둔 새로운 커널 L4Ka::Pistachio를 완전히 처음부터 구현했다. 이 커널은 2절 BSD 허가서에 따라 출시되었다.[8]
최신 Fiasco 버전
L4/Fiasco 마이크로커널도 수년간 광범위하게 개선되었다. 이제 x86, AMD64부터 여러 ARM 플랫폼에 이르는 여러 하드웨어 플랫폼을 지원한다. 특히, Fiasco 버전(Fiasco-UX)은 리눅스에서 사용자 수준 애플리케이션으로 실행될 수 있다.
L4/Fiasco는 L4v2 API에 대한 몇 가지 확장을 구현한다. 예외 IPC를 통해 커널은 CPU 예외를 사용자 수준 핸들러 애플리케이션으로 보낼 수 있다. alien thread의 도움으로 시스템 호출에 대한 세밀한 제어가 가능하다. X.2 스타일 UTCB가 추가되었다. 또한 Fiasco는 통신 권한 및 커널 수준 리소스 사용을 제어하는 메커니즘을 포함한다. Fiasco에서는 (2019년 5월 현재) 현재 리눅스 버전 (4.19)을 (L4Linux라고 불리는) 가상화하는 데 사용되는 기본 사용자 수준 서비스 모음(L4Env라고 불림)이 개발되었다.
뉴사우스웨일스 대학교 및 NICTA
개발은 뉴사우스웨일스 대학교 (UNSW)에서도 이루어졌으며, 이곳에서 개발자들은 여러 64비트 플랫폼에서 L4를 구현했다. 이들의 작업은 L4/MIPS 및 L4/Alpha를 만들어냈고, 리트케의 원래 버전은 소급하여 L4/x86으로 명명되었다. 리트케의 원래 커널처럼, UNSW 커널(어셈블리와 C의 혼합으로 작성됨)은 이식성이 없었으며 각각 처음부터 구현되었다. 고도로 이식 가능한 L4Ka::Pistachio가 출시되면서 UNSW 그룹은 자체 커널을 포기하고 L4Ka::Pistachio의 고도로 튜닝된 포트를 생산하는 데 집중했으며, 여기에는 역사상 가장 빠른 메시지 전달 구현(아이테니엄 아키텍처에서 36사이클)이 포함되었다.[9] 이 그룹은 또한 장치 드라이버가 커널 내부와 마찬가지로 사용자 수준에서도 동등하게 잘 작동할 수 있음을 입증했으며,[10] x86, ARM, MIPS 프로세서에서 실행되는 L4 기반 리눅스의 고도로 이식 가능한 버전인 Wombat을 개발했다. XScale 프로세서에서 Wombat의 컨텍스트 전환 비용은 기본 리눅스보다 최대 50배 낮다.[11]
나중에 현재 NICTA(이전 National ICT Australia, Ltd.)에 있는 UNSW 그룹은 L4Ka::Pistachio를 NICTA::L4-embedded라는 새로운 L4 버전으로 분기했다. 이 버전은 상업용 임베디드 시스템에 사용되었으며, 결과적으로 구현 트레이드오프는 작은 메모리 크기와 단순화된 복잡성을 선호했다. 높은 실시간 응답성을 보장하기 위해 거의 모든 시스템 호출이 선점 지점이 필요 없을 정도로 짧게 유지되도록 API가 수정되었다.[12]
상업적 배포
2005년 11월, NICTA는[13] 퀄컴이 자사의 Mobile Station Modem 칩셋에 NICTA의 L4 버전을 배포하고 있다고 발표했다. 이로 인해 2006년 말부터 판매되는 휴대 전화 핸드셋에 L4가 사용되었다. 2006년 8월, ERTOS 리더이자 UNSW 교수인 게르넛 하이저는 상업용 L4 사용자를 지원하고 NICTA와 긴밀히 협력하여 OKL4라는 브랜드 이름으로 상업용 L4를 추가로 개발하기 위해 오픈 커널 랩스 (OK Labs)라는 회사를 설립했다. 2008년 4월에 출시된 OKL4 μKernel 버전 2.1은 역량 기반 보안을 특징으로 하는 최초의 일반 공급 L4 버전이었다. 2008년 10월에 출시된 OKL4 μKernel 3.0은 OKL4 μKernel의 마지막 오픈 소스 버전이었다. 최신 버전은 OKL4 마이크로바이저라는 네이티브 하이퍼바이저 변형을 지원하기 위한 재작성을 기반으로 한 클로즈드 소스이다. OK Labs는 또한 Wombat의 후손인 OK:Linux라는 가상화된 리눅스와 심비안 OS 및 안드로이드의 가상화된 버전을 배포했다. OK Labs는 또한 NICTA로부터 seL4에 대한 권리를 획득했다.
OKL4 출하량은 2012년 초에 15억 개를 넘어섰으며,[5] 대부분 퀄컴 무선 모뎀 칩에 탑재되었다. 다른 배포에는 자동차 인포테인먼트 시스템이 포함된다.[14]
애플 A 시리즈 프로세서 중 A7부터는 2006년 NICTA에서 개발한 L4-embedded 커널을 기반으로 하는 sepOS(Secure Enclave Processor OS)라는 L4 운영체제를 실행하는 Secure Enclave 코프로세서를 포함한다.[15][16] 그 결과, 애플 실리콘을 탑재한 Mac을 포함한 모든 최신 애플 기기에 L4가 탑재되어 있다. 2015년에만 아이폰의 총 출하량은 3억 1천만 대로 추정되었다.[17]
Remove ads
고신뢰성: seL4
요약
관점
2006년에 NICTA 그룹은 공통평가기준과 그 이상과 같은 보안 요구사항을 충족시키는 데 적합한 고도로 안전하고 신뢰할 수 있는 시스템을 위한 기반을 제공하기 위해 seL4라는 3세대 마이크로커널을 처음부터 설계하기 시작했다. 처음부터 개발은 커널의 형식 검증을 목표로 했다. 성능과 검증이라는 때로는 상충되는 요구사항을 쉽게 충족하기 위해 팀은 하스켈 언어로 작성된 실행 가능한 명세에서 시작하는 중간-아웃 소프트웨어 프로세스를 사용했다.[18] seL4는 객체 접근성에 대한 형식적 추론을 가능하게 하는 역량 기반 보안 접근 제어를 사용한다.
기능적 정확성에 대한 형식 증명은 2009년에 완료되었다.[19] 이 증명은 커널의 구현이 사양에 대해 정확하다는 것을 보장하며, 교착 상태, 라이블록, 버퍼 오버플로, 산술 예외 또는 초기화되지 않은 변수 사용과 같은 구현 버그가 없음을 의미한다. seL4는 검증된 최초의 범용 운영체제 커널이라고 주장된다.[19] seL4에 대한 작업은 2019년 ACM SIGOPS 명예의 전당 상을 수상했다.
seL4는 커널 리소스 관리에 대한 새로운 접근 방식을 취하여[20] 커널 리소스 관리를 사용자 수준으로 내보내고 사용자 리소스와 동일한 역량 기반 접근 제어를 적용한다. 배럴피시도 채택한 이 모델은 격리 속성에 대한 추론을 단순화했으며, 나중에 seL4가 무결성 및 기밀성의 핵심 보안 속성을 시행한다는 증명을 가능하게 했다.[21] NICTA 팀은 또한 C 프로그래밍 언어에서 실행 가능한 기계어로의 번역의 정확성을 증명하여 컴파일러를 seL4의 신뢰할 수 있는 컴퓨팅 기반에서 제외시켰다.[22] 이는 커널 실행 파일에 대한 상위 수준 보안 증명이 유효함을 의미한다. seL4는 또한 하드 실시간 컴퓨팅에 사용하기 위한 전제 조건인 완전하고 건전한 최악 실행 시간(WCET) 분석을 포함하는 최초의 보호 모드 OS 커널이다.[21]
2014년 7월 29일, NICTA와 General Dynamics C4 Systems는 종단간 증명을 포함하는 seL4가 이제 오픈 소스 사용권으로 출시되었다고 발표했다.[23] 커널 소스 코드 및 증명은 GNU 일반 공중 사용 허가서 버전 2(GPLv2)에 따라 사용이 허가되었으며, 대부분의 라이브러리 및 도구는 BSD 2절에 따라 허가되었다. 2020년 4월, seL4의 개발 및 배포를 가속화하기 위해 리눅스 재단 산하에 seL4 재단이 설립되었다고 발표되었다.[24]
연구원들은 형식적 소프트웨어 검증 비용이 기존의 "고신뢰성" 소프트웨어 엔지니어링 비용보다 낮음에도 불구하고 훨씬 더 신뢰할 수 있는 결과를 제공한다고 말한다.[25] 특히, seL4 개발 중 코드 한 줄당 비용은 약 US$400으로 추정되며, 기존 고신뢰성 시스템의 경우 US$1,000과 비교된다.[26]
방위고등연구계획국(DARPA) 고신뢰성 사이버 군사 시스템(HACMS) 프로그램에 따라 NICTA는 프로젝트 파트너인 로크웰 콜린스, Galois Inc, 미네소타 대학교 및 보잉과 함께 seL4와 다른 보증 도구 및 소프트웨어를 사용하여 고신뢰성 드론을 개발했으며, 보잉이 개발 중인 선택적 유인 자율 보잉 AH-6 무인 리틀 버드 헬리콥터에 기술 이전을 계획했다. HACMS 기술의 최종 시연은 2017년 4월 버지니아주 스털링에서 진행되었다.[27] DARPA는 또한 존 런치베리가 시작한 프로그램에 따라 seL4 관련 중소기업 혁신 연구(SBIR) 계약에 자금을 지원했다. seL4 관련 SBIR을 받은 중소기업은 DornerWorks, Techshot, Wearable Inc, Real Time Innovations 및 Critical Technologies였다.[28]
2023년 10월, 니오 (기업)는 자사의 seL4 기반 SkyOS 운영체제가 2024년부터 양산되는 전기차에 탑재될 것이라고 발표했다.[29]
2023년에 seL4는 ACM 소프트웨어 시스템 상을 수상했다.
Remove ads
기타 연구 및 개발
하스켈로 작성된 OS인 Osker는 L4 사양을 목표로 했다. 이 프로젝트는 마이크로커널 연구가 아니라 OS 개발을 위한 함수형 프로그래밍 언어 사용에 주로 초점을 맞추었다.[30]
레독스 OS[31]는 seL4에서 영감을 얻었으며 마이크로커널 설계를 사용하는 Rust 기반 운영체제이다.
CodeZero[32]는 가상화 및 네이티브 OS 서비스 구현에 중점을 둔 임베디드 시스템용 L4 마이크로커널이다. GPL 라이선스 버전[33]과 B Labs Ltd.에서 라이선스를 다시 부여하고 엔비디아가 인수한 후 2010년에 클로즈드 소스로 분기된 버전이 있다.[34][35]
F9 마이크로커널[36]은 메모리 보호 기능이 있는 임베디드 장치용 ARM Cortex-M 프로세서 전용의 BSD 라이선스 L4 구현이다.
NOVA OS 가상화 아키텍처[37]는 작은 신뢰할 수 있는 컴퓨팅 기반으로 안전하고 효율적인 가상화 환경을 구축하는 데 중점을 둔 연구 프로젝트이다.[38][39] NOVA는 마이크로 하이퍼바이저, 사용자 수준 하이퍼바이저 (가상 머신 모니터) 및 그 위에서 실행되는 비특권 구성 요소화된 다중 서버 사용자 환경인 NUL로 구성된다. NOVA는 ARMv8-A 및 x86 기반 멀티 코어 시스템에서 실행된다.
WrmOS[40]는 L4 마이크로커널을 기반으로 하는 실시간 운영체제이다. 커널, 표준 라이브러리 및 네트워크 스택의 자체 구현을 가지고 있으며 ARM, SPARC, x86 및 x86-64 아키텍처를 지원한다. WrmOS에서 작동하는 가상화된 리눅스 커널(w4linux[41])이 있다.
Helios는 seL4에서 영감을 받은 마이크로커널이다.[42] Ares 운영체제의 일부이며 x86-64 및 aarch64를 지원하며 2023년 2월 현재 활발히 개발 중이다.[43]
Remove ads
같이 보기
- PikeOS
각주
더 읽어보기
외부 링크
Wikiwand - on
Seamless Wikipedia browsing. On steroids.
Remove ads