Pith. sign in

REVIEW 4 major objections 5 minor 33 references

MicroTEE: Designing TEE OS Based on the Microkernel Architecture

T0 review · 4 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read MicroTEE demonstrates that running TEE services as isolated microkernel applications keeps a single service vulnerability from bringing down the whole trusted OS.

desk verdict MicroTEE is a credible microkernel-based TEE prototype whose headline isolation claim is plausible but not demonstrated by the evidence in the paper. read the letter →

arxiv 1908.07159 v1 pith:HYFHOPEQ submitted 2019-08-20 cs.CR cs.OS

Dongxu Ji , Qianying Zhang , Shijun Zhao , Zhiping Shi , Yong Guan This is my paper · ORCID
classification cs.CRcs.OS
keywords TrustZoneTrustedExecutionEnvironmentmicrokernelseL4worldswitchcryptoservicekeymanagementTEEOS
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper argues that a Trusted Execution Environment (TEE) OS does not have to be a large monolithic kernel to be useful: by building the TEE on a microkernel, the services that handle encryption and platform keys can run as separate, isolated user-layer applications. The intended payoff is that an attacker who breaks into any one TEE service, such as the crypto service, is stopped there and cannot read the key-management service or take over the kernel itself. The paper designs MicroTEE around this idea, implements a prototype on an ARM TrustZone board, and measures crypto, IPC, and world-switch performance. It reports that for small data sizes, AES and SHA-256 in MicroTEE outperform the same operations in Linux because the microkernel's context switch is lighter.

What carries the argument

The load-bearing mechanism is the microkernel's per-application address-space isolation, inherited from a formally verified microkernel. In MicroTEE, the microkernel exposes only core services — address-space management, thread control blocks (TCBs), and IPC endpoints — and everything security-related is moved out of the kernel: the Crypto Service, Key Management, and all trusted applications are user-layer processes with separate address spaces. The Root Task, the first user application, owns unused memory and creates and manages TAs and their IPC links. A monitor, entered through the new MicroTEE SMC() syscall that executes the ARM Secure Monitor Call, performs the world switch by saving the current world's context, toggling the NS bit, and restoring the other world's context; parameters travel in registers r0 and r1. This combination turns "isolate the TEE's services" from a slogan into an implemented system and is what carries the claim that one vulnerable service cannot compromise the whole TEE OS.

What would settle it

On the MicroTEE prototype, inject a controlled overflow into the Crypto Service and attempt to read the Key Management service's memory or the kernel's; if the overflow reaches outside its own address space, the claim that one vulnerable service cannot compromise the whole TEE OS is false.

Watch

Extended reading notes

Core claim

MicroTEE's central claim is that the microkernel architecture removes the monolithic TEE's weakest property: in a TEE built on a monolithic kernel, one vulnerable driver or service compromises the entire secure OS, whereas in MicroTEE, the kernel supplies only address-space management, thread management, and IPC, and the crypto service and platform key management become ordinary user-layer applications. The kernel isolates each application's address space, so a fault or exploit in one service does not extend to the others or to the kernel. To bridge the trusted and normal worlds the design adds a monitor that saves and restores CPU context on world switches, plus a new system call, MicroTEE SMC(), through which user-layer apps enter privileged mode and issue the Secure Monitor Call. A Root Task created at boot owns all unused resources and manages the creation of trusted applications, dispatching commands from the normal world to the right TA and back. The prototype on the i.MX6Q board implements the world switch, a secure boot chain from the Boot ROM, and the three crypto services (AES, RSA, SHA-256), and its measurements show IPC latencies under one microsecond for short messages and better small-data crypto throughput than Linux.

Load-bearing premise

The claim holds only if the formally verified microkernel together with the newly added monitor and Secure Monitor Call (SMC) system call are free of exploitable flaws, since only the original kernel's verification is inherited and only the secure world is studied.

Editorial extensions

