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

• URL: http://arxiv.org/abs/2604.23560v1
• Date: Sun, 26 Apr 2026 06:56:51 GMT
• Title: Towards System-Oriented Formal Verification of Local-First Access Control
• Abstract summary: Conflict-free replicated data types (CRDTs) are increasingly employed in collaboration systems like Matrix for instant messaging and Keyhive for collaborative documents.<n>Since mutual trust is no longer warranted, these systems require Byzantine fault tolerance and fine-grained access control.<n>We follow a bottom-up approach towards constructing formally verified authorization algorithms for Byzantine fault-tolerant local-first systems.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• DKVE: Decentralized Key Validation for End-to-End Encrypted Messaging [0.7978226788634308]
  End-to-end encrypted messaging systems depend on authentic public key distribution to prevent man-in-the-middle (MitM) attacks.<n>Current solutions present a stark trade-off: out-of-band (OOB) verification provides strong security but lacks scalability for large contact lists.<n>We propose DKVE, a protocol that validates public keys through privacy-preserving cross-validation within users' social graphs.
  arXiv  Detail & Related papers  (2026-06-25T00:43:59Z)
• Dance Across Shifts: Forward-Facilitation Continual Test-Time Adaptation through Dynamic Style Bridging [65.11234199720428]
  Continual Test-Time Adaptation aims to empower perception systems to handle dynamic distribution shifts encountered after deployment.<n>We introduce a novel forward-facilitation paradigm through a method termed Dynamic Style Bridging.<n>During test time, to mitigate inherent generative bias and adapt these proxies to incoming data, we propose a multi-level bridging mechanism.
  arXiv  Detail & Related papers  (2026-05-18T16:18:17Z)
• From CRUD to Autonomous Agents: Formal Validation and Zero-Trust Security for Semantic Gateways in AI-Native Enterprise Systems [0.0]
  This paper proposes the design, formal validation, and empirical evaluation of a Semantic Gateway governed by the Model Context Protocol (MCP)<n>The gateway reframes the enterprise API as a semantic surface where tools are dynamically discovered, authorized, and executed based on intent and policy enforcement.<n>The architecture introduces a three-layer Zero-Trust security model comprising a pre-inference Semantic Firewall, deterministic Tool-Level RBAC, and out-of-band Cryptographic Human-in-the-Loop approval.
  arXiv  Detail & Related papers  (2026-04-28T12:25:06Z)
• Just Ask: Curious Code Agents Reveal System Prompts in Frontier LLMs [65.6660735371212]
  We present textbftextscJustAsk, a framework that autonomously discovers effective extraction strategies through interaction alone.<n>It formulates extraction as an online exploration problem, using Upper Confidence Bound--based strategy selection and a hierarchical skill space spanning atomic probes and high-level orchestration.<n>Our results expose system prompts as a critical yet largely unprotected attack surface in modern agent systems.
  arXiv  Detail & Related papers  (2026-01-29T03:53:25Z)
• Why Does the LLM Stop Computing: An Empirical Study of User-Reported Failures in Open-Source LLMs [50.075587392477935]
  We conduct the first large-scale empirical study of 705 real-world failures from the open-source DeepSeek, Llama, and Qwen ecosystems.<n>Our analysis reveals a paradigm shift: white-box orchestration relocates the reliability bottleneck from model algorithmic defects to the systemic fragility of the deployment stack.
  arXiv  Detail & Related papers  (2026-01-20T06:42:56Z)
• AI-NativeBench: An Open-Source White-Box Agentic Benchmark Suite for AI-Native Systems [52.65695508605237]
  We introduce AI-NativeBench, the first application-centric and white-box AI-Native benchmark suite grounded in Model Context Protocol (MCP) and Agent-to-Agent (A2A) standards.<n>By treating agentic spans as first-class citizens within distributed traces, our methodology enables granular analysis of engineering characteristics beyond simple capabilities.<n>This work provides the first systematic evidence to guide the transition from measuring model capability to engineering reliable AI-Native systems.
  arXiv  Detail & Related papers  (2026-01-14T11:32:07Z)
• JEEVHITAA -- An End-to-End HCAI System to Support Collective Care [5.456792874544804]
  We presentVHITAA, an Android/Flutter system that provides context-sensitive, role-aware sharing and verifiable information flows for care circles.<n>VHITAA ingests platform and device data (via Google Health and BLE connectors), constructs multi-layer user profiles from sensor streams and tiered, and enforces fine-grained, time-bounded access control across permissioned care graphs.
  arXiv  Detail & Related papers  (2025-12-06T09:36:27Z)
• Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis [49.31947916567367]
  Hamilton-Jacobi (J) reachability analysis is a popular formal verification tool for general nonlinear systems that can compute optimal reachable under worst-case uncertainties.<n>This work is the first HJ-based reachability-based system verification framework for the Robust Verification Controllers via HJ rover.<n>Within Ro-CoRe, we propose novel methods for safety verification and controller design.
  arXiv  Detail & Related papers  (2025-11-18T18:55:20Z)
• The Gatekeeper Knows Enough [0.0]
  Gatekeeper Protocol is a domain-agnostic framework that governs agent-system interactions.<n>Our results show that this approach significantly increases agent reliability, improves computational efficiency by minimizing token consumption, and enables scalable interaction with complex systems.
  arXiv  Detail & Related papers  (2025-10-16T17:00:42Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Practical quantum secure direct communication with squeezed states [37.69303106863453]
  We report the first table-top experimental demonstration of a CV-QSDC system and assess its security.<n>This realization paves the way into future threat-less quantum metropolitan networks, compatible with coexisting advanced wavelength division multiplexing (WDM) systems.
  arXiv  Detail & Related papers  (2023-06-25T19:23:42Z)
• Interactive System-wise Anomaly Detection [66.3766756452743]
  Anomaly detection plays a fundamental role in various applications. It is challenging for existing methods to handle the scenarios where the instances are systems whose characteristics are not readily observed as data. We develop an end-to-end approach which includes an encoder-decoder module that learns system embeddings.
  arXiv  Detail & Related papers  (2023-04-21T02:20:24Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.