論文の概要: Towards System-Oriented Formal Verification of Local-First Access Control
- arxiv url: http://arxiv.org/abs/2604.23560v1
- Date: Sun, 26 Apr 2026 06:56:51 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-28 17:12:07.432063
- Title: Towards System-Oriented Formal Verification of Local-First Access Control
- Title（参考訳）: ローカルファーストアクセス制御のシステム指向形式検証に向けて
- Authors: Florian Jacob, Johanna Stuber, Hannes Hartenstein,
- Abstract要約: 競合のない複製データ型(CRDT)は、インスタントメッセージングのMatrixやコラボレーションドキュメントのKeyhiveといったコラボレーションシステムにますます採用されています。
相互信頼はもはや保証されないため、これらのシステムはビザンチンの耐障害性ときめ細かいアクセス制御を必要とする。
我々は、ビザンチンのフォールトトレラントなローカルファーストシステムに対して、正式に認証された認証アルゴリズムを構築するためのボトムアップアプローチに従う。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: 競合のない複製データ型(CRDT)とローカルファーストの概念は、互いに信頼する少数のユーザの間で、小規模のコラボレーションシステムだけでなく、インスタントメッセージングのMatrixやコラボレーションドキュメントのKeyhiveといった大規模システムにも採用されている。
相互信頼はもはや保証されないため、これらのシステムはビザンチンの耐障害性ときめ細かいアクセス制御を必要とする。
今日、Matrix と Keyhive は、未検証の参照実装と非公式な仕様をペアリングしている。
本研究では,東ローマ帝国のフォールトトレラントなローカルファーストシステムに対して,正式に認証された認証アルゴリズムを構築するためのボトムアップアプローチに従う。
形式検証の中間ターゲットとして,複製データ型のセマンティクスと不変性をコントリビュートして,アクセス制御機能と複製のためのハッシュ年代記機能に基づいて,単純化された協調グループを管理する。
MatrixやKeyhiveといったローカルファーストシステムへの将来的な統合を実現するため、私たちは、ランタイムコストゼロでZ3定理証明器を使用してVerusフレームワークが有効にしているRustプログラミング言語を使用して、システムエンジニアへのアクセシビリティの実現に努めています。
本稿では,本手法によるユーザエクスペリエンスと事前結果について報告し,アクセス制御表現性のスケールアップに向けた次のステップについて論じる。
この手法が、MatrixやKeyhiveのような実世界のローカルファーストアクセス制御システムの複雑さにまで拡張できるかどうかは、今後の課題だが、我々の研究結果は、Verusによるシステム指向の形式検証の可能性を示している。
関連論文リスト
- Just Ask: Curious Code Agents Reveal System Prompts in Frontier LLMs [65.6660735371212]
textbftextscJustAskは,インタラクションのみで効果的な抽出戦略を自律的に発見するフレームワークである。
これは、アッパー信頼境界に基づく戦略選択と、原子プローブと高レベルのオーケストレーションにまたがる階層的なスキル空間を用いて、オンライン探索問題として抽出を定式化する。
この結果から,現代のエージェントシステムにおいて,システムプロンプトは致命的ではあるがほぼ無防備な攻撃面であることがわかった。
論文 参考訳（メタデータ） (2026-01-29T03:53:25Z) - Why Does the LLM Stop Computing: An Empirical Study of User-Reported Failures in Open-Source LLMs [50.075587392477935]
オープンソースのDeepSeek、Llama、Qwenのエコシステムから、705の現実世界の失敗に関する大規模な実証的研究を行った。
ホワイトボックスオーケストレーションは、モデルアルゴリズムの欠陥からデプロイメントスタックのシステム的脆弱性へと、信頼性のボトルネックを移動させます。
論文 参考訳（メタデータ） (2026-01-20T06:42:56Z) - JEEVHITAA -- An End-to-End HCAI System to Support Collective Care [5.456792874544804]
VHITAA(Android/Flutterシステム)は,ケアサークルに対して,コンテキストに敏感でロールアウェアな共有と検証可能な情報フローを提供する。
VHITAAは(Google HealthとBLEコネクタ経由で)プラットフォームとデバイスデータを取り込み、センサーストリームとタイアップから多層ユーザプロファイルを構築し、許可されたケアグラフ全体にわたって詳細な時間境界アクセス制御を実行する。
論文 参考訳（メタデータ） (2025-12-06T09:36:27Z) - Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis [49.31947916567367]
Hamilton-Jacobi (J) リーチビリティ解析は、最悪の不確実性の下で最適なリーチビリティを計算できる一般的な非線形システムに対する一般的な形式的検証ツールである。
この作業は、HJローバーを介してRobust Verification Controllersのための、HJベースのリーチビリティベースのシステム検証フレームワークである。
本稿では,Ro-CoReの安全性検証とコントローラ設計のための新しい手法を提案する。
論文 参考訳（メタデータ） (2025-11-18T18:55:20Z) - The Gatekeeper Knows Enough [0.0]
Gatekeeper Protocolは、エージェント・システム間のインタラクションを管理するドメインに依存しないフレームワークである。
提案手法は,エージェントの信頼性を著しく向上し,トークン消費を最小化することで計算効率を向上し,複雑なシステムとのスケーラブルな相互作用を可能にする。
論文 参考訳（メタデータ） (2025-10-16T17:00:42Z) - CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。
私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
論文 参考訳（メタデータ） (2024-11-20T14:16:55Z) - Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。
問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。
本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
論文 参考訳（メタデータ） (2024-03-15T17:32:02Z) - Practical quantum secure direct communication with squeezed states [37.69303106863453]
CV-QSDCシステムの最初の実験実験を行い,その安全性について報告する。
この実現は、将来的な脅威のない量子大都市圏ネットワークへの道を歩み、既存の高度な波長分割多重化(WDM)システムと互換性がある。
論文 参考訳（メタデータ） (2023-06-25T19:23:42Z) - Interactive System-wise Anomaly Detection [66.3766756452743]
異常検出は様々なアプリケーションにおいて基本的な役割を果たす。
既存のメソッドでは、インスタンスがデータとして容易に観察できないシステムであるシナリオを扱うのが難しい。
システム埋め込みを学習するエンコーダデコーダモジュールを含むエンドツーエンドアプローチを開発する。
論文 参考訳（メタデータ） (2023-04-21T02:20:24Z) - Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。
これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
論文 参考訳（メタデータ） (2022-08-23T05:02:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。