The seL4 Microkernel - An Introduction

Gernot Heiser
University of New South Wales
The seL4 Foundation, 2020
Google Scholar Citations:

本文是seL4官网对于seL4的一个介绍, 主要贡献是介绍了seL4的特点.

seL4首先是一个微内核, 是hypervisor, 可以在seL4运行主流OS的虚拟机
seL4被形式化证明了实现正确性: 将C源码和编译后的二进制指令分别抽象为图的形式, 证明二者等价性
与传统的UNIX permissions不同, seL4使用capabilities来实现更精细的访问控制
seL4是一个硬实时系统, 它有完整而可靠的最坏情况执行时间(WCET)分析

L4 Microkernels: The Lessons from 20 Years of Research & Deployment

Gernot Heiser, Kevin Elphinstone
University of New South Wales
ACM Transactions on Computer Systems (TOCS), 2016
Google Scholar Citations:

本文主要贡献是总结20多年来L4微内核设计与实现的演变.

seL4保留了最小性作为关键设计原则, 保留了通用性(几乎支持任意系统架构)
seL4被形式化证明了实现正确性: 将C源码和编译后的二进制指令分别抽象为图的形式, 证明二者等价性
与传统的UNIX permissions不同, seL4使用capabilities来实s现更精细的访问控制
seL4是一个硬实时系统, 它有完整而可靠的最坏情况执行时间(WCET)分析

Improving IPC by Kernel Design

Jochen Liedtke
German National Research Center for Computer Science (GMD)
Proceedings of the ACM symposium on Operating systems principles (SOSP), 1993
Google Scholar Citations:

本文主要贡献是给出提升IPC性能的技术, 并在Intel 486 DX-50处理器(50 MHz)测试L4的IPC性能, 一次短IPC的平均时间为5.2微秒, 与Mach相比提升22倍.

增加新的系统调用call和reply & receive next, 将原来4个系统调用降到2个
临时映射
Lazy Scheduling
Direct Process Switch
使用寄存器传递短消息

On Micro-Kernel Construction

Jochen Liedtke
German National Research Center for Computer Science (GMD)
Proceedings of the ACM symposium on Operating systems principles (SOSP), 1995
Google Scholar Citations:

现代微内核开山之作, 指出微内核在软件理念上优于宏内核: 更模块化的系统结构, 各个组件故障相互独立, 系统定制更加灵活.
虽然优点众多, 但是在当时微内核的效率过于低下而被抛弃, 错过操作系统发展的最佳时期. 作者认为合理的微内核设计在保留微内核优点的同时, 能达到优秀性能.
他在本文给出微内核实现时应当遵循的一些理念:

地址空间: 微内核提供简单基本的保护, 隐藏硬件层面地址空间, 同时必须支持内核之上实现地址空间的递归构建
线程和IPC: 为线程提供唯一的标识符(UID)
将内存管理、分页器、设备驱动器、二级Cache快表、Unix系统调用等移至用户态, 减小内核体积
将微内核做成机器相关, 舍弃可移植性, 针对不同处理器架构做优化, 提升微内核性能

The Performance of Micro-Kernel-Based Systems

Hermann Härtig, Michael Hohmuth, Jochen Liedtke, Sebastian Schönberg, Jean Wolter
Dresden University of Technology
Proceedings of the ACM symposium on Operating systems principles (SOSP), 1997
Google Scholar Citations:

首次将Linux移植到L4内核上, 根据L4提供的接口对Linux进行一定修改, 称为L4Linux. 本文将原生Linux与L4Linux做性能对比, 测试结果为在实际应用场景下L4Linux慢5%-10%, 证明L4与第一代微内核相比有显著的性能提升并且具有实际应用价值.

seL4: Formal Verification of an OS Kernel

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
University of New South Wales
Proceedings of the ACM symposium on Operating systems principles (SOSP), 2009
Google Scholar Citations:

首次提出seL4, 第一个对通用操作系统内核功能正确性的形式化证明. 本文关注功能正确性的证明, 从高阶逻辑到C语言实现, 不包括二进制部分.

Comprehensive formal verification of an OS microkernel

Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, Gernot Heiser, Authors Info & Claims
University of New South Wales
ACM Transactions on Computer Systems (TOCS), 2014
Google Scholar Citations:

