High assurance of information-flow security (IFS) for concurrent systems is challenging. A promising way for formal verification of concurrent systems is the rely-guarantee method. However, existing compositional reasoning approaches for IFS concentrate on language-based IFS. It is often not applicable for system-level security, such as multicore operating system kernels, in which secrecy of actions should also be considered. On the other hand, existing studies on the rely-guarantee method are basically built on concurrent programming languages, by which semantics of concurrent systems cannot be completely captured in a straightforward way. In order to formally verify state-action based IFS for concurrent systems, we propose a rely-guarantee-based compositional reasoning approach for IFS in this paper. We first design a language by incorporating ``Event'' into concurrent languages and give the IFS semantics of the language. As a primitive element, events offer an extremely neat framework for modeling system and are not necessarily atomic in our language. For compositional reasoning of IFS, we use rely-guarantee specification to define new forms of unwinding conditions (UCs) on events, i.e., event UCs. By a rely-guarantee proof system of the language and the soundness of event UCs, we have that event UCs imply IFS of concurrent systems. In such a way, we relax the atomicity constraint of actions in traditional UCs and provide a compositional reasoning way for IFS in which security proof of systems can be discharged by independent security proof on individual events. Finally, we mechanize the approach in Isabelle/HOL and develop a formal specification and its IFS proof for multicore separation kernels as a study case according to an industrial standard -- ARINC 653.

翻译：并发系统信息流安全的高保证性极具挑战性。对于并发系统的形式化验证，依赖-保证方法是一种有前景的途径。然而，现有针对信息流安全的组合推理方法主要关注基于语言的信息流安全，通常不适用于系统级安全（如多核操作系统内核），因为此类场景还需考虑动作的保密性。另一方面，现有依赖-保证方法研究基本建立在并发编程语言之上，难以直接完整刻画并发系统的语义。为形式化验证并发系统中基于状态-动作的信息流安全，本文提出一种基于依赖-保证的信息流安全组合推理方法。首先，我们通过将“事件”融入并发语言设计了一种新语言，并给出其信息流安全语义。在语言中，事件作为基本元素为系统建模提供了极为简洁的框架，且不必具有原子性。针对信息流安全的组合推理，我们利用依赖-保证规约定义了事件上新型的解缠绕条件（即事件解缠绕条件）。通过该语言的依赖-保证证明系统及事件解缠绕条件的合理性，我们证明事件解缠绕条件可推导出并发系统的信息流安全性。由此，我们放宽了传统解缠绕条件中动作的原子性约束，并提供了一种信息流安全组合推理方式，其中系统的安全证明可通过单个事件上的独立安全证明来完成。最后，我们在Isabelle/HOL中实现了该方法，并根据工业标准ARINC 653，以多核分离内核为案例开发了其形式规约及信息流安全证明。