L4 마이크로커널 패밀리

L4 microkernel family
L4 마이크로커널 패밀리
개발자요헨 리트케
기입처어셈블리 언어, 다음으로 C, C++
OS 패밀리L4
동작 상태현재의
소스 모델오픈 소스, 클로즈드 소스
초기 릴리즈1993년; 29년 전(1993년)
마케팅 대상신뢰성 높은 컴퓨팅
이용가능기간:영어, 독일어
플랫폼인텔 i386, x86, x86-64, ARM, MIPS, SPARC
커널 타입마이크로커널
면허증.소스 코드, 증명: GPLv2
라이브러리, 도구: BSD 2-clause
선행유멜
공식 웹사이트os.inf.tu-dresden.de/L4

L4는 2세대 마이크로커널 패밀리로 다양한 유형의 운영체제(OS)를 구현하기 위해 사용되지만 대부분 Unix와 같은 Portable Operating System Interface(POSIX) 준거 타입에 적합합니다.

L4는 이전 마이크로커널 L3와 마찬가지로 독일 컴퓨터 과학자 요헨 리트케가 초기 마이크로커널 기반 OS의 성능 저하에 대한 대응으로 개발했습니다.Liettke는 처음부터 다른 목표가 아닌 고성능을 위해 설계된 시스템이 실용적인 마이크로커널을 생산할 수 있다고 생각했습니다.1993년 인텔 i386 고유의 어셈블리 언어 코드를 수작업으로 구현한 것이 컴퓨터 [citation needed]업계에 큰 관심을 불러일으켰습니다.도입 이후 L4는 크로스 플랫폼과 보안, 격리 및 견고성을 향상시키기 위해 개발되어 왔습니다.

