論文の概要: Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems

• arxiv url: http://arxiv.org/abs/2309.09141v1
• Date: Sun, 17 Sep 2023 02:57:05 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-23 07:29:15.741908
• Title: Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems
• Title（参考訳）: コンカレントシステムにおける情報フローセキュリティのイベントベース構成推論
• Authors: Yongwang Zhao, David Sanan, Fuyuan Zhang, Yang Liu
• Abstract要約: 並列システムのための情報フローセキュリティ(IFS)のための,信頼度に基づく構成推論手法を提案する。 Event''を並列言語に組み込むことで、まず言語を設計し、その言語のIFSセマンティクスを提供します。 IFSの構成的推論には、イベント上の新しい種類の巻き戻し条件(UC)を定義するために、Depended-guarantee仕様を用いる。
• 参考スコア（独自算出の注目度）: 5.965840906609809
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: High assurance of information-flow security (IFS) for concurrent systems is challenging. A promising way for formal verification of concurrent systems is the rely-guarantee method. However, existing compositional reasoning approaches for IFS concentrate on language-based IFS. It is often not applicable for system-level security, such as multicore operating system kernels, in which secrecy of actions should also be considered. On the other hand, existing studies on the rely-guarantee method are basically built on concurrent programming languages, by which semantics of concurrent systems cannot be completely captured in a straightforward way. In order to formally verify state-action based IFS for concurrent systems, we propose a rely-guarantee-based compositional reasoning approach for IFS in this paper. We first design a language by incorporating ``Event'' into concurrent languages and give the IFS semantics of the language. As a primitive element, events offer an extremely neat framework for modeling system and are not necessarily atomic in our language. For compositional reasoning of IFS, we use rely-guarantee specification to define new forms of unwinding conditions (UCs) on events, i.e., event UCs. By a rely-guarantee proof system of the language and the soundness of event UCs, we have that event UCs imply IFS of concurrent systems. In such a way, we relax the atomicity constraint of actions in traditional UCs and provide a compositional reasoning way for IFS in which security proof of systems can be discharged by independent security proof on individual events. Finally, we mechanize the approach in Isabelle/HOL and develop a formal specification and its IFS proof for multicore separation kernels as a study case according to an industrial standard -- ARINC 653.
• Abstract（参考訳）: 並列システムにおける情報フローセキュリティ(IFS)の高保証は困難である。 並列システムの形式的検証に有望な方法は rely-guarantee メソッドである。 しかし、IFSの既存の構成推論アプローチは、言語ベースのIFSに集中している。 マルチコアオペレーティングシステムカーネルのようなシステムレベルのセキュリティには適用されないことが多く、アクションの秘密性も考慮すべきである。 一方、confluent-guaranteeメソッドに関する既存の研究は、基本的に並列プログラミング言語の上に構築されており、並列システムのセマンティクスを単純な方法で完全に捉えることはできない。 本稿では,コンカレントシステムに対する状態行動に基づくIFSの形式的検証を行うため,IFSに対する信頼保証に基づくコンポジション推論手法を提案する。 最初に '`Event'' を並行言語に組み込んで言語を設計し、その言語のIFSセマンティクスを提供する。 プリミティブ要素として、イベントはモデリングシステムの非常に優れたフレームワークを提供しており、私たちの言語では必ずしもアトミックではない。 IFS の構成的推論には、イベント UC 上の新しい形態の巻き戻し条件 (UC) を定義するために、Depended-guarantee 仕様を用いる。 言語に依存した証明システムとイベントUCの健全性により、イベントUCは並列システムのIFSを暗示する。 このような方法で、従来のUCにおける行動の原子性制約を緩和し、個別の事象に対する独立したセキュリティ証明によってシステムのセキュリティ証明を退避できるIFSの構成的推論方法を提供する。 最後に,Isabelle/HOL のアプローチを機械化し,産業標準 ARINC 653 による研究事例として,Isabelle/HOL の正式な仕様と IFS によるマルチコア分離カーネルの証明を開発する。

関連論文リスト

• WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+ [0.358439716487063]
  我々は,コンピュータサイエンスプログラムにおける形式的手法の状態を質的に評価することを目的としている。 卒前研究の中間に含めることができるレベル適合例を構築した。
  論文  参考訳（メタデータ） (2024-07-30T19:31:14Z)
