分布式非干扰
密码学与安全
2023-10-02 v2 计算机科学中的逻辑
摘要
信息流安全属性在若干年前（参见例如综述 \cite{FG01,Ry01}）被定义为适当的等价性检验问题。这些定义通过使用顺序计算模型（例如标记转移系统 \cite{GV15}）和交错行为等价（例如互模拟等价 \cite{Mil89}）给出。最近，Petri 网的分布式模型已被用于研究非干扰 \cite{BG03,BG09,BC15}，但在这些论文中也使用了交错语义。我们认为，为了捕获所有相关的信息流，必须使用真并发行为等价。特别地，我们针对 Petri 网提出了基于{\em 分支位置双相似} \cite{Gor23b} 的分布式非干扰属性，称为 DNI，这是一种针对带静默移动的有限 Petri 网的合理且可判定的等价。然后我们将注意力集中在称为 {\em 有限状态机} 的 Petri 网子类上，该子类可以（在同构意义下）由简单进程代数 CFM \cite{Gor17} 表示。DNI 在 CFM 进程上非常容易检验，因为它是组合的，因此不会遭受状态空间爆炸问题。此外，我们展示了 DNI 可以通过类型系统在 CFM 上以语法方式刻画。
引用
@article{arxiv.2301.08570,
title = {Distributed Non-Interference},
author = {Roberto Gorrieri},
journal= {arXiv preprint arXiv:2301.08570},
year = {2023}
}