IIIf 中的安全工程，第二部分——细化与互不干涉
软件工程
2024-12-17 v1 计算机科学中的逻辑
摘要
在本文中，我们通过解决细化信息流安全（IFC）这一长期存在的难题，为 Isabelle 内部与基础设施框架（IIIf）[31,16]的安全工程过程增加了第二部分。我们探讨了互不干涉的经典概念，该概念代表了不存在向较低层级信息流的绝对安全意义。众所周知，这一概念通常无法在规范细化中保持，这种现象被称为“细化悖论”[33]。我们采用 Morgan [33] 针对顺序程序规范的细化演算给出的解决方案，并将其推广到 IIIf 中包含参与者、去中心化和策略的基础设施的一般规范中。作为说明该问题、概念及解决方案的贯穿示例，我们使用了一个 Flightradar 系统规范示例 [20]。
关键词
引用
@article{arxiv.2412.10949,
title = {Security Engineering in IIIf, Part II -- Refinement and Noninterference},
author = {Florian Kammüller},
journal= {arXiv preprint arXiv:2412.10949},
year = {2024}
}
备注
This is a substantially extended version of a previously published paper [20]