非可塌进度泄漏
密码学与安全
2025-07-29 v1 编程语言
摘要
信息流控制系统通常执行进度不敏感的非干扰，以便于理解和执行。不幸的是，实际程序需要对结果进行匿名化处理并对输入进行背书，而这会导致非干扰不允许，而且还要防止攻击者通过进度通道控制泄漏，这一进度不敏感性被忽略。本工作将进度敏感安全与安全降级（匿名化和背书）的想法结合起来，确定一种安全降级进度信息的概念。我们使用超属性来提炼进度敏感与进度不敏感非干扰之间的差异，并将其与非可塌进度信息流相结合，以定义非可塌进度泄漏（NMPL）。我们提出了首个允许某些进度泄漏但执行 NMPL 的信息流类型系统，并展示了如何推断安全进度降级的位置。所有定理均在 Rocq 中得到验证。
引用
@article{arxiv.2505.12210,
title = {Nonmalleable Progress Leakage},
author = {Ethan Cecchetti},
journal= {arXiv preprint arXiv:2505.12210},
year = {2025}
}