論文の概要: Cargo Sherlock: An SMT-Based Checker for Software Trust Costs

• arxiv url: http://arxiv.org/abs/2512.12553v1
• Date: Sun, 14 Dec 2025 04:59:10 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-16 17:54:56.312538
• Title: Cargo Sherlock: An SMT-Based Checker for Software Trust Costs
• Title（参考訳）: Cargo Sherlock: SMTベースのソフトウェア信頼コストチェッカー
• Authors: Muhammad Hassnain, Anirudh Basu, Ethan Ng, Caleb Stanford,
• Abstract要約: 本稿では,サードパーティソフトウェア依存の信頼度を定量化するための公式な枠組みを提案する。 ソフトウェア分析ツールとメタデータからのデータを使用して、ソフトウェア依存関係の1次リレーショナルモデルを構築します。 私たちはこれらのアイデアを、Rustライブラリ(クラテス)をターゲットにしたCargo Sherlockに実装しています。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Supply chain attacks threaten open-source software ecosystems. This paper proposes a formal framework for quantifying trust in third-party software dependencies that is both formally checkable - formalized in satisfiability modulo theories (SMT) - while at the same time incorporating human factors, like the number of downloads, authors, and other metadata that are commonly used to identify trustworthy software in practice. We use data from both software analysis tools and metadata to build a first-order relational model of software dependencies; to obtain an overall "trust cost" combining these factors, we propose a formalization based on the minimum trust problem which asks for the minimum cost of a set of assumptions which can be used to prove that the code is safe. We implement these ideas in Cargo Sherlock, targeted for Rust libraries (crates), incorporating a list of candidate assumptions motivated by quantifiable trust metrics identified in prior work. Our evaluation shows that Cargo Sherlock can be used to identify synthetically generated supply chain attacks and known incidents involving typosquatted and poorly AI-maintained crates, and that its performance scales to Rust crates with many dependencies.
• Abstract（参考訳）: サプライチェーン攻撃は、オープンソースのソフトウェアエコシステムを脅かす。 本稿では, ダウンロード数, 著者数, 信頼性の高いソフトウェアを識別するメタデータなど, 人的要因を取り入れつつ, 形式的に検証可能な, 満足度変調理論(SMT)を定式化した, サードパーティソフトウェア依存関係の信頼度を定量化する形式的枠組みを提案する。 我々は、ソフトウェア分析ツールとメタデータの両方から得られたデータを用いて、ソフトウェア依存の1次関係モデルを構築する。これらの要因を組み合わせた総合的な「信頼コスト」を得るため、コードの安全性を証明するために使用できる一連の仮定の最小コストを求める最小信頼問題に基づく形式化を提案する。 私たちはこれらのアイデアを,Rustライブラリ(クラテス)をターゲットにしたCargo Sherlockに実装しています。 我々の評価によると、Cargo Sherlockは、シンボクテッドでAIのメンテナンスが不十分なクレートを含む、合成生成されたサプライチェーン攻撃や既知のインシデントを識別するために使用することができ、そのパフォーマンスは、多くの依存関係を持つRustクレートにスケール可能である。

関連論文リスト

• An LLM Agentic Approach for Legal-Critical Software: A Case Study for Tax Prep Software [7.672965856139587]
  大規模言語モデル(LLM)は、自然言語の規則を実行可能な論理に変換することを約束している。 本稿では,米国連邦政府の税制改革を事例として,法的に重要なソフトウェアを開発するためのエージェント的アプローチを提案する。
  論文  参考訳（メタデータ） (2025-09-16T19:13:26Z)
• Evaluating Language Model Reasoning about Confidential Information [95.64687778185703]
  言語モデルが文脈的堅牢性を示すか、文脈依存型安全仕様に準拠する能力を示すかを検討する。 我々は,ユーザ要求がいつ承認されたか,言語モデルが正しく判断できるかどうかを測定するベンチマーク(PasswordEval)を開発した。 現在のオープンソースとクローズドソースのモデルでは、一見単純な作業に苦労しています。
  論文  参考訳（メタデータ） (2025-08-27T15:39:46Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
  LLM(Commercial Large Language Model) APIは基本的な信頼の問題を生み出します。 ユーザーは特定のモデルに課金するが、プロバイダが忠実に提供できることを保証することはない。 我々は,このモデル置換問題を定式化し,現実的な逆条件下での検出方法を評価する。 我々は,信頼された実行環境(TEE)を実用的で堅牢なソリューションとして使用し,評価する。
  論文  参考訳（メタデータ） (2025-04-07T03:57:41Z)
• Bomfather: An eBPF-based Kernel-level Monitoring Framework for Accurate Identification of Unknown, Unused, and Dynamically Loaded Dependencies in Modern Software Supply Chains [0.0]
  依存性追跡手法の不正確さは、現代のソフトウェアサプライチェーンのセキュリティと整合性を損なう。 本稿では,拡張バークレーパケットフィルタ(eBPF)を利用したカーネルレベルのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-03-03T22:32:59Z)
• Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs [7.087237546722617]
  ソフトウェア正当性を確立する最も強力な方法の1つは、フォーマルな方法を使用することである。 私たちの仕事は、形式モデルの作成を自動化することで、この重大な欠点に対処します。 このようにして、形式モデルを作成するのに必要な時間を大幅に削減する。
  論文  参考訳（メタデータ） (2025-01-22T15:57:29Z)
• Automating SBOM Generation with Zero-Shot Semantic Similarity [2.169562514302842]
  Software-Bill-of-Materials (SBOM)は、ソフトウェアアプリケーションのコンポーネントと依存関係を詳述した総合的なインベントリである。 本稿では,破壊的なサプライチェーン攻撃を防止するため,SBOMを自動生成する手法を提案する。 テスト結果は説得力があり、ゼロショット分類タスクにおけるモデルの性能を示す。
  論文  参考訳（メタデータ） (2024-02-03T18:14:13Z)
• Auditing and Generating Synthetic Data with Controllable Trust Trade-offs [54.262044436203965]
  合成データセットとAIモデルを包括的に評価する総合監査フレームワークを導入する。 バイアスや差別の防止、ソースデータへの忠実性の確保、実用性、堅牢性、プライバシ保護などに焦点を当てている。 多様なユースケースにまたがる様々な生成モデルを監査することにより,フレームワークの有効性を実証する。
  論文  参考訳（メタデータ） (2023-04-21T09:03:18Z)
• PEOPL: Characterizing Privately Encoded Open Datasets with Public Labels [59.66777287810985]
  プライバシとユーティリティのための情報理論スコアを導入し、不誠実なユーザの平均パフォーマンスを定量化する。 次に、ランダムなディープニューラルネットワークの使用を動機付ける符号化スキームのファミリーを構築する際のプリミティブを理論的に特徴づける。
  論文  参考訳（メタデータ） (2023-03-31T18:03:53Z)
• Detecting Security Fixes in Open-Source Repositories using Static Code Analyzers [8.716427214870459]
  機械学習(ML)アプリケーションにおけるコミットを表現する機能として,既製の静的コードアナライザの出力がどの程度使用されるかを検討する。 埋め込みの構築やMLモデルをトレーニングして、脆弱性修正を含むソースコードコミットを自動的に識別する方法について検討する。 当社のメソッドとcommit2vecの組み合わせは,脆弱性を修正するコミットの自動識別において,最先端技術よりも明確な改善であることがわかった。
  論文  参考訳（メタデータ） (2021-05-07T15:57:17Z)

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

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