Email Gateway (Apr 04 2023 at 12:02): Email Gateway (Apr 04 2023 at 12:02):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I'm happy to announce a new AFP entry.
Enjoy,
René
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving
Information Flow Security in Concurrent Programs
by Thibault Dardinier
Information flow security ensures that the secret data manipulated by a program
does not influence its observable output. Proving information flow security is
especially challenging for concurrent programs, where operations on secret data
may influence the execution time of a thread and, thereby, the interleaving
between threads. Such internal timing channels may affect the observable outcome
of a program even if an attacker does not observe execution times. Existing
verification techniques for information flow security in concurrent programs
attempt to prove that secret data does not influence the relative timing of
threads. However, these techniques are often restrictive (for instance because
they disallow branching on secret data) and make strong assumptions about the
execution platform (ignoring caching, processor instructions with data-dependent
execution time, and other common features that affect execution time).
In this entry, we formalize and prove the soundness of CommCSL, a novel
relational concurrent separation logic for proving secure information flow in
concurrent programs that lifts these restrictions and does not make any
assumptions about timing behavior. The key idea is to prove that all mutating
operations performed on shared data commute, such that different thread
interleavings do not influence its final value. Crucially, commutativity is
required only for an abstraction of the shared data that contains the
information that will be leaked to a public output. Abstract commutativity is
satisfied by many more operations than standard commutativity, which makes our
technique widely applicable.
https://www.isa-afp.org/entries/CommCSL.html
Last updated: Apr 20 2024 at 04:19 UTC