First steps in verifying the seL4 Core Platform Paturel, Mathieu; Subasinghe, Isitha; Heiser, Gernot
Proceedings of the 14th ACM SIGOPS Asia-Pacific Workshop on Systems,
08/2023
Conference Proceeding
Odprti dostop
We report on our initial effort to formally verify the seL4 Core Platform, an OS framework for the verified seL4 microkernel. This includes a formal specification of the seL4 Core Platform library, ...an automated proof of its functional correctness, and a verified mapping of the seL4 Core Platform's System Description to the CapDL formalism that describes seL4 access rights and enables verified system initialisation.
Hardware-supported virtualization on ARM Varanasi, Prashant; Heiser, Gernot
Proceedings of the Second Asia-Pacific Workshop on Systems,
07/2011
Conference Proceeding
ARM is the dominant processor architecture for mobile devices and many other high-end embedded systems. Late last year ARM announced architectural support for virtualization, which will allow ...execution of unmodified guest operating system binaries. We have designed and implemented what we believe is the first hypervisor supporting pure virtualization using those hardware extensions and evaluated it on simulated hardware. We describe our approach and report our initial experience with the architecture.
The Jury Is In Biggs, Simon; Lee, Damon; Heiser, Gernot
Proceedings of the 9th Asia-Pacific Workshop on Systems,
08/2018
Conference Proceeding
The security benefits of keeping a system's trusted computing base (TCB) small has long been accepted as a truism, as has the use of internal protection boundaries for limiting the damage caused by ...exploits. Applied to the operating system, this argues for a small microkernel as the core of the TCB, with OS services separated into mutually-protected components (servers) -- in contrast to "monolithic" designs such as Linux, Windows or MacOS. While intuitive, the benefits of the small TCB have not been quantified to date. We address this by a study of critical Linux CVEs, where we examine whether they would be prevented or mitigated by a microkernel-based design. We find that almost all exploits are at least mitigated to less than critical severity, and 40% completely eliminated by an OS design based on a verified microkernel, such as seL4.
Can We Put the "S" Into IoT? Heiser, Gernot; Parker, Lucy; Chubb, Peter ...
2022 IEEE 8th World Forum on Internet of Things (WF-IoT),
2022-Oct.-26
Conference Proceeding
Security of IoT systems is often weak or absent, resulting in systems being compromised. We present the seL4 Core Platform, an operating-system framework that leverages the formally verified security ...enforcement of the seL4 microkernel to enable the construction of secure-by-design IoT systems, and even enables an incremental cyber retrofit of existing systems. The framework is designed to make its formal verification tractable. An initial evaluation shows that for performance-sensitive highthroughput networking, the platform significantly outperforms Linux.
Can We Prove Time Protection? Heiser, Gernot; Klein, Gerwin; Murray, Toby
Proceedings of the Workshop on Hot Topics in Operating Systems,
05/2019
Conference Proceeding
Timing channels are a significant and growing security threat in computer systems, with no established solution. We have recently argued that the OS must provide time protection, in analogy to the ...established memory protection, to protect applications from information leakage through timing channels. Based on a recently-proposed implementation of time protection in the seL4 microkernel, we investigate how such an implementation could be formally proved to prevent timing channels. We postulate that this should be possible by reasoning about a highly abstracted representation of the shared hardware resources that cause timing channels.
Mobile multicores Carroll, Aaron; Heiser, Gernot
Proceedings of the Workshop on Power-Aware Computing and Systems,
11/2013
Conference Proceeding
Energy management is a primary consideration in the design of modern smartphones, made more interesting by the recent proliferation of multi-core processors in this space. We investigate how core ...offlining and DVFS can be used together on these systems to reduce energy consumption. We show that core offlining leads to very modest savings in the best circumstances, with a heavy penalty in others, and show the cause of this to be low per-core idle power. We develop a policy in Linux that exploits this fact, and show that it improves up to 25% on existing implementations.
Covert channels enable information leakage between security domains that should be isolated by observing execution differences in shared hardware. These channels can appear in any stateful shared ...resource, including caches, predictors, and accelerators. Previous works have identified many vulnerable components, demonstrating and defending against attacks via reverse engineering. However, this approach requires much human effort and reasoning. With the Cambrian explosion of specialized hardware, it is becoming increasingly difficult to identify all vulnerabilities manually.
To tackle this challenge, we propose AutoCC, a methodology that leverages formal property verification (FPV) to automatically discover covert channels in hardware that is shared between processes. AutoCC operates at the register-transfer level (RTL) to exhaustively examine any machine state left by a process after a context switch that creates an execution difference. Upon finding such a difference, AutoCC provides a precise execution trace showing how the information was encoded into the machine state and recovered.
Leveraging AutoCC’s flow to generate FPV testbenches that apply our methodology, we evaluated it on four open-source hardware projects, including two RISC-V cores and two accelerators. Without hand-written code or directed tests, AutoCC uncovered known covert channels (within minutes instead of many hours of test-driven emulations) and unknown ones. Although AutoCC is primarily intended to find covert channels, our evaluation has also found RTL bugs, demonstrating that AutoCC is an effective tool to test both the security and reliability of hardware designs.
Covert channels enable information leakage between security domains that should be isolated by observing execution differences in shared hardware. These channels can appear in any stateful shared ...resource, including caches, predictors, and accelerators. Previous works have identified many vulnerable components, demonstrating and defending against attacks via reverse engineering. However, this approach requires much human effort and reasoning. With the Cambrian explosion of specialized hardware, it is becoming increasingly difficult to identify all vulnerabilities manually.To tackle this challenge, we propose AutoCC, a methodology that leverages formal property verification (FPV) to automatically discover covert channels in hardware that is shared between processes. AutoCC operates at the register-transfer level (RTL) to exhaustively examine any machine state left by a process after a context switch that creates an execution difference. Upon finding such a difference, AutoCC provides a precise execution trace showing how the information was encoded into the machine state and recovered.Leveraging AutoCC's flow to generate FPV testbenches that apply our methodology, we evaluated it on four open-source hardware projects, including two RISC-V cores and two accelerators. Without hand-written code or directed tests, AutoCC uncovered known covert channels (within minutes instead of many hours of test-driven emulations) and unknown ones. Although AutoCC is primarily intended to find covert channels, our evaluation has also found RTL bugs, demonstrating that AutoCC is an effective tool to test both the security and reliability of hardware designs.CCS CONCEPTS* Security and privacy → Side-channel analysis and countermeasures; Tamper-proof and tamper-resistant designs; Information flow control; * Hardware → Best practices for EDA.
PDF