本文是对seL4更完整的形式化证明, 不仅是功能正确性, 而且证明了二进制文件正确性.

First steps in verifying the seL4 Core Platform

Mathieu Paturel, Isitha Subasinghe, Gernot Heiser
University of New South Wales
Proceedings of the ACM SIGOPS Asia-Pacific Workshop on Systems (APSys), 2023
Google Scholar Citations:

本文指出seL4面临的挑战: seL4只是一个微内核, 不提供应用程序依赖的服务(文件系统, 网络服务, 资源管理), 在seL4上构建完整的操作系统十分困难, 需要较高的专业水平. seL4 Core Platform是一个用于在seL4上构建系统服务和应用程序的框架, seL4CP仍不兼容POSIX并且目前没有给出解决方案, 计划未来版本提供虚拟机抽象层运行遗产软件.

An Architectural Overview of QNX

Dan Hildebrand
Quantum Software Systems
USENIX Workshop on Microkernels and Other Kernel Architectures, 1992
Google Scholar Citations:

本文介绍QNX架构. 与seL4类似, QNX内核仅保留了IPC, 调度器, 中断控制和低级网络通信. 与seL4不同, QNX兼容POSIX并且能直接在用户态添加可选的进程 (设备管理器, 文件系统管理器等). 这种设计为QNX带来易用性, 在嵌入式领域得到非常广泛的应用, 我觉得这是L4家族最薄弱的地方. QNX也证明微内核理念没有问题, 在工业界可行.

To Preempt or Not To Preempt, That Is the Question

Bernard Blackham, Vernon Tang and Gernot Heiser
University of New South Wales
Proceedings of the Asia-Pacific Workshop on Systems (APSys), 2012
Google Scholar Citations:

RTOS为了降低中断延时通常设计为完全抢占式 (在内核执行时, 随时可以处理中断). 但这种设计带来高并发, 难以分析和Debug. 因此seL4采取非抢占式 (在内核执行时, 禁用中断, 只在某些时刻处理中断), 为形式化验证牺牲一部分性能. 本文对seL4和QNX最坏情况下中断延时进行分析, 最终结果是seL4大约为qnx的1.5倍, 得出结论: 合理设计的非抢占式内核可以达到与抢占式内核相当的中断延时. 对于RTOS, 采用非抢占式是可行的.

Improving Interrupt Response Time in a Verifiable Protected Microkernel

Bernard Blackham, Yao Shi, Gernot Heiser
University of New South Wales
Proceedings of the ACM European Conference on Computer Systems (EuroSys), 2012
Google Scholar Citations:

本文探讨降低非抢占式微内核中断延时的方法. seL4在内核执行时禁用中断, 当遇到抢占点或刚返回用户态时处理中断. 这种设计是为形式化验证做出让步, 增加一定中断延时, 作者探讨降低延时的方法并测量改进后的性能.
线程调度优化:

seL4最初使用Lazy Scheduling: 当前线程被IPC阻塞时仍加入就绪队列, 只是被标记为阻塞状态, 当调度器下次被调用时, 将仍被阻塞的线程出队. 这样的设计是考虑到seL4的同步IPC模型, 线程发送消息时被阻塞, 但通常又很快收到回复, 一般的调度策略会造成频繁地出队入队. 但是这种设计无法保证最坏情况性能
使用Benno Scheduling优化: 当前线程被IPC阻塞时不加入就绪队列, 放入阻塞队列. 另一方面, 当一个线程被IPC唤醒且具有高优先级, 直接切换到这个线程而不是将它放入就绪队列. 这种设计的平均性能与Lazy相同, 并保证了最坏情况性能

Timing Analysis of a Protected Operating System Kernel

Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury, Gernot Heiser
University of New South Wales
Proceedings of the 32nd IEEE Real-Time Systems Symposium (RTSS ), 2011
Google Scholar Citations:

本文分析seL4最坏情况中断延时. 文章对seL4中系统调用和中断延时分别进行静态分析和实际硬件上的测量.

Verified Protection Model of the seL4 Microkernel

Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone
University of New South Wales
Verified Software: Theories, Tools, Experiments: Second International Conference (VSTTE), 2008
Google Scholar Citations:

