seL4 프로젝트, ACM 소프트웨어 시스템 어워드 수상

seL4 개방형 마이크로커널 프로젝트가 컴퓨터 시스템 분야에서 가장 권위 있는 국제기구인 ACM(Association for Computing Machinery)이 매년 수여하는 ACM 소프트웨어 시스템 어워드(ACM Software System Award)를 수상했다. 이상은 공식 언어로 제공된 사양을 완전히 준수하고 미션 크리티컬 애플리케이션에서 사용할 준비가 되었음을 인정하는 수학적 작동 증명 분야의 성과에 대해 수여됩니다. seL4 프로젝트는 산업용 운영 체제 수준에서 프로젝트에 대한 신뢰성과 보안을 완전히 공식적으로 검증할 수 있을 뿐만 아니라 성능과 다양성을 희생하지 않고도 이를 달성할 수 있음을 보여주었습니다.

ACM 소프트웨어 시스템 어워드는 업계에 결정적인 영향을 미치고 새로운 개념을 도입하거나 새로운 상용 애플리케이션을 개척한 소프트웨어 시스템의 개발을 인정하기 위해 매년 수여됩니다. 상금은 미화 35달러입니다. 지난 몇 년 동안 ACM 상은 GCC 및 LLVM 프로젝트와 설립자 Richard Stallman 및 Chris Latner에게 수여되었습니다. UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB 및 eclipse도 수상한 다른 프로젝트 및 기술입니다. .

마이크로커널 seL4의 아키텍처는 사용자 공간에서 커널 자원을 관리하기 위한 부분을 제거하고 이러한 자원에 대해 사용자 자원과 동일한 액세스 제어 수단을 적용한다는 점에서 주목할 만합니다. 마이크로커널은 파일, 프로세스, 네트워크 연결 등을 관리하기 위한 즉시 사용 가능한 고급 추상화를 제공하지 않으며 대신 물리적 주소 공간, 인터럽트 및 프로세서 리소스에 대한 액세스를 제어하기 위한 최소한의 메커니즘만 제공합니다. 하드웨어와 상호 작용하기 위한 고수준 추상화 및 드라이버는 사용자 수준 작업의 형태로 마이크로커널 위에 별도로 구현됩니다. 마이크로커널에서 사용할 수 있는 리소스에 대한 이러한 작업의 액세스는 규칙 정의를 통해 구성됩니다.

출처 : opennet.ru