論文の概要: Verifying components of Arm(R) Confidential Computing Architecture with ESBMC
- arxiv url: http://arxiv.org/abs/2406.04375v1
- Date: Wed, 5 Jun 2024 09:09:37 GMT
- ステータス: 処理完了
- システム内更新日: 2024-06-10 18:49:00.528516
- Title: Verifying components of Arm(R) Confidential Computing Architecture with ESBMC
- Title（参考訳）: ESBMCによるArm(R) Confidential Computing Architectureのコンポーネント検証
- Authors: Tong Wu, Shale Xiong, Edoardo Manino, Gareth Stockwell, Lucas C. Cordeiro,
- Abstract要約: Realm Management Monitor (RMM) はArm Confidential Computing Architecture (Arm CCA) において重要なファームウェアコンポーネントである
これまでの研究は、RMMの仕様とプロトタイプ参照実装の検証に形式的検証技術を適用していた。
本稿では,SMT(Satifiability Modulo Theories)ベースのソフトウェアモデルチェッカーであるESBMCの適用について述べる。
- 参考スコア（独自算出の注目度）: 6.914213030256384
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Realm Management Monitor (RMM) is an essential firmware component within the recent Arm Confidential Computing Architecture (Arm CCA). Previous work applies formal techniques to verify the specification and prototype reference implementation of RMM. However, relying solely on a single verification tool may lead to the oversight of certain bugs or vulnerabilities. This paper discusses the application of ESBMC, a state-of-the-art Satisfiability Modulo Theories (SMT)-based software model checker, to further enhance RRM verification. We demonstrate ESBMC's ability to precisely parse the source code and identify specification failures within a reasonable time frame. Moreover, we propose potential improvements for ESBMC to enhance its efficiency for industry engineers. This work contributes to exploring the capabilities of formal verification techniques in real-world scenarios and suggests avenues for further improvements to better meet industrial verification needs.
- Abstract（参考訳）: Realm Management Monitor(RMM)は、Arm Confidential Computing Architecture(Arm CCA)において重要なファームウェアコンポーネントである。
これまでの研究は、RMMの仕様とプロトタイプ参照実装の検証に形式的手法を適用していた。
しかし、単一の検証ツールにのみ依存することは、特定のバグや脆弱性の監視につながる可能性がある。
本稿では,SMT(Satifiability Modulo Theories)ベースのソフトウェアモデルチェッカーであるESBMCの適用について述べる。
ESBMCのソースコードを正確に解析し、適切な時間枠内で仕様の失敗を特定する能力を示します。
さらに,産業技術者の効率を高めるため,ESBMCの潜在的な改善を提案する。
この研究は、実世界のシナリオにおける形式的検証技術の能力の探求に寄与し、産業的検証のニーズを満たすためのさらなる改善の道筋を提案する。
関連論文リスト
- Towards commands recommender system in BIM authoring tool using transformers [0.7499722271664147]
本研究では,BIMモデリングプロセスの高速化を目的としたシーケンシャルレコメンデーションシステムの可能性について検討する。
本稿では,BIMソフトウェアコマンドを推奨項目として扱うことにより,ユーザの履歴的インタラクションに基づいて次の最良コマンドを予測する,新たなエンドツーエンドアプローチを提案する。
論文 参考訳（メタデータ） (2024-06-02T17:47:06Z) - A Provably Effective Method for Pruning Experts in Fine-tuned Sparse Mixture-of-Experts [49.394145046409044]
本論文は,MoEモデルにおけるエキスパートの刈り取りに有効な手法として,初めて提案するものである。
理論的には、事前訓練されたモデルからルータl2ノルムを小さく変更することで、専門家のプルーニングを優先順位付けすることで、テスト精度の維持が保証される。
我々の理論解析は、単純化されたMoEアーキテクチャ上でのバイナリ分類タスクに重点を置いているが、我々の専門的なプルーニング手法は、大きな視覚的MoEモデルに基づいて検証されている。
論文 参考訳（メタデータ） (2024-05-26T17:52:58Z) - Skills Composition Framework for Reconfigurable Cyber-Physical Production Modules [44.99833362998488]
本稿では、スキルベースの再構成可能なサイバー物理生産モジュールにおけるスキルの構成と実行のためのフレームワークを提案する。
分散ビヘイビアツリー(BT)に基づいており、低レベルのデバイス固有のコードとAIベースのタスク指向フレームワークとの良好な統合を提供する。
論文 参考訳（メタデータ） (2024-05-22T12:56:05Z) - OSM: Leveraging Model Checking for Observing Dynamic 1 behaviors in
Aspect-Oriented Applications [0.0]
観測ベース統計モデルチェック(OSM)フレームワークは、基本的なシステムコードから直接実行可能な形式モデルを構築するために開発された。
これにより、プリコンディションシフト中の電子健康記録システムの未収量性能が保証される。
論文 参考訳（メタデータ） (2024-03-03T00:03:34Z) - ESBMC v7.4: Harnessing the Power of Intervals [4.6232063855710654]
ESBMCはモデルチェックのために多くの最先端技術を実装しています。
新しい機能によって、サポート対象のプログラムやプロパティの検証結果が得られます。
ESBMCは、検証性能を向上させるために、プログラム内の式を新しい間隔で解析する。
論文 参考訳（メタデータ） (2023-12-22T14:56:46Z) - A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳（メタデータ） (2023-09-12T09:37:26Z) - A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification [8.733354577147093]
本稿では,Large Language Models(LLM)とFormal Verification戦略を組み合わせたソフトウェア脆弱性の自動修復手法を提案する。
我々は、ESBMC-AIフレームワークを概念実証として、よく認識され、業界に受け入れられたSMTベースのコンテキスト境界モデルチェッカー(ESBMC)と事前訓練されたトランスフォーマーモデルを活用する。
本研究は,バッファオーバーフローや演算オーバーフロー,ポインタ参照障害などの問題を高精度に検出および修正するESBMC-AIの機能を示すものである。
論文 参考訳（メタデータ） (2023-05-24T05:54:10Z) - Relational Action Bases: Formalization, Effective Safety Verification,
and Invariants (Extended Version) [67.99023219822564]
我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。
RABは両方の制限を解除することで既存のモデルを一般化する。
データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
論文 参考訳（メタデータ） (2022-08-12T17:03:50Z) - MMOCR: A Comprehensive Toolbox for Text Detection, Recognition and
Understanding [70.16678926775475]
MMOCRは、テキストの検出と認識のためのオープンソースのツールボックスである。
それは14の最先端のアルゴリズムを実装しており、これは私たちが現在知っているすべてのオープンソースのOCRプロジェクトよりも多い。
論文 参考訳（メタデータ） (2021-08-14T14:10:23Z) - Explanations of Machine Learning predictions: a mandatory step for its
application to Operational Processes [61.20223338508952]
信用リスクモデリングは重要な役割を果たす。
近年,機械学習や深層学習の手法が採用されている。
この分野における説明可能性問題に LIME 手法を適用することを提案する。
論文 参考訳（メタデータ） (2020-12-30T10:27:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。