本文对seL4访问控制模型进行形式化验证, 证明seL4权能系统支持两个子系统之间的强制隔离.

在seL4中, 线程、内存、IPC都完全通过Capability管控.
在boot时, seL4预分配内核运行需要的所有内存, 剩余的内存完全由Resource Manager (RM) 管理和分配. 任何程序的行为都受到RM授予的Capability限制.
文章形式化证明了RM为子系统提供初始Capabilities后, 子系统内部只能获取这些Capabilities, 无法跨越边界获取其他子系统的Capabilities.

seL4 Enforces Integrity

Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June, Andronick, Gerwin Klein
University of New South Wales
International Conference on Interactive Theorem Proving(ITP), 2011
Google Scholar Citations:

本文形式化证明seL4微内核权能系统的两个高级访问控制特性: integrity和authority confinement.

integrity是指只有拥有相应权能才能对相应对象进行写操作
authority confinement是指除非明确指明, 权能不会在子系统之间转移

Scheduling-context capabilities: A principled, light-weight operating-system mechanism for managing time

Anna Lyons, Kent McLeod, Hesham Almatary, Gernot Heiser
University of New South Wales
Proceedings of the ACM European Conference on Computer Systems (EuroSys), 2018
Google Scholar Citations:

本文提出一种在seL4中基于权能系统来控制CPU时间的模型, 将CPU时间抽象为名为scheduling-context的对象, 这个对象包含Budget (运行时间), Period (运行周期), 处理器ID等信息. 这个模型使得seL4权能系统同时支持空间分区和时间分区, 为混合严重性系统(MCS)提供强大支持.

An Overview of Microkernel, Hypervisor and Microvisor Virtualization Approaches for Embedded Systems

Asif Iqbal, Nayeema Sadeque and Rafika Ida Mutia
Department of Electrical and Information Technology, Lund University, Sweden
Report, 2010
Google Scholar Citations:

本文阐述微内核一个重要应用领域: 在嵌入式系统中的虚拟化作用并讨论三种虚拟化实现方法: microkernel、hypervisor和microvisor(OKL4). microkernel和hypervisor的主要区别. 本文认为OKL4融合hypervisor和microkernel, 同时达到低虚拟机监控开销和小尺寸, 是很优秀的技术.

The OKL4 microvisor: convergence point of microkernels and hypervisors

Gernot Heiser, Ben Leslie
University of New South Wales
Proceedings of the Asia-Pacific Workshop on Systems (APSys), 2010
Google Scholar Citations:

本文指出针对microkernel和hypervisor的讨论已经没有意义, 两者有许多共同之处并提供类似的抽象. 实现一个名为OKL4的microvisor, 结合了microkernel和hypervisor两个模型并证明它满足虚拟化的最小开销这一hypervisor的目标, 同时也满足microkernel最小尺寸这一目标.

SemperOS: A Distributed Capability System

Matthias Hille, Nils Asmussen, Pramod Bhatotia, Hermann Härtig
Technische Universität Dresden, The University of Edinburgh, Barkhausen Institute
Proceedings of the USENIX Conference on Usenix Annual Technical Conference (ATC), 2019
Google Scholar Citations:

本文提出一种可扩展的分布式权能系统, 并实现了一个名为SemperOS的多内核OS来运行这个系统..

XPC: Architectural Support for Secure and Efficient Cross Process Call

Dong Du, Zhichao Hua, Yubin Xia, Binyu Zang, Haibo Chen
Institute of Parallel and Distributed Systems, Shanghai Jiao Tong University
Proceedings of the International Symposium on Computer Architecture (ISCA), 2019
Google Scholar Citations:

本文实现一个名为XPC的原语, 用于同步IPC. 与以往优化IPC的方法相比, XPC最大特点是不需要陷入内核, 而且XPC做到零复制成本消息传递.

SkyBridge: Fast and Secure Inter-Process Communication for Microkernels

Zeyu Mi, Dingji Li, Zihan Yang, Xinran Wang, Haibo Chen
Institute of Parallel and Distributed Systems, Shanghai Jiao Tong University
Proceedings of the ACM European Conference on Computer Systems (EuroSys), 2019
Google Scholar Citations:

