Funding
Our Partners
Time Protection
aka
Timing Channel Prevention
Aim
Design, implementation, evaluation and verification of black-box OS abstractions and mechanisms for time protection: the prevention of timing channels.
Overview
|
|
Micro-architectural timing channels result from competing access to shared, finite hardware resources. Sharing may be time-multiplexed (intra-core) or concurrent (inter-core). |
Unauthorised information leakage is a violation of a system's security policy (see the background page for further explanation). Enforcing security is a primary responsibility of the operating system (OS); yet no contemporary, general-purpose OS has the means for preventing this violation. Our aim is to change this.
Our formally verified seL4 microkernel provably prevents other security violations, including through covert storage channels. This makes timing channels the last, fundamentally unsolved security problem in operating systems, and seL4 the ideal platform for solving it.
In particular, the OS must provide mandatory enforcement of timing-channel freedom, i.e. security enforcement must not depend on application cooperation. Mandatory enforcement is the only way to ensure that untrusted code operating on secret information does not leak it. Such code is commonplace: legacy software stacks running on untrustworthy mainstream OSes such as Linux, Macos or Windows, smartphone apps, browser plugins and server-provided Javascript routinely process confidential data. Furthermore, the use of gadgets in the Spectre attack has shown that even supposedly trustworthy code can be turned into a Trojan.
Hence we are looking for black-box OS-level mechanisms for providing temporary isolation. For spatial isolation such mechanisms are well-established, the core mechanism is memory protection. Here we are working on providing the corresponding temporal isolation, which we accordingly call time protection.
Approach
Our earlier investigations have shown that complete time protection is not possible on present hardware, hence solving this problem requires a hardware-software co-design approach. In other words: we need a new, security-oriented, hardware-software contract.
Consequently, we are pursuing a number of directions concurrently, with the ultimate aim of verified time protection.
OS mechanisms
We have designed and implemented (in seL4) fundamental time-protection mechanisms. These consist of:
-
A new kernel clone mechanism that provides a policy-free way of setting up a system without any memory shared between security partitions (save a small number of kernel data structures that are accessed carefully to ensure deterministic execution). This eliminates any channels through a shared kernel image.
Kernel cloning provides a way of identifying security-domain switches, thus informing the kernel at which context switches additional scrubbing operations are needed. This is a policy-free way of minimising isolation overheads.
-
Security-partition switches that carefully reset all shared micro-architectural state, while making switch times completely deterministic, and in particular, independent of previous execution history.
-
Mechanisms for partitioning lower-level caches, where flushing cost would be high and would not help if those caches are shared across cores. This employs page colouring, and extends to kernel code and data.
-
Partitioning of interrupt sources, so the system is able to use interrupt-driven I/O, unlike classical separation kernels, which disable all interrupts and rely on high-overhead polled I/O.
We have demonstrated that these mechanisms are effective, to the degree that the hardware provides the right mechanisms for scrubbing or partitioning state. Please see the downloads page for accessing the relevant artefacts.
OS Abstractions
Having developed seL4 mechanisms able to provide time protection, we now are working on suitable abstractions that integrate with the existing seL4 model, in particular the new scheduling-context capabilities that provide a principled treatment of time as a resource, with the aim of supporting mixed-criticality real-time systems.
Our aim is a similarly principled model that combines both types of temporal isolation, temporal integrity for real time, and temporal confidentiality for security.
Hardware-software contract
- We have defined the high-level properties of the HW-SW contract that the OS needs to provide time protection.
-
Our collaborators at ETH Zurich have designed, implemented (on RISC-V) a simple
and easy-to-implement hardware support mechanism in
the form of the
fence.tinstruction. Their evaluation shows that the instruction is an effective and low-overhead mechanism for implementing time protection. - A RISC-V task group is looking at adding this to the RISC-V ISA.
Verifying time protection
We are working on proving that our system provides complete time protection. This will require formally specifying the hardware-software contract (at as abstract a level as possible), including formally defining partitionable vs flushable hardware resources.
Specifically we are working on a operational specification of the required properties, so that time protection can be verified as a functional-correctness property without explicit reasoning about time. This approach will allow us to extend seL4's existing proofs of information flow security to also provide assurance about timing channels.
Our collaborators at PlanV will be
formally verifying the implementation of the fence.t
instruction.
Support
Time protection is financially supported by the German Cyberagentur under the Ecosystem formally verifiable IT – Provable cybersecurity (EvIT) program as part of the PISTIs-V Project.
It was previously supported by grants from the Australian Research Council (ARC) and from US Air Force the Asian Office for Aerospace Research and Development (AOARD).
Collaboration
We are partnered with:
- Munich-based PlanV on
verifying the hardware implementation of
fence.t - The PULP team at
the Integrated Systems Lab
of ETH Zurich on the design of hardware-support mechanisms (such
as
fence.t.
News
- 25-01-20: Cyberagentur announces funding for the PISTIs-V project. Our time protection work, which was on hold since the ARC funding ran out, is being restarted as part of PISTIs-V — stay tuned!
- 22-11: Our paper on our Isabelle/HOL formalisation of time protection has been accepted by FM 2023.
- 21-02: Our joint paper with ETH reporting the prototype implementation and evaluation of hardware support for time protection wins the Best Paper Award at DATE.
- 19-07: Gernot Heiser wins a grant from the AOARD as further support for verifying time protection.
- 19-04: Our paper reporting the implementation and evaluation of time protection wins the Best Paper Award at EuroSys.
- 18-11: Gernot Heiser, Toby Murray and Gerwin Klein won a 3-year (2019–2021) Discovery Grant from the ARC for verifying time protection.
- 18-08: Our paper introducing the concept of time protection wins the Best Paper Award at APSys.
- 18-04: We undertook a comprehensive analysis of microarchitectural timing channels on multiple Intel and ARM processors and the effectiveness of hardware-provided defences.
Contacts
People
Current |
Past |
