論文の概要: Towards Formal Verification of a TPM Software Stack

• arxiv url: http://arxiv.org/abs/2307.16821v1
• Date: Mon, 31 Jul 2023 16:35:16 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-23 15:50:21.610791
• Title: Towards Formal Verification of a TPM Software Stack
• Title（参考訳）: TPMソフトウェアスタックの形式検証に向けて
• Authors: Yani Ziani and Nikolai Kosmatov and Fr\'ed\'eric Loulergue and Daniel Gracia P\'erez and T\'eo Bernier
• Abstract要約: 本稿では,Frama-C 検証プラットフォームを用いた tpm2-ts の形式的検証について述べる。 リンクされたリストと複雑なデータ構造に基づいて、ライブラリのコードは検証ツールにとって非常に難しいように思える。
• 参考スコア（独自算出の注目度）: 0.5074812070492739
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: The Trusted Platform Module (TPM) is a cryptoprocessor designed to protect integrity and security of modern computers. Communications with the TPM go through the TPM Software Stack (TSS), a popular implementation of which is the open-source library tpm2-tss. Vulnerabilities in its code could allow attackers to recover sensitive information and take control of the system. This paper describes a case study on formal verification of tpm2-tss using the Frama-C verification platform. Heavily based on linked lists and complex data structures, the library code appears to be highly challenging for the verification tool. We present several issues and limitations we faced, illustrate them with examples and present solutions that allowed us to verify functional properties and the absence of runtime errors for a representative subset of functions. We describe verification results and desired tool improvements necessary to achieve a full formal verification of the target code.
• Abstract（参考訳）: Trusted Platform Module (TPM) は、現代のコンピュータの完全性とセキュリティを保護するために設計された暗号プロセッサである。 TPMとの通信は、オープンソースライブラリtpm2-tssであるTPM Software Stack (TSS)を介して行われる。 コードの脆弱性により、攻撃者は機密情報を回復し、システムを制御できる。 本稿では,Frama-C 検証プラットフォームを用いた tpm2-ts の形式的検証について述べる。 リンクリストと複雑なデータ構造をベースとしたライブラリコードは、検証ツールにとって非常に難しいようだ。 対象とするいくつかの問題と制限を提示し、機能特性の検証と関数の代表的なサブセットに対する実行時エラーの欠如を可能にする例とソリューションを示します。 対象コードの完全な形式的検証を実現するために必要な検証結果と所望のツール改善について述べる。

関連論文リスト

• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。 私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
  論文  参考訳（メタデータ） (2024-11-20T14:16:55Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• DetToolChain: A New Prompting Paradigm to Unleash Detection Ability of MLLM [81.75988648572347]
  DetToolChainはマルチモーダル大言語モデル(MLLM)のゼロショットオブジェクト検出能力を解き放つ新しいパラダイムである。 提案手法は,高精度検出にヒントを得た検出プロンプトツールキットと,これらのプロンプトを実装するための新しいChain-of-Thoughtから構成される。 DetToolChainを用いたGPT-4Vは,オープン語彙検出のための新しいクラスセットにおいて,最先端のオブジェクト検出器を+21.5%AP50で改善することを示す。
  論文  参考訳（メタデータ） (2024-03-19T06:54:33Z)
• DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
  プロパティベースのテストはセキュアプロトコルのセキュリティバグの検出に有効である。 セキュアマルチパーティ計算(MPC)を特に対象とする。 MPCプロトコルのビットレベル実装において,様々な欠陥を検出するテストを作成する。
  論文  参考訳（メタデータ） (2024-03-08T02:02:24Z)
• HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
  信頼性コンピューティングは、Trusted Execution Environments(TEEs)と呼ばれる特別なハードウェア隔離ユニットを使用して、コテナントクラウドデプロイメントにおける機密コードとデータの保護を可能にする。 低レベルのC/C++ベースのツールチェーンを提供するTEEは、固有のメモリ安全性の脆弱性の影響を受けやすく、明示的で暗黙的な情報フローのリークを監視するための言語構造が欠如している。 私たちは、Haskellに埋め込まれたドメイン固有言語(cla)であるHasTEE+を使って、上記の問題に対処します。
  論文  参考訳（メタデータ） (2024-01-17T00:56:23Z)
• Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security [0.0]
  メモリ管理の誤った仕様と実装は、システムのクラッシュや悪用可能な攻撃につながる可能性がある。 本稿では,実世界のOSにおける並列メモリ管理の最初の正式な仕様と機構的証明について述べる。
  論文  参考訳（メタデータ） (2023-09-17T03:41:10Z)
• A Novel Approach to Identify Security Controls in Source Code [4.598579706242066]
  本稿では,一般的なセキュリティ制御の包括的リストを列挙し,それぞれにデータセットを作成する。 最新のNLP技術であるBERT(Bidirectional Representations from Transformers)とTactic Detector(Tactic Detector)を使って、セキュリティコントロールを高い信頼性で識別できることを示しています。
  論文  参考訳（メタデータ） (2023-07-10T21:14:39Z)
• (Security) Assertions by Large Language Models [25.270188328436618]
  セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(LLM)を用いることを検討する。 我々は、人気のあるLCMに注目し、プロンプトの様々なレベルの詳細を考慮し、アサーションを箱から書き出す能力を特徴付ける。
  論文  参考訳（メタデータ） (2023-06-24T17:44:36Z)
• Monitoring ROS2: from Requirements to Autonomous Robots [58.720142291102135]
  本稿では,構造化自然言語で記述された要件から自律ロボットのランタイムモニタを生成するための形式的アプローチの概要について述べる。 当社のアプローチでは,Fletal Requirement Elicitation Tool (FRET) とランタイム検証フレームワークであるCopilotを,Ogma統合ツールを通じて統合しています。
  論文  参考訳（メタデータ） (2022-09-28T12:19:13Z)
• Towards Semantic Communication Protocols: A Probabilistic Logic Perspective [69.68769942563812]
  我々は,NPMを確率論理型言語ProbLogで記述された解釈可能なシンボルグラフに変換することによって構築された意味プロトコルモデル(SPM)を提案する。 その解釈性とメモリ効率を利用して、衝突回避のためのSPM再構成などのいくつかの応用を実演する。
  論文  参考訳（メタデータ） (2022-07-08T14:19:36Z)
• Conformance Checking with Uncertainty via SMT (Extended Version) [66.58864135810981]
  データ認識参照プロセスに対する不確実なログの適合性を確認する方法を示す。 我々のアプローチはモジュラーであり、異なるタイプの不確実性に均質に適合する。 本研究は,概念実証によるアプローチの正しさと実現可能性を示す。
  論文  参考訳（メタデータ） (2022-06-15T11:39:45Z)

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

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