원래의 바이너리 L4 커널 어플리케이션 바이너리 인터페이스(ABI)와 그 후속 버전에는 L4Ka를 포함한 다양한 재실장이 있었습니다.: 피스타치오(칼스루에 공과대학), L4/MIPS(뉴사우스웨일스대학(UNSW), Fiasco(드레스덴 공과대학(TU 드레스덴))이러한 이유로 L4라는 이름은 일반화되어 더 이상 Liettke의 원래 구현만을 지칭하지 않습니다.이제 L4 커널 인터페이스 및 다른 버전을 포함한 전체 마이크로커널 패밀리에 적용됩니다.

L4는 널리 배치되어 있습니다.Open Kernel Labs의 OKL4는 수십억 대의 모바일 [1][2]디바이스에 탑재되어 있습니다.

디자인 패러다임

Liettke는 마이크로커널의 일반적인 개념을 다음과 같이 기술하고 있습니다.

개념은 커널 외부로 이동하는 것, 즉 경쟁 구현을 허용하는 것이 시스템의 필수 기능을 [3]구현할 수 없는 경우에만 마이크로커널 내부에서 허용됩니다.

이 정신에서 L4 마이크로커널은 주소 공간(페이지 테이블 압축 및 메모리 보호 제공), 스레드 및 스케줄링(실행 압축 및 시간 보호 제공), 프로세스 간 통신(격리 경계 간 통신 제어) 등 기본적인 메커니즘을 거의 제공하지 않습니다.

L4와 같은 마이크로커널을 기반으로 하는 운영체제는 Linux나 구세대 마이크로커널과 같은 모노리식 커널이 내부적으로 포함하는 서버로서의 서비스를 사용자 공간에서 제공합니다.예를 들어, 안전한 Unix와 같은 시스템을 구현하려면 서버는 커널에 포함된 마하 권한 관리를 제공해야 합니다.

역사

마하와 같은 1세대 마이크로커널의 저조한 성능으로 인해 많은 개발자들이 1990년대 중반에 전체 마이크로커널 개념을 재검토하게 되었습니다.Mach에서 사용되는 비동기 커널 내 프로세스 통신 개념이 성능 저하의 주요 원인 중 하나로 판명되었습니다.이것에 의해, Mach 베이스의 operating system의 개발자는, 파일 시스템이나 드라이버 등, 몇개의 시간 크리티컬한 컴포넌트를 [citation needed]커널내로 이동시킬 수 있었습니다.이로 인해 성능 문제가 다소 개선되었지만 진정한 마이크로커널의 최소성 개념에 명백히 위배됩니다(또한 주요 장점도 낭비됩니다).

마하 병목현상에 대한 자세한 분석 결과, 특히 작업 세트가 너무 큰 것으로 나타났습니다.IPC 코드는 공간적 인접성이 낮다는 것을 나타냅니다.즉, 캐시 누락이 너무 많으며,[3] 그 대부분이 커널 내에 있습니다.이 분석을 통해 효율적인 마이크로커널은 성능에 중요한 코드의 대부분이 (최초 레벨) 캐시(가능하면 해당 캐시의 일부)에 들어갈 수 있을 정도로 작아야 한다는 원칙이 대두되었습니다.

L3

Jochen Liettke는 성능 및 머신 고유의 설계(크로스 플랫폼 소프트웨어와는 대조적으로)에 세심한 주의를 기울인 잘 설계된 프로세스 간 통신(IPC) 계층이 실제 환경에서 큰 성능 향상을 가져올 수 있다는 것을 증명하기 시작했습니다.마하의 복잡한 IPC 시스템 대신 L3 마이크로커널은 추가 오버헤드 없이 메시지를 전달했습니다.필요한 보안 정책을 정의하고 구현하는 것은 사용자 공간 서버의 의무로 간주되었습니다.커널의 역할은 사용자 수준의 서버가 정책을 적용할 수 있도록 하기 위해 필요한 메커니즘을 제공하는 것뿐입니다.1988년에 개발된 L3는 Technischer überwachungsverein(Technical Inspection Association)[citation needed]이 수년 동안 사용한 안전하고 견고한 운영 체제임을 입증했습니다.

L4 패밀리 트리

L4

L3를 사용해 본 결과, Liettke는 몇 가지 다른 마하 개념도 잘못 사용되고 있다는 결론을 내렸습니다.그는 마이크로커널 개념을 더욱 단순화함으로써 고성능을 주력으로 설계된 최초의 L4 커널을 개발했습니다.모든 성능을 추출하기 위해 전체 커널을 어셈블리 언어로 작성했으며 IPC는 [4]마하보다 20배 더 빨랐다.이러한 극적인 성능 향상은 운영 체제에서는 드문 일이며, Liettke의 연구는 L4의 새로운 구현과 Liettke가 1996년에 일하기 시작한 IBM, TU Dresden 및 UNSW를 포함한 많은 대학 및 연구소에서 L4 기반 시스템에 대한 작업을 촉발했습니다.IBM의 Thomas J. Watson Research Center Liedtke와 그의 동료들은 L4 및 마이크로커널 기반 시스템, 특히 Sawmill [5]OS에 대한 연구를 계속했습니다.

L4Ka: 하젤넛

1999년 Liettke는 Carlsruhe 대학의 시스템 아키텍처 그룹을 인수하여 마이크로커널 시스템에 대한 연구를 계속하였습니다.고성능 마이크로커널을 보다 높은 수준의 언어로 구성할 수 있다는 개념의 증거로서 이 그룹은 L4Ka를 개발했습니다.: Hazelnut: IA-32 및 ARM 기반 머신에서 동작하는 커널의 C++ 버전.그 노력은 성공적이었고, 성능은 여전히 만족스러웠으며, 출시와 함께 커널의 순수 어셈블리 언어 버전은 사실상 중단되었습니다.

L4/Faasco

L4Ka의 개발과 병행하여:: Hazelnut, 1998년 운영체제 그룹 TUD:TU Dresden의 OS는 L4/Fiasco라는 이름의 L4 커널 인터페이스의 C++ 구현을 자체 개발하기 시작했습니다.L4Ka와 대조적으로:: Hazelnut (커널에서의 동시 처리를 허용하지 않음)및 그 후속 L4Ka:: 특정 프리엠프션포인트에서만 커널 인터럽트를 허용하는 피스타치오에서는 L4/Fiasco는 (아토믹 오퍼레이션의 극히 짧은 것을 제외하고) 완전 프리엠프션으로 인터럽트 지연을 줄일 수 있었습니다.이는 L4/Fiasco가 Dreden에서 개발된 하드 실시간 컴퓨팅 지원 운영 체제인 [6]DROPS의 기반으로 사용되기 때문에 필요하다고 간주되었습니다.그러나 완전히 프리엠프션 가능한 설계의 복잡성으로 인해 이후 버전의 Fiasco는 제한된 수의 프리엠프션 포인트를 제외하고 인터럽트가 비활성화된 커널을 실행하는 전통적인 L4 접근 방식으로 돌아가게 되었습니다.

크로스 플랫폼

L4Ka: 피스타치오

L4Ka 출시까지:: 피스타치오 및 새로운 버전의 Fiasco에서는 모든 L4 마이크로커널은 기본적으로 기본 CPU 아키텍처와 밀접하게 연결되어 있었습니다.L4 개발의 다음 큰 변화는 크로스 플랫폼(플랫폼에 의존하지 않는) 애플리케이션 프로그래밍 인터페이스(API)의 개발로 높은 수준의 휴대성에도 불구하고 여전히 고성능 특성을 유지했습니다.커널의 기본 개념은 동일했지만, 새로운 API는 멀티프로세서 시스템의 더 나은 지원, 쓰레드와 주소 공간 간의 느슨한 연결, 사용자 수준 스레드 제어 블록(UTCB)과 가상 레지스터의 도입 등 이전 L4 버전에 비해 많은 중요한 변화를 제공했습니다.2001년 초에 새로운 L4 API(버전 X.2 a.k.a. 버전 4)를 출시한 후 Karlsruhe 대학의 System Architecture Group은 새로운 커널인 L4Ka를 구현했습니다.: 하이 퍼포먼스와 휴대성에 중점을 둔 피스타치오, 완전히 처음부터.2절 BSD [7]라이선스로 출시되었습니다.

새로운 버전의 Fiasco

L4/Fiasco 마이크로커널도 수년간 대폭 개선되었습니다.현재는 x86부터 AMD64까지 여러 하드웨어 플랫폼을 지원하고 있습니다.특히 Fiasco(Fiasco-UX) 버전은 Linux에서 사용자 수준의 애플리케이션으로 실행할 수 있습니다.

L4/Fiasco는 L4v2 API에 대한 몇 가지 확장을 구현합니다.예외 IPC 를 사용하면, 커널은 CPU 예외를 유저 레벨의 핸들러 애플리케이션에 송신할 수 있습니다.외부 스레드를 사용하여 시스템 호출을 세밀하게 제어할 수 있습니다. X.2 스타일의 UTCB가 추가되었습니다.또, Fiasco는, 통신권이나 커널 레벨의 자원 사용을 제어하는 메카니즘을 포함한다.Fiasco에서는 현재 Linux 버전(2019년 5월 기준 4.19개)을 패러 가상화하기 위해 사용되는 기본 사용자4 수준 서비스 모음(L4Env라는 이름)이 개발되어 있습니다.

뉴사우스웨일스 대학교 NICTA

개발은 뉴사우스웨일스대학(UNSW)에서도 이루어졌으며, 개발자들은 여러 64비트 플랫폼에 L4를 구현했습니다.그들의 작업은 L4/MIPS와 L4/Alpha를 낳았고, 결과적으로 Liettke의 원래 버전은 소급하여 L4/x86으로 명명되었다.Liedtke의 원래 커널과 마찬가지로 UNSW 커널(어셈블리와 C를 혼합하여 작성)은 포터블하지 않고 각각 처음부터 구현되었습니다.휴대성이 뛰어난 L4Ka 출시:: Pistachio, UNSW 그룹은 고도로 조정된 L4Ka 포트를 생성하기 위해 자체 커널을 포기했습니다.: 지금까지 보고된 것 중 가장 빠른 메시지 전달 구현(Itanium [8]아키텍처 36 사이클)을 포함한 피스타치오.이 그룹은 또한 디바이스 드라이버가 커널 [9]내와 마찬가지로 사용자 레벨에서도 뛰어난 성능을 발휘할 수 있다는 것을 증명하고 x86, ARM 및 MIPS 프로세서에서 실행되는 L4 상의 Linux의 이식성이 뛰어난 버전인 Wombat을 개발했습니다.XScale 프로세서에서 Wombat 컨텍스트 전환 비용은 기본 [10]Linux보다 최대 50배 낮습니다.

이후 UNSW 그룹은 NICTA(구 National ICT Australia, Ltd.)의 새 집에서 L4Ka를 포크로 삼았다.:NITA::L4-embedded라는 이름의 새로운 L4 버전으로 피스타치오.이름에서 알 수 있듯이, 이는 상용 임베디드 시스템에서 사용하기 위한 것이었고, 그 결과 구현의 트레이드오프는 작은 메모리 크기와 감소된 복잡성을 선호했습니다.이 API는 거의 모든 시스템콜이 높은 실시간 [11]응답성을 보장하기 위해 프리엠프션포인트가 필요 없을 정도로 짧게 유지되도록 변경되었습니다.

상용 도입

2005년 11월, NICTA는[12] 퀄컴이 모바일 스테이션 모뎀 칩셋에 NICTA의 L4 버전을 도입하고 있다고 발표했습니다.이에 따라 2006년 말부터 판매되는 휴대전화 단말기에 L4를 사용하게 됐다.2006년 8월 ERTOS 리더이자 UNSW 교수인 Gernot Heiser는 Open Kernel Labs(OK Labs)라는 이름의 회사를 설립하여 NICTA와 긴밀히 협력하여 상용 L4 사용자를 지원하고 브랜드 이름 OKL4로 L4를 더욱 개발하였습니다.2008년 4월에 출시된 OKL4 버전 2.1은 기능 기반 보안을 갖춘 L4의 첫 번째 일반 버전입니다.2008년 10월에 출시된 OKL4 3.0은 OKL4의 마지막 오픈 소스 버전입니다.최신 버전은 클로즈드 소스로, OKL4 마이크로바이저라는 네이티브 하이퍼바이저 변종을 지원하기 위한 개서를 기반으로 합니다.OK Labs는 또한 Wombat의 후손인 OK:Linux라는 이름의 반가상화 Linux와 Symbian의 반가상화 버전을 배포했습니다.OS와 안드로이드OK Labs는 NICTA로부터 seL4에 대한 권리도 취득했습니다.

OKL4 출하량은 주로 [2]퀄컴 무선 모뎀 칩에 의해 2012년 초에 15억대를 넘어섰습니다.기타 배치에는 자동차 인포테인먼트 [13]시스템이 포함됩니다.

A7부터 시작하는 Apple A 시리즈 프로세서에는 2006년 [15]NICTA에서 개발된 L4 임베디드 커널에 기반한 L4 운영[14] 체제를 실행하는 Secure Enclave 코프로세서가 포함되어 있습니다.이는 L4가 현재 모든 iOS 기기에서 출하되고 있음을 의미하며,[16] 2015년 총 출하량은 3억1000만대로 추정됩니다.

높은 보증성: seL4

2006년 NICTA 그룹은 공통기준 등의 보안요건을 충족하는 데 적합한 매우 안전하고 신뢰성 높은 시스템의 기반을 제공하기 위해 seL4라는 이름의 3세대 마이크로커널의 스크래치 설계를 시작했다.개발은 처음부터 커널의 정식 검증을 목표로 하고 있었다.퍼포먼스와 검증에 관해 때때로 모순되는 요건을 쉽게 충족시키기 위해 팀은 [17]Haskell로 작성된 실행 가능한 사양에서 시작하는 중간 규모의 소프트웨어 프로세스를 사용했습니다.seL4는 기능 기반의 보안 액세스 제어를 사용하여 객체 접근성에 대한 공식적인 추론을 가능하게 합니다.

기능적 정확성에 대한 공식적인 증명은 [18]2009년에 완료되었다.이 증명은 커널의 구현이 그 사양에 대해 올바르다는 보증을 제공하며, 데드록, 라이브록, 버퍼 오버플로, 산술 예외 또는 초기화되지 않은 변수의 사용과 같은 구현 버그가 없음을 암시합니다.seL4는 [18]최초로 검증된 범용 운영체제 커널이라고 합니다.

seL4는 커널 자원 [19]관리에 새로운 접근방식을 채택하여 커널 자원 관리를 사용자 수준으로 내보내고 사용자 리소스와 동일한 기능 기반 액세스 제어를 적용합니다.Barrelfish에 의해 채택된 이 모델은 격리 속성에 대한 추론을 단순화하고, seL4가 무결성과 [20]기밀성의 핵심 보안 속성을 강제한다는 이후 증거를 가능하게 했습니다.NICTA 팀은 또한 프로그래밍 언어 C에서 실행 가능한 머신 코드로의 변환이 올바른지 증명하여 컴파일러를 seL4의 [21]신뢰할 수 있는 컴퓨팅 기반에서 제외했습니다.이는 커널 실행 파일에 대한 높은 수준의 보안 증명이 유지됨을 의미합니다.또한 seL4는 하드 실시간 [20]컴퓨팅에서 사용하기 위한 필수 조건인 완전하고 건전한 WCET(Worst-Case Execution Time) 분석을 갖춘 최초의 공개 보호 모드 OS 커널입니다.

2014년 7월 29일, NICTA와 General Dynamics C4 Systems는 엔드 투 엔드 증명이 포함된 seL4가 오픈 소스 라이센스로 [22]출시되었다고 발표했습니다.커널 소스 코드와 증명은 GNU General Public License 버전 2(GPLv2)에 따라 라이선스가 부여되며 대부분의 라이브러리와 툴은 BSD 2 절에 따라 라이선스가 부여됩니다.2020년 4월, seL4의 [23]개발 및 도입을 가속화하기 위해 Linux Foundation 산하에 seL4 Foundation이 설립되었다고 발표했습니다.

연구자들은 정식 소프트웨어 검증 비용이 훨씬 더 신뢰할 수 있는 [24]결과를 제공함에도 불구하고 기존의 "고보증" 소프트웨어 엔지니어링 비용보다 낮다고 말합니다.특히, seL4 개발 중 코드 한 줄에 드는 비용은 약 400달러로 추정되었으며, 이는 기존의 고보증 시스템의 [25]경우 1,000달러로 추정되었습니다.

NICTA는 DARPA(Defense Advanced Research Projects Agency, DARPA) High-Assurance Cyber Military Systems(HACMS) 프로그램 하에서 프로젝트 파트너인 Rockwell Collins, Galois Inc, 미네소타 대학교 및 Boeing과 함께 SEL4를 사용하여 다른 보증 도구와 계획된 기술을 사용하여 고보증 드론을 개발했습니다.보잉사가 개발하고 있는 무인 보잉 AH-6 무인 리틀 버드 헬리콥터.HACMS 기술의 최종 시연은 2017년 [26]4월 버지니아 주 스털링에서 실시되었습니다.DARPA는 또한 John Launchbury 박사가 시작한 프로그램으로 seL4와 관련된 여러 SBIR(Small Business Innovative Research) 계약에 자금을 지원했습니다.seL4 관련 SBIR을 받는 스몰 비즈니스에는 다음이 포함됩니다.DornerWorks, Techshot, Wearable Inc, Real Time Innovations 및 Critical Technologies.[27]

기타 연구 개발

Haskell로 작성된 OS인 Osker는 L4 사양을 대상으로 했습니다.단, 이 프로젝트는 주로 마이크로커널 [28]연구가 아닌 OS 개발에 기능적인 프로그래밍 언어를 사용하는 것에 초점을 맞췄습니다.

Code[29] Zero는 임베디드 시스템용 L4 마이크로커널로 네이티브 OS 서비스의 가상화 및 구현에 중점을 두고 있습니다.GPL 라이선스 [30]버전과 Nvidia에 인수되어 2010년에 [31][32]분기된 B Labs Ltd.에 의해 유증된 버전이 있습니다.

F9 마이크로커널은 [33]BSD 라이선스의 L4 구현으로 메모리 보호 기능이 있는 딥 임베디드 디바이스용 ARM Cortex-M 프로세서 전용입니다.

NOVA OS 가상화 아키텍처는[34] 신뢰할 수 있는 컴퓨팅 기반의 안전하고 효율적인 가상화 환경을[35][36] 구축하는 데 중점을 둔 연구 프로젝트입니다.NOVA는 마이크로 하이퍼바이저, 사용자 수준의 하이퍼바이저(가상 머신 모니터) 및 NUL이라는 이름의 권한이 없는 컴포넌트화된 다중 서버 사용자 환경으로 구성됩니다.NOVA는 ARMv8-A 및 x86 기반 멀티 코어 시스템에서 실행됩니다.

WrmOS는[37] L4 마이크로커널 기반의 실시간 운영 체제입니다.커널, 표준 라이브러리 및 네트워크 스택을 자체 구현하여 ARM, SPARC, x86 및 x86-64 아키텍처를 지원합니다.WrmOS에서 작동하는 반가상화 Linux 커널(w4linux[38])이 있습니다.

「 」를 참조해 주세요.

레퍼런스

  1. ^ "Hypervisor Products: General Dynamics Mission Systems". General Dynamics Mission Systems. Archived from the original on 15 November 2017. Retrieved 26 April 2018.
  2. ^ a b "Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments" (Press release). Open Kernel Labs. 19 January 2012. Archived from the original on 11 February 2012.
  3. ^ a b Liedtke, Jochen (December 1995). "On µ-Kernel Construction". Proceedings 15th ACM Symposium on Operating Systems Principles (SOSP). pp. 237–250. Archived from the original on 25 October 2015.
  4. ^ Liedtke, Jochen (December 1993). "Improving IPC by kernel design". 14th ACM Symposium on Operating System Principles. Asheville, NC, USA. pp. 175–188.
  5. ^ Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathon; Deller, Luke; Reuther, Lars (2000). "The Sawmill multiserver approach". ACM SIGOPS European Workshop. Kolding, Denmark. pp. 109–114.
  6. ^ "DROPS - Overview". Dresden University of Technology. Archived from the original on 7 August 2011. Retrieved 10 August 2011.
  7. ^ l4ka.org: L4Ka:: 피스타치오 마이크로커널 견적: "..."지원되는 다양한 아키텍처는 L4Ka를 다음과 같이 만듭니다.: 다양한 시스템에 이상적인 연구 개발 플랫폼 구축."
  8. ^ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (April 2005). "Itanium: A system implementor's tale". USENIX Annual Technical Conference. Annaheim, CA, USA. pp. 264–278. Archived from the original on 17 February 2007.
  9. ^ Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot (September 2005). "User-level device drivers: achieved performance". Journal of Computer Science and Technology. 20 (5): 654–664. CiteSeerX 10.1.1.59.6766. doi:10.1007/s11390-005-0654-4. S2CID 1121537.
  10. ^ van Schaik, Carl; Heiser, Gernot (January 2007). "High-performance microkernels and virtualisation on ARM and segmented architectures". 1st International Workshop on Microkernels for Embedded Systems. Sydney, Australia: NICTA. pp. 11–21. Archived from the original on 1 March 2015. Retrieved 25 October 2015.
  11. ^ Ruocco, Sergio (October 2008). "A Real-Time Programmer's Tour of General-Purpose L4 Microkernels". EURASIP Journal on Embedded Systems. 2008: 1–14. doi:10.1155/2008/234710. S2CID 7430332.
  12. ^ "NICTA L4 Microkernel to be Utilised in Select QUALCOMM Chipset Solutions" (Press release). NICTA. 24 November 2005. Archived from the original on 25 August 2006.
  13. ^ "Open Kernel Labs Automotive Virtualization Selected by Bosch for Infotainment Systems" (Press release). Open Kernel Labs. 27 March 2012. Archived from the original on 2 July 2012.
  14. ^ "iOS Security, iOS 12.3" (PDF). Apple Inc. May 2019.
  15. ^ Mandt, Tarjei; Solnik, Mathew; Wang, David (31 July 2016). "Demystifying the Secure Enclave Processor" (PDF). BlackHat USA. Las Vegas, Nevada, USA. Archived (PDF) from the original on 21 October 2016.
  16. ^ Elmer-DeWitt, Philip (28 October 2014). "Forecast: Apple will ship 310 million iOS devices in 2015". Fortune. Archived from the original on 27 September 2015. Retrieved 25 October 2015.
  17. ^ Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; Cock, David; Chakravarty, Manuel M. T. (September 2006). "Running the manual: an approach to high-assurance microkernel development". ACM SIGPLAN Haskell Workshop. Portland, Oregon. pp. 60–71.
  18. ^ a b Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009). "seL4: Formal verification of an OS kernel" (PDF). 22nd ACM Symposium on Operating System Principles. Big Sky, MT, USA. Archived (PDF) from the original on 28 July 2011.
  19. ^ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (April 2008). Kernel design for isolation and assurance of physical memory. 1st Workshop on Isolation and Integration in Embedded Systems. Glasgow, UK. doi:10.1145/1435458. Retrieved 22 February 2020.
  20. ^ a b Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (February 2014). "Comprehensive Formal Verification of an OS Microkernel". ACM Transactions on Computer Systems. 32 (1): 2:1–2:70. CiteSeerX 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342.
  21. ^ Sewell, Thomas; Myreen, Magnus; Klein, Gerwin (June 2013). "Translation Validation for a Verified OS Kernel". ACM SIGPLAN Conference on Programming Language Design and Implementation. Seattle, WA, USA. doi:10.1145/2491956.2462183.
  22. ^ "Secure operating system developed by NICTA goes open source" (Press release). NICTA. 29 July 2014. Archived from the original on 15 March 2016.
  23. ^ "Security Gets Support of Linux Foundation" (Press release). Linux Foundation. 7 April 2020. Archived from the original on 15 March 2016.
  24. ^ Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (2014). "Comprehensive formal verification of an OS microkernel" (PDF). ACM Transactions on Computer Systems. 32: 64. CiteSeerX 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342. Archived (PDF) from the original on 3 August 2014.
  25. ^ Heiser, Gernot (16 January 2015). seL4 Is Free: What Does This Mean for You?. Auckland, New Zealand: Linux.conf.au.
  26. ^ "DARPA selects Rockwell Collins to apply cybersecurity technology to new platforms" (Press release). Rockwell Collins. 24 April 2017. Archived from the original on 11 May 2017.
  27. ^ "DARPA Agency Sponsor Dr. John Launchbury". SBIRSource. 2017. Archived from the original on 29 September 2017. Retrieved 16 May 2017.
  28. ^ Hallgren, T.; Jones, M.P.; Leslie, R.; Tolmach, A. (2005). "A principled approach to operating system construction in Haskell" (PDF). Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming. 40 (9): 116–128. doi:10.1145/1090189.1086380. ISSN 0362-1340. Archived (PDF) from the original on 15 June 2010. Retrieved 24 June 2010.
  29. ^ "Announce: Introducing Codezero". Dresden University of Technology.
  30. ^ "jserv/codezero: Codezero Microkernel". GitHub. Archived from the original on 15 August 2015. Retrieved 20 October 2020.
  31. ^ "Code Zero : Embedded Hypervisor and OS". Archived from the original on 11 January 2016. Retrieved 25 January 2016.
  32. ^ "Archived copy". Archived from the original on 2 February 2014. Retrieved 2 February 2014.{{cite web}}: CS1 maint: 제목으로 아카이브된 복사(링크)
  33. ^ "F9 Microkernel". GitHub. Retrieved 20 October 2020.
  34. ^ "NOVA Microhypervisor website". Retrieved 9 January 2021.
  35. ^ Steinberg, Udo; Kauer, Bernhard (April 2010). "NOVA: A Microhypervisor-Based Secure Virtualization Architecture". EuroSys '10: Proceedings of the 5th European Conference on Computer Systems. Paris, France.
  36. ^ Steinberg, Udo; Kauer, Bernhard (April 2010). "Towards a Scalable Multiprocessor User-level Environment". IIDS'10: Workshop on Isolation and Integration for Dependable Systems. Paris, France.
  37. ^ "WrmOS". Retrieved 20 October 2020.
  38. ^ "w4linux is paravirtualized Linux kernel working on WrmOS". Retrieved 20 October 2020.

