假设但验证：并发应用中泄露信息的演绎验证（扩展版）
密码学与安全
2023-09-08 v1
摘要
我们考虑对故意泄露信息的非平凡并发程序指定安全性并证明其安全性的问题。我们提出一种方法，将该问题分解为：(a) 证明程序仅泄露其已通过假设注解（在演绎程序验证中已被广泛使用的）解除降级的信息；以及 (b) 依据声明式安全策略审计这些解除降级操作。我们展示了如何通过扩展现有程序逻辑 SecCSL 来强制条件 (a)，以及如何通过证明一组简单的蕴含式来检查 (b)。部分挑战在于定义相应的语义可靠性准则，并将其与逻辑规则及策略审计形式化地联系起来。我们在一个自动主动程序验证器中支持该方法，并应用该验证器针对一系列解除降级策略验证了多个案例研究程序的实现。
引用
@article{arxiv.2309.03442,
title = {Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version)},
author = {Toby Murray and Mukesh Tiwari and Gidon Ernst and David A. Naumann},
journal= {arXiv preprint arXiv:2309.03442},
year = {2023}
}