Conflict-free replicated data types (CRDTs) and the local-first concept are increasingly employed not only in small-scale collaboration systems among few users who trust each other, but also in large-scale systems, like Matrix for instant messaging and Keyhive for collaborative documents. Since mutual trust is no longer warranted, these systems require Byzantine fault tolerance and fine-grained access control. As of today, Matrix and Keyhive pair an informal specification with an unverified reference implementation. In this work, we follow a bottom-up approach towards constructing formally verified authorization algorithms for Byzantine fault-tolerant local-first systems. As intermediate target for formal verification, we contribute semantics and invariants of a replicated data type for managing simplified collaboration groups, based on capabilities for access control and hash chronicles for replication. To enable future integration into local-first systems like Matrix and Keyhive, we strive for accessibility to system engineers by using the Rust programming language for formal specification, verification, and implementation, enabled by the Verus framework using the Z3 theorem prover at zero runtime cost. We report on our experience and preliminary results following this approach, and discuss next steps towards scaling up access control expressiveness. Whether this approach can be scaled up to the complexity of real-world local-first access control systems like Matrix or Keyhive remains future work, but our findings demonstrate the potential of system-oriented formal verification with Verus.

翻译：冲突自由复制数据类型（CRDTs）和本地优先概念不仅越来越多地应用于少数互信用户间的小规模协作系统，还被用于大规模系统，例如即时通讯领域的Matrix和协作文档领域的Keyhive。由于互信不再有保障，这些系统需要拜占庭容错和细粒度访问控制。目前，Matrix和Keyhive均采用非形式化规范与未经验证的参考实现相结合的方式。本研究遵循自底向上的方法，为拜占庭容错本地优先系统构建形式化验证的授权算法。作为形式化验证的中间目标，我们贡献了管理简化协作组的复制数据类型的语义与不变量，该数据类型基于能力进行访问控制，并利用哈希链实现复制。为便于未来集成至Matrix和Keyhive等本地优先系统，我们力求面向系统工程师的可达性：使用Rust编程语言进行形式化规范、验证与实现，并借助Verus框架（基于Z3定理证明器）实现零运行时开销。我们报告了采用此方法的经验与初步结果，并讨论了提升访问控制表达力的下一步工作。该方案能否扩展到Matrix或Keyhive等真实世界本地优先访问控制系统的复杂度仍有待未来研究，但我们的发现证明了采用Verus进行系统导向形式化验证的潜力。