本文实现一个名为SkyBridge的同步IPC设计, 它利用Intel芯片的VMFUNC指令来切换虚拟地址空间, 从而直接切换到目标进程(不需要陷入内核). 但很明显SkyBridge不能跨硬件平台, 而且消息传递不是零复制成本.

Harmonizing Performance and Isolation in Microkernels with Efficient Intra-kernel Isolation and Communication

Jinyu Gu, Xinyue Wu, Wentai Li, Nian Liu, Zeyu Mi, Yubin Xia, Haibo Chen
Institute of Parallel and Distributed Systems, Shanghai Jiao Tong University
Proceedings of the USENIX Conference on Usenix Annual Technical Conference (ATC), 2019
Google Scholar Citations:

本文实现一个名为UnderBridge的IPC设计, 核心思想是在内核态中划分出各个相互独立的保护域, 将系统服务重新放回内核态, 运行在这些独立的保护域中. 这种设计维持各组件之间相互独立, 并且系统调用像宏内核一样只需要两次模式切换. UnderBridge同样不能跨硬件平台, 内核态相互独立的保护域依赖Intel硬件设施MPK.

TreeSLS: A Whole-system Persistent Microkernel with Tree-structured State Checkpoint on NVM

Fangnuo Wu, Mingkai Dong, Gequan Mo, Haibo Chen
Institute of Parallel and Distributed Systems, Shanghai Jiao Tong University
Proceedings of the ACM symposium on Operating systems principles (SOSP), 2023
Google Scholar Citations:

传统单层存储(Single-level Store, SLS)可以解决数据持久化问题, 但开销大性能低而且不支持透明的外部同步性. 本文提出TreeSLS, 一种基于非易失性存储器(Non-Volatile Memory, NVM)低开销、具有透明外部同步性的SLS系统.
TreeSLS采用微内核架构, 一方面因为微内核大大简化内核状态, 系统服务基本在用户态, 所以设计检查点时不用了解这些复杂的系统对象; 另一方面微内核通常使用权能系统, 如果将这些权能对象组织为树形结构, 整个系统的状态就被抽象为这棵树, 以进行高效的增量状态检查点.

Scale and Performance in a Filesystem Semi-Microkernel

Jing Liu, Anthony Rebello, Yifan Dai, Chenhao Ye
University of Wisconsin-Madison
Proceedings of the ACM symposium on Operating systems principles (SOSP), 2021
Google Scholar Citations:

半微内核是指将操作系统某个系统服务移至用户态, 大部分功能仍然保留在内核态. 半微内核概念兴起于网络领域, 本文注意到网络系统和文件系统的相似性, 用半微内核架构实现名为uFS的本地文件系统(文件系统作为用户进程).
采用微内核设计的文件系统能摆脱传统宏内核限制:

快速开发和部署: 像开发应用一样开发文件系统, 不用修改内核
突破宏内核文件系统性能瓶颈: 用户进程进行文件操作时直接请求用户级文件系统, 不需要陷入内核, 减少两次模式切换. 新出现的SPDK使得用户级进程可以直接访问存储设备, 完全不需要内核参与

Snap: a Microkernel Approach to Host Networking

Michael Marty, Marc de Kruijf, Jacob Adriaens, Christopher Alfeld, Sean Bauer, Carlo Contavalli Michael Dalton, Nandita Dukkipati, William C. Evans, Steve Gribble, Nicholas Kidd, Roman Kononov, Gautam Kumar, Carl Mauer, Emily Musick, Lena Olson, Erik Rubow, Michael Ryan, Kevin Springborn, Paul Turner, Valas Valancius, Xi Wang, and Amin Vahdat
Google
Proceedings of the ACM symposium on Operating systems principles (SOSP), 2019
Google Scholar Citations:

