Noninterference guarantees that an attacker cannot infer secrets by interacting with a program. Information flow control (IFC) type systems assert noninterference by tracking the level of information learned (pc) and disallowing communication to entities of lesser or unrelated level than the pc. Control flow constructs such as loops are at odds with this pattern because they necessitate downgrading the pc upon recursion to be practical. In a concurrent setting, however, downgrading is not generally safe. This paper utilizes session types to track the flow of information and contributes an IFC type system for message-passing concurrent processes that allows downgrading the pc upon recursion. To make downgrading safe, the paper introduces regrading policies. Regrading policies are expressed in terms of integrity labels, which are also key to safe composition of entities with different regrading policies. The paper develops the type system and proves progress-sensitive noninterference for well-typed processes, ruling out timing attacks that exploit the relative order of messages. The type system has been implemented in a type checker, which supports security-polymorphic processes using local security theories.

翻译：非干扰性保证了攻击者无法通过与程序交互来推断秘密信息。信息流控制类型系统通过追踪已获知信息的级别（pc）并禁止向低于或无关于此pc级别的实体进行通信，从而断言非干扰性。诸如循环之类的控制流结构与此模式存在冲突，因为它们在递归时需要降低pc级别才能实际应用。然而，在并发环境中，降级通常并不安全。本文利用会话类型来追踪信息流，并提出了一种适用于消息传递并发进程的IFC类型系统，该系统允许在递归时降低pc级别。为确保降级的安全性，本文引入了降级策略。降级策略通过完整性标签来表达，这些标签也是安全组合具有不同降级策略的实体的关键。本文开发了该类型系统，并为良类型进程证明了进展敏感的非干扰性，从而排除了利用消息相对顺序的时序攻击。该类型系统已在类型检查器中实现，支持使用本地安全理论的安全多态进程。