一次规约，多次验证：通过分层抽象验证隔离性保障
Reduce Once, Verify Many: Verifying Isolation Guarantees via Hierarchical Abstractions
浏览论文内容
中文总结 AI 辅助
该研究提出一种在Isabelle/HOL中形式化的系统化方法，支持七种数据库隔离级别验证，利用分层抽象将弱隔离级别的规约证明简化为一次高层抽象的通用规约，大幅减少用户证明工作量。
中文摘要 AI 辅助
我们提出了一种数学上严谨的系统化方法，用于验证数据库隔离性保障，该方法支持七种隔离级别，揭示了隔离级别间的根本二分法：更强的级别可仅通过精化验证，而较弱的级别还需额外的规约；同时提供了抽象模型的分层结构，通过剥离最繁琐的部分大幅简化证明。特别地，我们通过在分层结构的高层抽象中执行一次完成的规约，消除了较弱隔离级别下每个协议单独规约证明的需求。为实现这一点，我们开发并应用了通用的规约理论，该理论也具有更广泛的应用价值。总体而言，我们的方法将用户的证明工作量降至对分层结构中最具体模型的一次更简单的精化。所有结果均在Isabelle/HOL中形式化。
英文摘要
We present a mathematically rigorous, systematic approach for the verification of database isolation guarantees, which (i) supports a spectrum of seven isolation levels, (ii) uncovers a fundamental dichotomy among isolation levels: stronger levels can be verified via refinement alone, whereas weaker levels additionally require reduction, and (iii) provides a hierarchy of abstract models that substantially simplifies proofs by factoring out their most labor-intensive parts. In particular, we eliminate the need for per-protocol reduction proofs for the weaker class of isolation levels by performing a once-and-for-all reduction at a high level of abstraction in our hierarchy. To achieve this, we develop and apply a generic theory of reduction, which is also of more general interest. Overall, our approach minimizes the user's proof effort to a single, simpler refinement of the most concrete model in our hierarchy. All our results are formalized in Isabelle/HOL.