随着网络硬件的发展、云计算以及高性能分布式系统的兴起, 主机对网络服务的需求非常广泛并且变化迅速. 但传统的网络服务在操作系统内核中实现, 宏内核代码复杂与大体量使得新的网络功能无法高效开发. 同时, 对于内核的更新需要终止其上运行的应用程序, 在工业界中这一成本十分高昂.
于是Google借鉴微内核思想, 将网络服务移出内核, 作为用户级进程, 设计名为Snap的框架. 通过引入微内核架构, Snap既能中心化地管理网络资源, 而且避免内核中开发网络功能的繁琐. Snap被Google在工业界大规模部署, 它带来的快速更新迭代的优点在工业化产品中尤为重要.

EPK: Scalable and Efficient Memory Protection Keys

Jinyu Gu, Hao Li, Wentai Li, Yubin Xia, Haibo Chen
Institute of Parallel and Distributed Systems, Shanghai Jiao Tong University
Proceedings of the USENIX Conference on Usenix Annual Technical Conference (ATC), 2022
Google Scholar Citations:

Intel推出的MPK技术支持单个地址空间内至多16个互相隔离的内存域, 本文提出EPK设计, 将其拓展至8192个内存域, 大幅增加了可用场景. 本文延续UnderBridge思路, 基于EPK提出名为HyBridge的IPC设计: 将通信频繁的用户级系统服务进程放在同一地址空间中互相隔离的不同内存域中. 这与UnderBridge非常类似, 但在两个方面做的更好: UnderBridge有16个内存域的限制, 至多容纳16个系统服务; UnderBridge因为把系统服务放回内核态, 所以应用调用后仍需要两次页表切换, 但HyBridge没有这个开销.

RedLeaf: Isolation and Communication in a Safe Operating System

Vikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel, Zhaofeng Li, Gerd Zellweger, Anton Burtsev
The George Washington University
Proceedings of the Conference on Operating Systems Design and Implementation, 2020
Google Scholar Citations:

与以往使用硬件机制(Intel MPK, VMFUNC)来完成子系统之间的隔离不同, 本文旨在实现一种基于程序设计语言的轻量级细粒度域隔离. 本文使用Rust开发名为RedLeaf的微内核操作系统, 利用Rust语言的类型与内存安全性实现隔离域.

Fine-Grained Isolation for Scalable, Dynamic, Multi-tenant Edge Clouds

Yuxin Ren, Guyue Liu, Vlad Nitu, Wenyuan Shao, Riley Kennedy, Gabriel Parmer, Timothy Wood, Alain Tchana
The George Washington University
Proceedings of the USENIX Conference on Usenix Annual Technical Conference (ATC), 2020
Google Scholar Citations:

现有操作系统难以满足5G边缘云的应用场景: 为大量客户提供高性能多样化的云服务, 同时提供强大客户隔离和服务隔离. 本文采用微内核架构实现名为EdgeOS的操作系统, 核心设计是为每个客户动态增加一个新的隔离域, 并使用数据复制完成消息传递.

Twizzler: a Data-Centric OS for Non-Volatile Memory

Daniel Bittman, Peter Alvaro, Pankaj Mehra, Darrell D. E. Long, Ethan L. Miller
UC Santa Cruz
Proceedings of the USENIX Conference on Usenix Annual Technical Conference (ATC), 2020
Google Scholar Citations:

可字节寻址的非易失存储(Non-Volatile Memory, NVM)为程序操作持久性数据提供一种全新方式. 现有操作系统的文件I/O接口(read, write)无法充分发挥NVM优势: NVM读写延时很低, 如果直接引入NVM会使得系统调用带来的陷入内核开销反而占据主导.
本文重新设计名为Twizzler的操作系统, 借鉴微内核思想, 将内核从I/O路径中移除, 直接为程序提供内存式持久性数据访问.

M³x: Autonomous Accelerators via Context-Enabled Fast-Path Communication

Nils Asmussen, Michael Roitzsch, Hermann Härtig
Technische Universität Dresden, Germany
Proceedings of the USENIX Conference on Usenix Annual Technical Conference (ATC), 2019
Google Scholar Citations:

传统的进程间通信如管道, 套接字和微内核IPC都需要内核的干涉. 于是名为fast-path communication的通信技术被提出, 它绕过内核从而降低开销. 但由于内核不参与通信, 将fast-path communication与上下文切换结合很困难, 本文提出M³x设计将这二者结合, 实现自主加速器.
这种设计为微内核IPC技术发展带来启发.

