Towards System-Oriented Formal Verification of Local-First Access Control

TL;DR

This paper presents a formal verification approach for access control in Byzantine fault-tolerant local-first systems, using Rust and the Verus framework to improve system reliability.

Contribution

It introduces semantics and invariants for a replicated data type to support verified access control algorithms in local-first systems, with a focus on system-oriented formal methods.

Findings

Developed a formal specification and verification of a replicated data type for access control.

Demonstrated the use of Rust and Verus for accessible formal verification.

Reported preliminary results showing potential for scaling to real-world systems.

Abstract

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.