通过模态逻辑视角看安全属性
密码学与安全
2023-09-19 v1 计算机科学中的逻辑
多智能体系统
摘要
我们引入一种使用模态逻辑对计算机系统安全性进行推理的框架。该框架具有充分的表现力以刻画多种已知安全属性，同时直观且独立于语法细节与实施机制。我们展示如何使用我们的形式体系来表示保密性、完整性、鲁棒去分类和透明认可的各种进展敏感与终止敏感（不）变体，并证明其与标准定义的等价性。我们方法的直观性和与语义现实的贴近使我们能够明确这些定义的数个隐藏假设，识别其中潜在的问题与微妙之处，同时也为表述更清晰版本及未来扩展至全新属性提供了可能。
引用
@article{arxiv.2309.09542,
title = {Security Properties through the Lens of Modal Logic},
author = {Matvey Soloviev and Musard Balliu and Roberto Guanciale},
journal= {arXiv preprint arXiv:2309.09542},
year = {2023}
}
备注
19 pages, including references and appendix. Extended version of paper accepted to CSF 2024