Till innehåll på sidan

Information Flow Refinement

Docent lecture by Roberto Guanciale, division of Theoretical Computer Science

Tid: To 2022-03-10 kl 10.00

Plats: E2

Språk: English

Föreläsare: Roberto Guanciale

Confidentiality is a key property of secure computer systems. It is also a fraught one: sophisticated attacks continue to

emerge that use different microarchitectural features to extract secret data. For example, the recent Spectre attacks have demonstrated the fundamental insecurity of current computer microarchitecture, where features like pipelining, out-of-order and speculation can be used to extract arbitrary information about the memory contents of a process.

For realistic architectures and software a monolithic analysis of confidentiality is not feasible, since such an analysis has to take into account the wealth of features of modern computer systems such as caches, multiple cores, pipelines, buses, GPUs, devices, and so on. To cope with systems at this level of complexity, a modular approach based on some form of refinement is essential, since it would allow to handle different security threats at different abstraction levels and then to compose the analysis results to provide security at system level.

In this lecture we present ignorance-preserving refinement. This is a new epistemic approach 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 refined model can add state variables that may induce new observational power or side channels. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model. We will investigate properties of ignorance-preserving refinement, in particular sequential composability, and introduce an unwinding condition that is designed to support software verification. We finally apply the theory to three relevant examples: a simple secure multiparty protocol, the oblivious RAM construction of Chung and Pass, and a separation kernel.

feasible, since such an analysis has to take into account the wealth of features of modern computer systems such as caches, multiple cores, pipelines, buses, GPUs, devices, and so on. To cope with systems at this level of complexity, a modular approach based on some form of refinement is essential, since it would allow to handle different security threats at different abstraction levels and then to compose the analysis results to provide security at system level.

In this lecture we present ignorance-preserving refinement. This is a new epistemic approach 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 refined model can add state variables that may induce new observational power or side channels. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model. We will investigate properties of ignorance-preserving refinement, in particular sequential composability, and introduce an unwinding condition that is designed to support software verification. We finally apply the theory to three relevant examples: a simple secure multiparty protocol, the oblivious RAM construction of Chung and Pass, and a separation kernel.