If this is right

  • A compromise of Crypto Service, Key Management, or one trusted application stays inside that application's address space; the kernel and every other service continue to run.
  • The TEE kernel's attack surface is reduced to core mechanisms — address spaces, threads, IPC, and interrupt delivery — because drivers and services run outside the kernel.
  • Short control messages (0 or 10 words) cross the IPC path in under a microsecond, so for the small messages TEEs typically exchange the isolation overhead is modest.
  • For small data sizes, AES and SHA-256 complete faster in MicroTEE than in Linux because the microkernel context switch is lighter; for large inputs, computation time dominates and the two systems converge.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The authors leave it implicit that the monitor and the new MicroTEE SMC() system call sit outside the formally verified kernel, so the no-whole-TEE-compromise guarantee actually rests on unverified new code; the paper only studies the secure world.
  • For the same reason, the monitor is a natural single point of failure in any stronger security claim: a fault there during context save/restore or interrupt routing could let an attacker cross from the normal world into the secure world.
  • A test the paper does not report is deliberate fault injection: plant a vulnerability in Crypto Service and check whether a malicious TA can reach Key Management's memory or the kernel's; the architecture predicts it cannot, and running that test would directly exercise the paper's main claim.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. MicroTEE proposes a TrustZone-based TEE OS built on the seL4 microkernel. The paper argues that by implementing TEE services (crypto, key management) and trusted applications as isolated user-layer applications on top of a small, formally verified microkernel, a vulnerability in one kernel service will not compromise the whole TEE OS, unlike monolithic TEEs such as QSEE and TrustedCore. The design adds a monitor for secure/normal world switching and a new SMC system call, together with a secure boot chain. The authors implemented a prototype on the Freescale i.MX6Q Sabre Lite board, measured IPC latency and world-switch overhead, and compared AES and SHA-256 throughput with Linux, reporting better small-data performance in MicroTEE. The central claimed contribution is architectural isolation plus an initial prototype evaluation.

Significance. If the isolation claim were established, the microkernel-based TEE architecture would be a meaningful step toward reducing the attack surface of TEE OSes, and the paper would gain additional value from being backed by a concrete prototype and by reusing seL4's formal verification results. The reported measurements are useful preliminary data, and the secure boot chain is a sensible design component. However, the security significance is not currently demonstrated: the monitor and the added SMC system call lie outside the verified seL4 core, no security analysis of those components is provided, and the evaluation explicitly covers only the secure world. The paper is therefore best read as a promising systems report whose headline security benefit requires either substantially more evidence or carefully narrowed claims.

major comments (4)
  1. [IV.B and V.A] The central isolation claim depends on seL4's verified isolation, but the paper adds a new system call, MicroTEE SMC(), and a monitor that runs in monitor mode and handles world switching. Section V.B says the MicroTEE kernel is 'based on' seL4, not identical to it, and the paper does not state whether MicroTEE SMC() is implemented inside the seL4 kernel source or as a user-level trampoline. In either case, the monitor itself is outside the seL4 correctness proof, and a bug in its context save/restore or SMC dispatch can corrupt secure-world state or allow a malicious normal-world caller to violate the assumed isolation boundary. The paper therefore does not establish the abstract claim that a vulnerability in one service cannot compromise the whole TEE OS; it needs either a security argument covering the added monitor and SMC path or a restriction of the claim to the verified kernel alone.
  2. [V.A] Section V.A explicitly states that only the secure-world context is studied and saved/restored in the monitor. This means the normal-world side of the world switch, including the path by which normal-world applications invoke MicroTEE SMC and receive results, is not implemented or demonstrated. Since the motivating threat model is attack from the normal world, the absence of normal-world handling leaves the most security-critical part of the prototype unevaluated and unsupported.
  3. [VI.C and Figures 6-8] The performance comparison with Linux lacks essential baseline details: the Linux kernel version, the cryptographic library or implementation used (e.g., OpenSSL), the timing method, whether the comparison runs on the same i.MX6Q board and CPU frequency, and the compiler/optimization settings are not reported. The text attributes the small-data difference to context-switch overhead, but no direct measurement of Linux context-switch cost is provided. As reported, the claim that MicroTEE is 'better than Linux' for small data sizes is not reproducible or fully supported.
  4. [IV.B and V.A] The monitor passes command ID and args via r0/r1 and shared-memory addresses, but the paper does not describe any validation of these parameters. There is no statement of how the monitor checks that shared-memory addresses and lengths refer to valid secure-world memory, or how it prevents a malicious normal world from causing monitor-mode memory corruption through the SMC interface. Because the monitor is the only boundary between worlds, this missing parameter-validation detail is load-bearing for the security claim.