QNX Neutrino Documentation

Mike Cramer
Quantum Software Systems

介绍QNX系统架构和设计思想的网站. 介绍QNX内核的结构、函数功能和IPC设计以及QNX作为用户进程的进程管理器、文件系统管理器、设备管理器和网络管理器。

HarmonyOS Overview

HUAWEI

华为官方对鸿蒙操作系统的一个概述. 鸿蒙是定位于万物互联的分布式操作系统, 总体架构可以分为四层: 内核层, 系统服务层, 框架层和应用层.

内核层: 鸿蒙采用多内核设计, 使它能适应不同硬件配置的设备, 在内核子系统上有一层内核抽象层, 为上层提供基本的内核功能, 这一层抹去了底层不同内核实现的区别, 使得不同的内核实现对上层来说是透明的. 内核层还包括驱动子系统, 驱动子系统中有硬件驱动基础(HDF), 这一点为构建鸿蒙硬件生态系统打下基础
系统服务层: 由四个部分组成, 分别是基本系统功能子系统集, 基本软件服务子系统集, 增强的软件服务子系统集和硬件服务子系统集. 除了基本系统功能子系统集, 其他三个子系统集可以根据要部署的设备类型进行定制化处理
框架层: 提供开发鸿蒙应用所需的框架, 包括应用框架, UI框架, 以及软硬件服务的API
应用层: 系统应用及第三方应用运行在这层

HarmonyOS 2 Security Technical White Paper

HUAWEI

描述鸿蒙操作系统安全技术与功能的白皮书. 鸿蒙的安全机制可以概括为: 保证正确的人通过正确的设备使用正确的数据. 通过"分布式多端协同身份认证"来保证"正确的人", 通过"在分布式终端上构筑可信运行环境"来保证"正确的设备", 通过"分布式数据在跨终端流动的过程中，对数据进行分类分级管理"来保证"正确的数据".

HarmonyOS 2 Security Technical White Paper

HUAWEI

华为官网对于鸿蒙操作系统安全技术的介绍.

Huawei Mine Harmony

HUAWEI

鸿蒙操作系统在工业界的应用. 矿鸿是华为基于鸿蒙开发的操作系统, 针对安全可信能力做了增强，保障设备、应用、数据和服务安全, 并对煤矿行业定制功能增强套件, 包括面向煤矿实际生产场景的软总线通信、设备鉴权与认证、近场发现与连接等功能, 根据煤矿生产实际需求, 开发适用于煤矿行业的矿鸿国产操作系统, 实现完全安全可信

HarmonyOS Smart Cockpit

HUAWEI

基于鸿蒙开发的车载操作系统.

ghOSt: Fast & Flexible User-Space Delegation of Linux Scheduling

Jack Tigar Humphries, Neel Natu, Ashwin Chaugule, Ofir Weisse, Barret Rhoden, Josh Don, Luigi Rizzo, Oleg Rombakh, Paul Turner, Christos Kozyrakis
Google
Proceedings of the ACM symposium on Operating systems principles (SOSP), 2021
Google Scholar Citations:

本文指出大型云服务提供商通常需要根据客户需求来定制新的调度策略来达到最佳性能. 然而Linux的调度模块集成在内核之中, 实现一个新的调度器非常困难, 而将新的调度器部署到服务器甚至更加困难, 大大降低开发效率. 本文提出ghOSt, 将Linux调度程序开发从内核态移动至用户进程, 大大提高灵活性, 同时保证调度开销较低.

Direct Inter-Process Communication (dIPC): Repurposing the CODOMs Architecture to Accelerate IPC

