Provable Time Protection for Eliminating Timing Channels

Abstract

The original proposal listed the following four objectives for the project, to be done for the seL4 microkernel: 1. Develop previously propotyped time protection mechanisms into a security model in the seL4 microkernel that integrates with existing information-flow reasoning about seL4; 2. formalise a high-level abstraction of micro-architectural state, i.e. the hardware resources that make execution speed dependent on execution history, and then formalise the operations that affect this state; 3. formalise absence of temporal interference (and thus timing channels) as spatial or temporal partitioning of such state; 4. building on the above, formally prove that time protection mechanisms recently prototyped in seL4 eliminate timing channels by correctly partitioning microarchitectural state. Over the course of the project we made initial progress on the first three objectives. We note that the project is co-funded by the Australian Research Council (ARC) for the years 201921.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 25, 2022
Accession Number
AD1171310

Entities

People

  • Gernot Heiser

Organizations

  • Commonwealth Scientific and Industrial Research Organisation

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Air Force Research Laboratories
  • Computer Access Control
  • Computer Architecture
  • Computing System Architectures
  • Instruction Set Architecture
  • Instructions
  • Military Research
  • Models
  • Operating Systems
  • Reasoning
  • Scientific Research
  • Security
  • Specifications
  • Workshops

Fields of Study

  • Computer science

Readers

  • Environmental Engineering.
  • Integrated Circuit Design and Technology.
  • Parallel and Distributed Computing.