minor comments (5)
  1. [III.B] The paper states that seL4 is 'proven to be bug-free'; the actual result is a functional correctness proof of the kernel implementation against a formal specification, not a proof of absence of all possible security-relevant bugs. This wording should be qualified.
  2. [VI.A] Each IPC measurement is reported as an average of only 16 calls, with no variance or confidence interval; a larger sample and error bars would make the comparison more convincing.
  3. [References] Reference [8] contains the typo 'Attcaking', and reference [19] omits the first initial of the last author; the reference list should be checked for consistency.
  4. [Figures 1, 2, and 4] Several figure labels are very small or cramped, particularly in the boot-process diagram (Figure 4), and the figures should be redrawn at higher resolution for readability.
  5. [Table II] The caption '1024&2048 BITS -RSA' is awkwardly formatted; it should be rewritten as 'RSA signing and verification times for 1024-bit and 2048-bit keys'.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: MicroTEE's isolation claim rests on microkernel/seL4 isolation and direct prototype measurements, not on fitted inputs or self-referential reasoning.

full rationale

The paper's central claim—that isolating TEE services as user-layer applications prevents a single vulnerable service from compromising the whole TEE OS—is an architectural argument relying on the microkernel isolation mechanism inherited from seL4 and on prototype implementation, not on a derivation that reuses its own conclusion. seL4's formal verification (refs 30–33) is external, independently published support, and the paper does not claim to have re-derived it. The newly added MicroTEE SMC() system call and monitor are explicitly described as additions, and Section V.A states 'Since only the secure world is studied in this paper, the context of the secure world is saved and restored in the monitor'; this is a stated limitation that affects whether the full TrustZone switch is verified, but it is a correctness/completeness risk, not a circular step. Performance results are direct measurements (IPC latency, SMC call overhead, AES/RSA/SHA-256 throughput) compared with Linux benchmarks; no parameter is fitted to a subset and then predicted. Self-citations [25] and [26] appear only in the related-work survey of physical-attack defenses and are not load-bearing for the isolation claim. No equation or construction reduces the output to the input, so there is no significant circularity.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No fitted parameters or new physical entities appear in the paper. The central burden is a set of trust assumptions about inheritance of seL4 verification, the correctness of the monitor, the trustworthiness of the Root Task, and the availability of keys in secure storage. These are software trust boundaries, not mathematical free parameters.

assumptions (5)
  • domain assumption seL4 is fully formally verified and its guarantees remain valid in MicroTEE despite the added SMC system call and monitor.
    Section V.B says MicroTEE kernel is 'based on the seL4 microkernel'; Section IV.B introduces a new system call MicroTEE SMC(), which is not part of the verified seL4 kernel, so the bug-free guarantee cannot be inherited without reverification.
  • domain assumption The monitor correctly saves and restores contexts and cannot be leveraged by the normal world to bypass isolation.
    Section IV.B and V.A assign world switching to the monitor, but no integrity or security analysis of the monitor is given, and Section V.A states only the secure world context is studied.
  • domain assumption The Root Task is trusted and not attacker-controlled, and its capability configuration correctly governs TA and service IPC permissions.
    Section IV.D describes Root Task as manager with highest priority at the user layer, but no proof or analysis shows a malicious TA cannot escalate through the Root Task.
  • domain assumption Platform Root Key and Device Key are available in secure storage and the software Key Management service prevents their exfiltration.
    Section IV.E says keys are 'assuming that they are provided by the vendor and already stored in trusted hardware', while Section V.B says keys are managed in a user-layer Key Management service, leaving the trust boundary ambiguous.
  • domain assumption ARM TrustZone hardware isolation and the described secure boot chain behave as specified on the i.MX6Q.
    Sections III.A and IV.G rely on Boot ROM verification of signed bootloaders; on i.MX6Q this depends on HAB configuration, which the paper does not describe. Section V.C says the microkernel 'has to' perform an integrity check of the Root Task, not that it does.

how reviews work

0 comments
Cite this review

Pith. "Pith review of MicroTEE: Designing TEE OS Based on the Microkernel Architecture." pith.science (2026). https://pith.science/paper/HYFHOPEQ

@misc{pith2026190807159,
  author       = {Pith},
  title        = {Pith review of: MicroTEE: Designing TEE OS Based on the Microkernel Architecture},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HYFHOPEQ}},
  note         = {Machine review of arXiv:1908.07159}
}
read the original abstract