Lluís Vilanova, Marc Jordà, Nacho Navarro, Yoav Etsion, Mateo Valero
Universitat Polit`ecnica de Cataluny
Proceedings of the ACM European Conference on Computer Systems (EuroSys), 2017
Google Scholar Citations:

本文实现dIPC, 利用CODOMs体系架构优化IPC, 将进程映射到共享地址空间, 允许线程以安全的方式直接在进程之间执行常规的函数调用, 将内核从IPC关键路径中移除, 大大提高IPC效率.

Time Protection: The Missing OS Abstraction

Qian Ge, Yuval Yarom, Tom Chothia, Gernot Heiser
University of New South Wales
Proceedings of the ACM European Conference on Computer Systems (EuroSys), 2019
Google Scholar Citations:

本文指出目前操作系统对时序保护的支持不足并在seL4中实施了时序保护.

The last mile: An empirical study of timing channels on seL4

David Cock, Qian Ge, Toby Murray, Gernot Heiser
University of New South Wales
Proceedings of the ACM Conference on Computer and Communications Security (CCS), 2014
Google Scholar Citations:

本文主要贡献是在seL4上测试具有代表性的时序信道攻击, 同时在seL4中实施一些防治手段并测试性能. 最终得出即使在seL4中, 彻底防御时序信道攻击仍困难.

M3: A hardware/operating-system co-design to tame heterogeneous manycores

Nils Asmussen, Marcus Volp, Benedikt Nothenm, Hermann Hartig, Gerhard Fettweis
Technische Universität Dresden, Germany
Proceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2016
Google Scholar Citations:

本文提出一种微内核操作系统M3, 旨在适应当今计算机系统中核心数量急剧增加和异构性增长的趋势. 通过引入网络芯片层级的隔离和数据传输单元(DTU)的概念, M3将通用核心和加速器视为一等公民, 实现了对异构多核心的统一控制和协同. 此外, 采用核心中立通信协议. 通过DTU提供操作系统服务, 使这些服务对于任意类型的核心都可访问. 通过在大量可用核心的背景下评估 M3 的性能，本文展示了该操作系统在一些应用水平基准测试中相对于传统的 Linux 操作系统的性能提升超过五倍的可行性. 这些设计原则和性能结果为未来计算机体系结构的发展提供了有益的参考

Code Optimizations Using Formally Verified Properties

Yao Shi, Bernard Blackham, Gernot Heiser
University of New South Wales
Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA), 2013
Google Scholar Citations:

本文指出形式化验证不仅带来强大安全性, 并且还带来不变性, 使程序是完全可控的, 这种性质可以应用到编译器代码优化领域. 在完全经过形式化验证的seL4上进行测试, 最终将seL4的平均运行性能提升28%, 最坏情况执行时间优化25%.

Atlantis: robust, extensible execution environments for web applications

James Mickens, Mohan Dhawan
Microsoft
Proceedings of the ACM symposium on Operating systems principles (SOSP), 2011
Google Scholar Citations:

本文提出一种基于微内核的新型浏览器Atlantis, 保证了安全性和可扩展性. 相较于以往的微内核浏览器, Atlantis的创新之处在于允许每个Web页面定义自己的标记解析器、布局引擎、DOM树和脚本运行环境, 使页面能够定制其执行环境而不影响浏览器接口的稳定性. 这种可扩展性解决了现代Web堆栈复杂、实现困难的问题, 使得开发者能更灵活地构建健壮、安全的Web应用程序. 此外, Atlantis通过利用多个内核提供了比以往微内核浏览器更强的安全性保障, 为用户提供了更可靠的浏览体验.

Foundational Software Solutions for The Modern Vehicle

BlackBerry QNX

QNX在汽车领域取得巨大成功, 已经被部署在超过两亿车辆上. QNX Neutrino RTOS的微内核架构保证强大安全性, 将所有服务运行于用户态, 有效减少网络攻击面. 在复杂系统中, QNX Hypervisor利用最新的ARMv8和x86-64硬件虚拟化扩展, 使汽车制造商能够将不同操作系统(QNX、Linux、Android)和混合关键性功能整合到一个单一的SoC中, 同时保持性能和隔离. QNX兼容POSIX, 让开发人员能够快速上手并且保证软件可移植性.

Foundational Software Solutions for The Medical Devices

BlackBerry QNX

QNX天生适用于对安全性要求极高的医疗设备领域

Foundational Software Solutions for The Robotics and Automation

BlackBerry QNX

QNX系统在机器人技术和自动化领域的应用.

The HACMS project

University of New South Wales

seL4在工业界最突出的应用, 在DARPA资助的HACMS计划中, seL4被用于保护一架自主直升机(Boeing's Unmanned Little Bird (ULB) autonomous helicopter)免受网络攻击.