추가 정보

  • Liedtke, Jochen; Bartling, Ulrich; Beyer, Uwe; Heinrichs, Dietmar; Ruland, Rudolf; Szalay, Gyula (April 1991). "Two years of experience with a μ-Kernel based OS". ACM SIGOPS Operating Systems Review. 25 (2): 51–62. doi:10.1145/122120.122124.
  • Liedtke, Jochen, Haeberlen, 안드레아스, 공원, Yoonho, 전 미국 자동차 노조 위원장, 라르스;Uhlig, Volkmar(222000년 10월)."Stub-Code 성능 중요한이 되는 것은".1워크숍 산업 체험 시스템 소프트웨어에 회보(WIESS), 샌 디에이고, CA, 2000년 10월.52006년 9월에 있는 원본(PDF)에서 Archived.52006년 9월.(L4커널과 컴파일러에)Retrieved.
  • Cheng, Guanghui; McGuire, Nicholas. L4/Fiasco/L4Linux Kickstart (PDF). Distributed & Embedded Systems Lab (Report). Lanzhou University. Archived from the original (PDF) on 27 March 2012.
  • Elphinstone, 케빈;Heiser, Gernot(2013년 11월)."L3seL4까지:뭐 본 적 있어 우리는 Learnt L4Microkernels의 20년 만에?"(PDF). 24일 ACMSIGOPS 심포지엄 지원되는 운영 시스템 원리에.Farmington, 1939, 미국.를 대신하여 서명함. 133–150.CiteSeerX 10.1.1.636.9410. doi:10.1145/2517349.2522720.아이 에스비엔 978-1-4503-2388-8.L4설계 및 구현 접근 방식의 진화.

외부 링크