論文の概要: Griotte: Verified Compartmentalisation via Capabilities
- arxiv url: http://arxiv.org/abs/2609.01110v1
- Date: Tue, 01 Sep 2026 11:50:45 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-02 16:31:36.611495
- Title: Griotte: Verified Compartmentalisation via Capabilities
- Title（参考訳）: Griotte: 能力による比較の検証
- Authors: June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal,
- Abstract要約: CHERIoTは、ハードウェア機能を活用してコンパートメントの概念を定義する、新しいハードウェアとソフトウェアの共同設計である。
デフォルトでは、コンパートメントは、バグや悪意のある振る舞いに対するダメージを制限するために分離される。
スイッチタはCHERIoTコンパートメントモデルのセキュリティ保証を強制するために重要である。
- 参考スコア（独自算出の注目度）: 0.9641309631461574
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: CHERIoT is a novel hardware-software co-design that leverages hardware capabilities to define a notion of compartment, in a minimalistic capability-based OS, CHERIoT RTOS. By default, compartments are isolated to limit damage in case of bugs or malicious behaviour. To allow cross-compartment communication, the OS provides a privileged component, called the switcher. The switcher provides an interface for cross-compartment calls, while enforcing isolation between compartments and guaranteeing stack safety. Together with hardware capabilities, the switcher is critical to enforce the security guarantees of the CHERIoT compartment model. The design of CHERIoT raises two questions: First, how can one formalise the informal notion of compartmentalisation that CHERIoT compartments are designed to provide? And second, given that the safety properties of CHERIoT hinge on the complementary roles of the capability machine and of the switcher, does the design of CHERIoT enforce the desired security properties? In this paper, we introduce Griotte and Griotte OS, idealised but faithful versions of the CHERIoT machine and the CHERIoT RTOS, which we use to answer these two questions: First, we formally capture the aforementioned security guarantees in the form of a continuation-based logical relation which captures the combined behaviour of the switcher and of the capability machine. And second, we define a specification for the Griotte switcher that enforces those guarantees, and prove that the implementation meets the specification. We demonstrate Griotte on a range of key scenarios illustrating different aspects of CHERIoT, including integrity of the local state in the presence of memory sharing with unknown code. Our approach is modular: we verify compartments individually, and then compose their specifications. Together, our contributions give a solid formal foundation to the design of CHERIoT.
- Abstract（参考訳）: CHERIoTは、ハードウェア機能を活用して、最小限の機能ベースのOSであるCHERIoT RTOSでコンパートメントの概念を定義する、新しいハードウェアとソフトウェアの共同設計である。
デフォルトでは、コンパートメントは、バグや悪意のある振る舞いに対するダメージを制限するために分離される。
クロスコンパートメント通信を可能にするため、OSはSwitcherと呼ばれる特権コンポーネントを提供する。
スイッチタは、コンパートメント間の分離とスタック安全性の保証を図りながら、クロスコンパートメントコールのためのインターフェースを提供する。
ハードウェア機能とともに、スイッチャーはCHERIoTコンパートメントモデルのセキュリティ保証を強制することが重要である。
CHERIoTの設計は2つの疑問を提起する。 まず、CHERIoTコンパートメントを提供するように設計された、非公式なコンパートナライゼーションの概念を形式化するにはどうすればよいのか?
第二に、機能マシンとスイッチャーの相補的な役割におけるCHERIoTヒンジの安全性特性を考えると、CHERIoTの設計は望ましいセキュリティ特性を強制するのだろうか?
本稿では,CHERIoTマシンとCHERIoT RTOSの理想的だが忠実なバージョンであるGriotteとGriotte OSを紹介する。
次に、これらの保証を強制するGriotteスイッチャーの仕様を定義し、実装が仕様を満たすことを証明します。
我々は、未知のコードによるメモリ共有の存在下でのローカル状態の整合性など、CHERIoTのさまざまな側面を説明できるさまざまな重要なシナリオについて、Griotteを実証する。
私たちのアプローチはモジュール化されており、コンパートメントを個別に検証し、その仕様を作成します。
私たちのコントリビューションは、CHERIoTの設計にしっかりとした公式な基盤を提供します。
関連論文リスト
- Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code [0.5296470528744145]
制御フローやデータフローの制限のような非機能要件は、組み込みシステムの安全性にとって重要である。
Cモジュールのためのインタフェース仕様契約言語を提案する。
Scania trucks におけるソフトウェアを用いた安全クリティカル C コードの2つのケーススタディについて報告する。
論文 参考訳（メタデータ） (2026-05-19T21:12:45Z) - Dive into Claude Code: The Design Space of Today's and Future AI Agent Systems [42.345465506597044]
Claude Codeは、シェルコマンドを実行し、ファイルを編集し、ユーザに代わって外部サービスを呼び出すことができるエージェントコーディングツールである。
本研究では、公開されているTypeScriptソースコードを分析して、その包括的なアーキテクチャについて説明する。
論文 参考訳（メタデータ） (2026-04-14T17:59:37Z) - QoeSiGN: Towards Qualified Collaborative eSignatures [42.13843953705695]
EUのeIDAS規制は、例えば、進歩と資格(QES)のeSignatureを規定している。
QESは、認定信託サービスプロバイダ(QTSP)が発行する資格証明書に基づいています。
オーストリアのeIDのQES生成過程に関する脅威分析を行う。
本稿では,新しいP2C2技術を活用したQoeSiGNを提案する。
論文 参考訳（メタデータ） (2025-12-15T18:07:17Z) - AlignSAE: Concept-Aligned Sparse Autoencoders [47.18866175760984]
本稿では,SAE の機能と定義オントロジーを"pre-train, then-train" カリキュラムで整合させる手法である AlignSAE を紹介する。
初期教師なしトレーニングフェーズの後、特定の概念を専用潜在スロットにバインドするために教師付きポストトレーニングを適用する。
この分離により、非関係な特徴から干渉することなく、特定の関係を検査・制御できる解釈可能なインターフェースが生成される。
論文 参考訳（メタデータ） (2025-12-01T18:58:22Z) - PICO: Secure Transformers via Robust Prompt Isolation and Cybersecurity Oversight [0.0]
本稿では,迅速なインジェクション攻撃を防止するために,ロバストなトランスフォーマーアーキテクチャを提案する。
PICOフレームワークは,信頼できないユーザ入力から信頼されたシステム命令を構造的に分離する。
専門のSecurity Expert AgentをMixture-of-Expertsフレームワークに組み込んでいます。
論文 参考訳（メタデータ） (2025-04-26T00:46:13Z) - A Security Framework for General Blockchain Layer 2 Protocols [11.284365017329861]
本稿では、Layer 2 (L2)プロトコルの最初の一般的なセキュリティフレームワークを示す。
我々のフレームワークはIITMベースのUniversal Composability(iUC)フレームワークをベースにしています。
我々は,3つの主要なL2スケーリングパラダイム – 支払いチャネル(Brick),サイドチェーン(Liquid Network),ロールアップ(Arbitrum) – のそれぞれから,その例を分析した。
論文 参考訳（メタデータ） (2025-04-21T08:48:24Z) - Collaborative Inference over Wireless Channels with Feature Differential Privacy [57.68286389879283]
複数の無線エッジデバイス間の協調推論は、人工知能(AI)アプリケーションを大幅に強化する可能性がある。
抽出された特徴を抽出することは、プロセス中に機密性の高い個人情報が暴露されるため、重大なプライバシーリスクをもたらす。
本稿では,ネットワーク内の各エッジデバイスが抽出された機能のプライバシを保護し,それらを中央サーバに送信して推論を行う,新たなプライバシ保存協調推論機構を提案する。
論文 参考訳（メタデータ） (2024-10-25T18:11:02Z) - On Cryptographic Mechanisms for the Selective Disclosure of Verifiable Credentials [39.4080639822574]
認証資格は、物理的資格のデジタルアナログである。
検証者に提示して属性を明らかにしたり、クレデンシャルに含まれる属性を述語することも可能だ。
プレゼンテーション中にプライバシを保存する1つの方法は、クレデンシャル内の属性を選択的に開示することである。
論文 参考訳（メタデータ） (2024-01-16T08:22:28Z) - Rely-guarantee Reasoning about Concurrent Memory Management:
Correctness, Safety and Security [0.0]
メモリ管理の誤った仕様と実装は、システムのクラッシュや悪用可能な攻撃につながる可能性がある。
本稿では,実世界のOSにおける並列メモリ管理の最初の正式な仕様と機構的証明について述べる。
論文 参考訳（メタデータ） (2023-09-17T03:41:10Z) - "Yeah, it does have a...Windows `98 Vibe'': Usability Study of Security
Features in Programmable Logic Controllers [19.08543677650948]
Programmable Logic Controllers (PLC) の設定ミスはしばしばインターネットに公開される。
PLC接続構成と2つのキーセキュリティ機構のユーザビリティについて検討する。
未知のラベルやレイアウト、誤解を招く用語を用いることで、すでに複雑なプロセスが悪化することがわかった。
論文 参考訳（メタデータ） (2022-08-04T07:20:00Z) - Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
本稿では,無線アクセスネットワーク(RAN)アプリケーションの安全管理のためのシンボル強化学習(SRL)アーキテクチャを提案する。
我々は、ユーザが所定のセルネットワークトポロジに対して高レベルの論理的安全性仕様を指定できる純粋に自動化された手順を提供する。
ユーザがシステムに意図仕様を設定するのを支援するために開発されたユーザインターフェース(UI)を導入し、提案するエージェントの動作の違いを検査する。
論文 参考訳（メタデータ） (2021-06-03T16:45:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。