ARM TrustZone technology is widely used to provide Trusted Execution Environments (TEE) for mobile devices. However, most TEE OSes are implemented as monolithic kernels. In such designs, device drivers, kernel services and kernel modules all run in the kernel, which results in large size of the kernel. It is difficult to guarantee that all components of the kernel have no security vulnerabilities in the monolithic kernel architecture, such as the integer overflow vulnerability in Qualcomm QSEE TrustZone and the TZDriver vulnerability in HUAWEI Hisilicon TEE architecture. This paper presents MicroTEE, a TEE OS based on the microkernel architecture. In MicroTEE, the microkernel provides strong isolation for TEE OS's basic services, such as crypto service and platform key management service. The kernel is only responsible for providing core services such as address space management, thread management, and inter-process communication. Other fundamental services, such as crypto service and platform key management service are implemented as applications at the user layer. Crypto Services and Key Management are used to provide Trusted Applications (TAs) with sensitive information encryption, data signing, and platform attestation functions. Our design avoids the compromise of the whole TEE OS if only one kernel service is vulnerable. A monitor has also been added to perform the switch between the secure world and the normal world. Finally, we implemented a MicroTEE prototype on the Freescale i.MX6Q Sabre Lite development board and tested its performance. Evaluation results show that the performance of cryptographic operations in MicroTEE is better than it in Linux when the size of data is small.

Figures

Figures reproduced from arXiv: 1908.07159 by the authors.

