Nonmalleable Progress Leakage
Ethan Cecchetti
信息流控制系统通常强制对进度不敏感的互不干涉,因为它易于理解和执行。 不幸的是,真正的程序需要解密结果并认可输入,这些输入是不干涉的,同时防止攻击者控制泄漏,包括通过进度渠道,而进度不敏感会忽略这些渠道。 这项工作将对进度敏感的安全与安全降级(解密和背书)相结合,以确定安全降级进度信息的概念。 我们使用超属性来提炼进度敏感和进度不敏感互不干涉之间的分离,并将其与非可销售信息流(安全降级的现有(进展不敏感)定义)相结合,以定义不可销售的进展泄漏(NMPL)。 我们介绍了第一个信息流类型系统,以便在执行 NMPL 时允许一些进度泄漏,我们展示了如何推断安全进度降级的位置。 所有定理都在Rocq中验证。
Information-flow control systems often enforce progress-insensitive noninterference, as it is simple to understand and enforce. Unfortunately, real programs need to declassify results and endorse inputs, which noninterference disallows, while preventing attackers from controlling leakage, including through progress channels, which progress-insensitivity ignores. This work combines ideas for progress-sensitive security with secure downgrading (declassification and endorsement) to identify a notio...