在 Isabelle/UTP 中检验与自动化机密性理论
密码学与安全
2023-10-18 v1
摘要
近期在现代 CPU 上发现的漏洞（例如 Spectre [1]）的严重性，凸显了信息泄露对计算机系统安全可能造成的破坏性影响。同时，这表明机密性应被提升为程序验证的常规组成部分，以便在开发早期发现和缓解此类漏洞。我们提出的理论主要基于 Bank 的理论 [2]——一个在统一编程理论（Unifying Theories of Programming, UTP）[3] 中形式化的机密性属性推理框架。我们在 Isabelle 定理证明器当前实现的 UTP（即 Isabelle/UTP [4]）中机械化了我们的编码。我们发现了 Bank 原始框架中的一些理论问题。最后，我们展示了如何利用我们的机械化形式化验证 Bank 著作中的部分示例。
引用
@article{arxiv.2310.10658,
title = {Checking and Automating Confidentiality Theory in Isabelle/UTP},
author = {Lex Bailey and Jim Woodcock and Simon Foster and Roberto Metere},
journal= {arXiv preprint arXiv:2310.10658},
year = {2023}
}