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.
CITATION STYLE
Guanciale, R., Baumann, C., Buiras, P., Dam, M., & Nemati, H. (2022). A Case Study in Information Flow Refinement for Low Level Systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13360 LNCS, pp. 54–79). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-08166-8_4
Mendeley helps you to discover research relevant for your work.