A Case Study in Information Flow Refinement for Low Level Systems

Guanciale, Roberto and Baumann, Christoph and Buiras, Pablo and Dam, Mads and Nemati, Hamed
(2022) A Case Study in Information Flow Refinement for Low Level Systems.
In: The Logic of Software. A Tasting Menu of Formal Methods. Springer International Publishing, pp. 54-79. ISBN 978-3-031-08166-8

[img]
Preview
 Text
InfoFlowRefinementcasestudy.pdf
Download (473kB) | Preview
Official URL: https://doi.org/10.1007/978-3-031-08166-8_4

Abstract

In this work we employ information-flow-aware refinement to study security properties of a separation kernel. We focus on refinements that support changes in data representation and semantics, including the addition of state variables that may induce new observational power or side channels. We leverage an epistemic approach to ignorance-preserving refinement where an abstract model is used as a specification of a system's permitted information flows that may include the declassification of secret information. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model. In particular, we show that a simple key manager may cause information leakage via a refinement that includes cache and timing information. Finally, we show that deploying standard countermeasures against cache-based timing channels regains ignorance preservation.

Item Type: Book Section
Depositing User: Hamed Nemati
Date Deposited: 23 Sep 2022 09:50
Last Modified: 23 Sep 2022 09:50
Primary Research Area: NRA2: Reliable Security Guarantees
URI: https://publications.cispa.saarland/id/eprint/3785

Actions

Actions (login required)

View Item View Item
CISPA is powered by EPrints 3 which is developed by the School of Electronics and Computer Science at the University of Southampton. More information and software credits.