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

Technical Summary: Towards System-Oriented Formal Verification of Local-First Access Control

1. Problem Statement

The paper addresses a critical gap in the development of local-first systems (decentralized, low-latency, and highly available systems like Matrix or Keyhive). While these systems rely on Conflict-Free Replicated Data Types (CRDTs) to manage concurrency, they often lack formal verification for their security protocols.

As these systems scale, they move from small, trusted groups to large-scale environments where participants cannot be mutually trusted. This necessitates Byzantine Fault Tolerance (BFT) and fine-grained access control. Currently, major protocols like Matrix rely on informal specifications and unverified reference implementations, which has historically led to security vulnerabilities (e.g., algorithms violating security invariants). The core challenge is designing authorization algorithms that are:

• Byzantine Fault-Tolerant: Resilient against malicious actors who use omission, equivocation, or backdating.
• Eventually Consistent: Able to reach a common state without central coordination.
• Non-monotonic: Capable of handling revocations, which can change the authorization status of previously "authorized" concurrent events.

2. Methodology

The authors adopt a bottom-up approach to formal verification. Instead of attempting to verify a massive, complex system like Matrix directly, they construct and verify simplified, modular authorization algorithms to establish a foundation for future scaling.

Key methodological components include:

• Formal Specification: They define the mathematical semantics of a replicated data type for collaboration groups using capabilities (for access rights) and hash chronicles (for Byzantine-resilient replication via hash-linked DAGs).
• Security Invariants: They define three critical invariants:
  1. Authorization Safety: Ensures that the authorization of an event remains invariant unless a valid revocation occurs.
  2. Query Safety: Ensures that any change in query results (e.g., group name or permissions) is driven by a discursively authorized event.
  3. Revocation Safety: Ensures that if an event is unauthorized at a certain timestamp, it remains unauthorized for all earlier causal timestamps (preventing "backdating" attacks).
• Toolchain (Verus & Rust): To make verification accessible to system engineers, they use Verus, a verification framework for the Rust programming language. Verus allows for the unification of specification, implementation, and verification in a single source file, using the Z3 theorem prover at zero runtime cost.

3. Key Contributions

• Semantics of a Replicated Authorization Data Type: A formal mathematical model (Spec 1 and Spec 2) for managing group capabilities and metadata in a Byzantine environment.
• Verified Authorization Algorithms: The authors implemented and verified three progressive stages of an algorithm:
  1. Monotonic Granting: Only allows grants before group creation.
  2. Monotonic Evolution: Allows grants after creation but no revocations.
  3. Non-monotonic Revocation: Supports both grants and revocations, introducing the complexity of "discursive authorization" (where concurrent events can affect an event's validity).
• Proof of Totality and Purity: They proved that their query functions are pure (ensuring strong convergence/eventual consistency) and total (ensuring the system does not crash/panic even under Byzantine conditions).

4. Results

The authors successfully demonstrated that the Verus framework can be used to bridge the gap between high-level security specifications and low-level Rust implementations.

• They proved that their simplified algorithms satisfy the defined Authorization, Query, and Revocation Safety invariants.
• They demonstrated that by using a "granted-present-revoke" model (similar to observed-remove sets), they could effectively mitigate Byzantine attacks like backdating and equivocation.
• The verification process confirmed that the implementation correctly handles the non-monotonic nature of revocations, where an event's authorization status might change due to the arrival of concurrent revocation events.

5. Significance

This work is significant because it provides a blueprint for system-oriented formal verification. Rather than treating formal methods as a purely theoretical exercise, the authors show how they can be integrated into the actual development workflow of high-performance systems using Rust.

By proving that security invariants can be maintained in a Byzantine, local-first environment, the paper paves the way for more robust decentralized protocols. It moves the field closer to a future where large-scale, decentralized communication and collaboration tools (like a decentralized Wikipedia or secure messaging) can be mathematically guaranteed to be secure against malicious actors.