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 different 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 runtime, and other common features that affect execution time). In this paper, we present a novel verification technique for 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. We formalize our technique in CommCSL, a relational concurrent separation logic with support for commutativity-based reasoning, and prove its soundness in Isabelle/HOL. We implemented CommCSL in HyperViper, an automated verifier based on the Viper verification infrastructure, and demonstrate its ability to verify challenging examples.

翻译：信息流安全性确保程序处理的机密数据不会影响其可观察输出。对于并发程序而言，证明信息流安全性尤其具有挑战性，因为对机密数据的操作可能影响线程的执行时间，从而影响不同线程之间的交错。即使攻击者不观察执行时间，这种内部时间通道也可能影响程序的可观察结果。现有的并发程序信息流安全性验证技术试图证明机密数据不影响线程的相对时序。然而，这些技术往往具有限制性（例如，不允许对机密数据进行分支），并对执行平台做出强假设（忽略缓存、具有数据依赖运行时间的处理器指令以及影响执行时间的其他常见特性）。在本文中，我们提出了一种新颖的并发程序安全信息流验证技术，该技术消除了这些限制，并且不对时序行为做任何假设。其核心思想是证明对共享数据执行的所有变异操作是可交换的，从而使得不同的线程交错不会影响其最终值。关键在于，可交换性仅要求针对共享数据的一个抽象，该抽象包含将泄露给公共输出的信息。与标准可交换性相比，抽象可交换性满足更多操作，这使得我们的技术具有广泛适用性。我们在CommCSL（一种支持基于可交换性推理的关系型并发分离逻辑）中形式化了该技术，并在Isabelle/HOL中证明了其正确性。我们在HyperViper（一个基于Viper验证基础设施的自动化验证器）中实现了CommCSL，并展示了其验证具有挑战性示例的能力。