• Beyond Mask: Rethinking Guidance Types in Few-shot Segmentation [67.35274834837064]
  我々は、テキスト、マスク、ボックス、画像からのプロンプトを統合するユニバーサルビジョン言語フレームワーク(UniFSS)を開発した。 UniFSSは最先端の手法よりも優れています。
  論文  参考訳（メタデータ） (2024-07-16T08:41:01Z)
• SCIF: A Language for Compositional Smart Contract Security [3.2707122129201975]
  SCIFは、構成的にセキュアなスマートコントラクトを構築するための言語です。 SCIFは、セキュアな情報フローの基本的な構成原理に基づいている。 相互作用するプリンシパルと部分信頼の豊富なエコシステムをサポートする。
  論文  参考訳（メタデータ） (2024-07-01T11:51:21Z)
• Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications [0.0]
  この記事では、CRSの正式な仕様と検証のための依存型推論フレームワークであるPiCoreを提案する。 我々は、複雑な反応構造をサポートするイベント仕様言語を設計し、イベントの振る舞いからCRSのリアクティブな側面の仕様とロジックを分離する。 この設計により、仕様や証明の変更なしに既存の2つの言語とそれらの信頼保証証明システムを統合することに成功した。
  論文  参考訳（メタデータ） (2023-09-17T03:43:25Z)
• (Security) Assertions by Large Language Models [25.270188328436618]
  セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(LLM)を用いることを検討する。 我々は、人気のあるLCMに注目し、プロンプトの様々なレベルの詳細を考慮し、アサーションを箱から書き出す能力を特徴付ける。
  論文  参考訳（メタデータ） (2023-06-24T17:44:36Z)
• Token-level Sequence Labeling for Spoken Language Understanding using Compositional End-to-End Models [94.30953696090758]
  音声合成言語理解システムを構築した。 ASRのために訓練された中間デコーダを頼りにすることで、私たちのエンドツーエンドシステムは、入力モダリティを音声からトークンレベルの表現に変換する。 我々のモデルは、名前付きエンティティ認識のラベル付けタスクにおいて、カスケードモデルと直接エンド・ツー・エンドモデルの両方より優れている。
  論文  参考訳（メタデータ） (2022-10-27T19:33:18Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。 次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。 これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
  論文  参考訳（メタデータ） (2022-08-23T05:02:09Z)
• Generalized Few-shot Semantic Segmentation [68.69434831359669]
  本稿では,GFS-Seg(Generalized Few-Shot Semantic)と呼ばれる新しいベンチマークを導入する。 GFS-セグにおいて、先行する最先端の一般化が不足していることを示す最初の研究である。 本研究では,1)支援サンプルから共起前の知識を活用すること,2)各クエリ画像の内容に基づいて条件付き情報に動的に拡張することにより,性能を著しく向上するコンテキスト認識型プロトタイプ学習(CAPL)を提案する。
  論文  参考訳（メタデータ） (2020-10-11T10:13:21Z)
• PIN: A Novel Parallel Interactive Network for Spoken Language Understanding [68.53121591998483]
  既存の RNN ベースのアプローチでは、ID と SF のタスクは、それらの間の相関情報を利用するために、しばしば共同でモデル化される。 SNIPSとATISという2つのベンチマークデータセットによる実験は、我々のアプローチの有効性を実証している。 さらに,事前学習した言語モデルBERTが生成した発話の特徴埋め込みを用いて,提案手法はすべての比較手法の中で最先端の手法を実現する。
  論文  参考訳（メタデータ） (2020-09-28T15:59:31Z)
• Interventional Few-Shot Learning [88.31112565383457]
  本稿では,新しいFew-Shot Learningパラダイム,Interventional Few-Shot Learningを提案する。 コードはhttps://github.com/yue-zhongqi/ifsl.comで公開されている。
  論文  参考訳（メタデータ） (2020-09-28T01:16:54Z)
• Quantifying Assurance in Learning-enabled Systems [3.0938904602244355]
  機械学習コンポーネントを組み込んだシステムの依存性保証は、安全クリティカルなアプリケーションで使用する上で重要なステップである。 本稿では, LESが信頼できるという保証の定量的概念を, 保証ケースのコアコンポーネントとして開発する。 本稿では,現実の自律型航空システムへの適用による保証対策の有用性について述べる。
  論文  参考訳（メタデータ） (2020-06-18T08:11:50Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。