Figure 1
Figure 1. The ARM TrustZone Architecture Because TrustZone cannot resist physical attacks, studies have provided ways to improve it. The design in [25] leverages SRAM to provide a root of trust for TrustZone. It provides security against both physical and software attacks. SoftME [26], CaSE [27], TrustShadow [28], and CryptMe [29] provide TEE system with approaches to resist physical attacks. B. SEL4 Microkernel The seL4 [30]… view at source ↗
Figure 2
Figure 2. The Architecture of MicroTEE corresponding handler, SMC handler, is invoked according to the monitor vector table base address stored in the Monitor Vector Base Address Register (MVBAR). The current state of the system, whether secure or normal, is depended on the NS bit in the Secure Configuration Register (SCR), and SMC handler stores the current world’s context on the stack. The monitor modifies the NS bit to the… view at source ↗
Figure 4
Figure 4. Secure Boot Process V. PROTOTYPE IMPLEMENTATION We have implemented a MicroTEE prototype on the Freescale i.MX6Q Sabre Lite development board. This section describes the implementation of all the components, including the Monitor, the MicroTEE kernel based on the seL4 micro￾kernel and the security services. A. The Monitor The monitor is responsible for the switch between the normal world and the secure world. It is … view at source ↗
Figures from the paper (4 more)
Figure 3
Figure 3. Figure 3: The Process of Root Task Calling TA G. Secure Boot At boot time, attackers can perform downgrade attacks, which replace secure software images in flash with tampered images. If the system boots an image from flash without checking its integrity, the system is vulnerabl…
Figure 5
Figure 5. Figure 5: Time of IPC B. Overhead of World Switch The time cost of world switch is also measured. Mea￾surement begins with a TA executing an SMC system call, MicroTEE SMC(command ID, args), and ends with the TA continuing to execute. The world switch involves switching into the …
Figure 6
Figure 6. Figure 6: Performance of AES Encryption and Decryption in MicroTEE [PITH_FULL_IMAGE:figures/full_fig_p007_6.png]
Figure 7
Figure 7. Figure 7: Performance of AES Encryption and Decryption in Linux [PITH_FULL_IMAGE:figures/full_fig_p007_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages

  1. [1]

    Security technology building a secure system using trustzone technology (white paper),

    ARM, “Security technology building a secure system using trustzone technology (white paper),” ARM Limited , 2009

    work page 2009

  2. [2]

    Trustzone explained: Architectural features and use cases,

    B. Ngabonziza, D. Martin, A. Bailey, H. Cho, and S. Martin, “Trustzone explained: Architectural features and use cases,” in 2016 IEEE 2nd International Conference on Collaboration and Internet Computing (CIC). IEEE, 2016, pp. 445–451

    work page 2016

  3. [3]

    T2droid: A trustzone-based dynamic analyser for android applications,

    S. D. Yalew, G. Q. Maguire, S. Haridi, and M. Correia, “T2droid: A trustzone-based dynamic analyser for android applications,” in 2017 IEEE Trustcom/BigDataSE/ICESS. IEEE, 2017, pp. 240–247

    work page 2017

  4. [4]

    Secure block device–secure, flexible, and efficient data storage for arm trustzone systems,

    D. Hein, J. Winter, and A. Fitzek, “Secure block device–secure, flexible, and efficient data storage for arm trustzone systems,” in 2015 IEEE Trustcom/BigDataSE/ISPA, vol. 1. IEEE, 2015, pp. 222–229

    work page 2015

  5. [5]

    Trusttokenf: A generic security framework for mobile two-factor authentication using trustzone,

    Y . Zhang, S. Zhao, Y . Qin, B. Yang, and D. Feng, “Trusttokenf: A generic security framework for mobile two-factor authentication using trustzone,” in 2015 IEEE Trustcom/BigDataSE/ISPA , vol. 1. IEEE, 2015, pp. 41–48

    work page 2015

  6. [6]

    Protc: Protecting drone’s peripherals through arm trustzone,

    R. Liu and M. Srivastava, “Protc: Protecting drone’s peripherals through arm trustzone,” in Proceedings of the 3rd Workshop on Micro Aerial V ehicle Networks, Systems, and Applications . ACM, 2017, pp. 1–6

    work page 2017

  7. [7]

    Qsee trustzone kernel integer over flow vulnerability,

    D. Rosenberg, “Qsee trustzone kernel integer over flow vulnerability,” in Black Hat conference , 2014, p. 26

    work page 2014

  8. [8]

    Attcaking your

    D. Shen, “Attcaking your ”trusted core” exploiting trustzone on android,” in Black Hat conference , 2015

    work page 2015

Show all 33 references
  1. [9]

    Nova: a microhypervisor-based secure vir- tualization architecture,

    U. Steinberg and B. Kauer, “Nova: a microhypervisor-based secure vir- tualization architecture,” in Proceedings of the 5th European conference on Computer systems . ACM, 2010, pp. 209–222

    2010

  2. [10]

    Fiasco.oc,

    TU-Dresden, “Fiasco.oc,” https://os.inf.tu-dresden.de/fiasco/

  3. [11]

    Developers, “Redox,” https://www.redox-os.org/

    R. Developers, “Redox,” https://www.redox-os.org/

  4. [12]

    On-board cre- dentials with open provisioning,

    K. Kostiainen, J.-E. Ekberg, N. Asokan, and A. Rantala, “On-board cre- dentials with open provisioning,” in Proceedings of the 4th International Symposium on Information, Computer , and Communications Security . ACM, 2009, pp. 104–115

    2009

  5. [13]

    On-board credentials: an open credential platform for mobile devices,

    K. Kostiainen et al., “On-board credentials: an open credential platform for mobile devices,” 2012

    2012

  6. [14]

    Towards user-friendly credential transfer on open credential platforms,

    K. Kostiainen, N. Asokan, and A. Afanasyeva, “Towards user-friendly credential transfer on open credential platforms,” in International con- ference on Applied cryptography and network security . Springer, 2011, pp. 395–412

    2011

  7. [15]

    Key attestation from trusted execution environments,

    K. Kostiainen, A. Dmitrienko, J.-E. Ekberg, A.-R. Sadeghi, and N. Asokan, “Key attestation from trusted execution environments,” inIn- ternational Conference on Trust and Trustworthy Computing . Springer, 2010, pp. 30–46

    2010

  8. [16]

    Practical property-based attestation on mobile devices,

    K. Kostiainen, N. Asokan, and J.-E. Ekberg, “Practical property-based attestation on mobile devices,” in International Conference on Trust and Trustworthy Computing. Springer, 2011, pp. 78–92

    2011

  9. [17]

    Trustonic, “Kinibi,” https://www.trustonic.com/

  10. [18]

    TurstKernel, “T6,” https://www.trustkernel.com/

  11. [19]

    Using arm trustzone to build a trusted language runtime for mobile applications,

    N. Santos, H. Raj, S. Saroiu, and A. Wolman, “Using arm trustzone to build a trusted language runtime for mobile applications,” in ACM SIGARCH Computer Architecture News , vol. 42, no. 1. ACM, 2014, pp. 67–80

    2014

  12. [20]

    Trusted language runtime (tlr): enabling trusted applications on smartphones,

    N. Santos, H. Raj, S. Saroiu, and Wolman, “Trusted language runtime (tlr): enabling trusted applications on smartphones,” in Proceedings of the 12th Workshop on Mobile Computing Systems and Applications . ACM, 2011, pp. 21–26

    2011

  13. [21]

    Op-tee documentation,

    Linaro, “Op-tee documentation,” 2019

    2019

  14. [22]

    The andix research osłarm trustzone meets industrial control systems security,

    A. Fitzek, F. Achleitner, J. Winter, and D. Hein, “The andix research osłarm trustzone meets industrial control systems security,” in 2015 IEEE 13th International Conference on Industrial Informatics (INDIN) . IEEE, 2015, pp. 88–93

    2015

  15. [23]

    Open-tee– an open virtual trusted execution environment,

    B. McGillion, T. Dettenborn, T. Nyman, and N. Asokan, “Open-tee– an open virtual trusted execution environment,” in 2015 IEEE Trust- com/BigDataSE/ISPA, vol. 1. IEEE, 2015, pp. 400–407

    2015

  16. [24]

    Tee internal core api specification,

    GlobalPlatform, “Tee internal core api specification,” 2018

    2018

  17. [25]

    Providing root of trust for arm trustzone using on-chip sram,

    S. Zhao, Q. Zhang, G. Hu, Y . Qin, and D. Feng, “Providing root of trust for arm trustzone using on-chip sram,” in Proceedings of the 4th International Workshop on Trustworthy Embedded Devices . ACM, 2014, pp. 25–36

    2014

  18. [26]

    Softme: A software- based memory protection approach for tee system to resist physical attacks,

    M. Zhang, Q. Zhang, S. Zhao, Z. Shi, and Y . Guan, “Softme: A software- based memory protection approach for tee system to resist physical attacks,” Security and Communication Networks , 2019

    2019

  19. [27]

    Case: Cache-assisted secure execution on arm processors,

    N. Zhang, K. Sun, W. Lou, and Y . T. Hou, “Case: Cache-assisted secure execution on arm processors,” in 2016 IEEE Symposium on Security and Privacy (SP) . IEEE, 2016, pp. 72–90

    2016

  20. [28]

    Trustshadow: Secure execution of unmodified applications with arm trustzone,

    L. Guan, P. Liu, X. Xing, X. Ge, S. Zhang, M. Yu, and T. Jaeger, “Trustshadow: Secure execution of unmodified applications with arm trustzone,” in Proceedings of the 15th Annual International Conference on Mobile Systems, Applications, and Services . ACM, 2017, pp. 488– 501

    2017

  21. [29]

    Cryptme: Data leakage prevention for unmodified programs on arm devices,

    C. Cao, L. Guan, N. Zhang, N. Gao, J. Lin, B. Luo, P. Liu, J. Xiang, and W. Lou, “Cryptme: Data leakage prevention for unmodified programs on arm devices,” in International Symposium on Research in Attacks, Intrusions, and Defenses . Springer, 2018, pp. 380–400

    2018

  22. [30]

    From l3 to sel4 what have we learnt in 20 years of l4 microkernels?

    K. Elphinstone and G. Heiser, “From l3 to sel4 what have we learnt in 20 years of l4 microkernels?” in Proceedings of the Twenty-F ourth ACM Symposium on Operating Systems Principles . ACM, 2013, pp. 133–150

    2013

  23. [31]

    sel4 reference manual,

    P. Derrin, D. Elkaduwe, and K. Elphinstone, “sel4 reference manual,” NICTA-National Information and Communications Technology Aus- tralia, 2006

    2006

  24. [32]

    sel4: Formal verification of an os kernel,

    G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish et al. , “sel4: Formal verification of an os kernel,” in Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles . ACM, 2009, pp. 207–220

    2009

  25. [33]

    Timing analysis of a protected operating system kernel,

    B. Blackham, Y . Shi, S. Chattopadhyay, A. Roychoudhury, and G. Heiser, “Timing analysis of a protected operating system kernel,” in 2011 IEEE 32nd Real-Time Systems Symposium . IEEE, 2011, pp. 339–348

    2011

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.