循环进程网络中的信息流控制
Information Flow Control in Cyclic Process Networks
AI总结：
本文提出一种结合会话类型的信息流控制类型系统，支持循环进程网络，利用循环结构实现更宽松的安全控制，并将死锁视为侧信道，证明了良类型程序的死锁敏感非干扰性。
摘要：
保护机密数据是当今应用程序中一项重要的安全考量。尤其值得关注的是，需要防止无意中向（恶意的）观察者泄露信息，该观察者可能与程序交互并从所做出的观察中推断信息。信息流控制（IFC）类型系统通过静态地排除此类泄露来应对这一问题。本文为消息传递并发程序贡献了一个IFC类型系统，这是当今许多应用程序（如云计算和物联网应用）所选择的计算模型。此类应用程序通常隐式或显式地编码了消息交换必须遵循的协议，为了静态地确保协议安全，可以使用诸如会话类型之类的行为类型系统。本文将IFC与会话类型相结合，并在以下方面超越了先前的工作：（1）支持现实的循环进程网络，而不是局限于树形网络；（2）利用循环进程网络，实现更宽松但完全安全的IFC控制；（3）将死锁视为另一种形式的侧信道，并为良类型程序断言死锁敏感的非干扰性（DSNI）。为了证明DSNI，本文发展了一种新颖的逻辑关系，该逻辑关系考虑了循环进程网络。该逻辑关系植根于线性逻辑，但放弃了先前工作所施加的树形拓扑限制。
英文摘要：
Protection of confidential data is an important security consideration of today's applications. Of particular concern is to guard against unintentional leakage to a (malicious) observer, who may interact with the program and draw inference from made observations. Information flow control (IFC) type systems address this concern by statically ruling out such leakage. This paper contributes an IFC type system for message-passing concurrent programs, the computational model of choice for many of today's applications such as cloud computing and IoT applications. Such applications typically either implicitly or explicitly codify protocols according to which message exchange must happen, and to statically ensure protocol safety, behavioral type systems such as session types can be used. This paper marries IFC with session typing and contributes over prior work in the following regards: (1) support of realistic cyclic process networks as opposed to the restriction to tree-shaped networks, (2) more permissive, yet entirely secure, IFC control, exploiting cyclic process networks, and (3) considering deadlocks as another form of side channel, and asserting deadlock-sensitive noninterference (DSNI) for well-typed programs. To prove DSNI, the paper develops a novel logical relation that accounts for cyclic process networks. The logical relation is rooted in linear logic, but drops the tree-topology restriction imposed by prior work.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
