超越算法证明：面向实现层可验证安全的新范式
密码学与安全
2025-08-05 v1
摘要
虽然传统密码学研究聚焦于算法层面的可验证安全，但许多现实攻击却利用系统实现中的弱点，例如内存管理不当、熵源不足以及不安全的密钥生命周期。现有方法虽针对这些风险进行了处理，但缺乏一种统一且可验证的框架来建模实现层面的安全。本文提出了一种新的范式——实现层可验证安全（Implementation-Level Provable Security），其以结构化可验证的抵御部署期间真实攻击面韧性来定义安全。为证明其可行性，我们提出了SEER（Secure and Efficient Encryption-based Erasure via Ransomware），即一种利用并强化巴布克勒索软件（Babuk ransomware）加密核心的文件销毁系统。SEER集成了密钥擦除、熵验证以及执行一致性检查，以确保受约束、可审计的攻击面。我们的评估显示，SEER在保持实际性能的同时实现了强大的不可恢复性保证。这一工作展示了从抽象理论模型向实际可验证的实现层安全转变的趋势。
引用
@article{arxiv.2508.01144,
title = {Beyond Algorithmic Proofs: Towards Implementation-Level Provable Security},
author = {Jiahui Shang and Luning Zhang and Zhongxiang Zheng},
journal= {arXiv preprint arXiv:2508.01144},
year = {2025}
}