論文の概要: 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クレートにスケール可能である。

関連論文リスト

• IMMACULATE: A Practical LLM Auditing Framework via Verifiable Computation [49.796717294455796]
  経済的なモチベーションのある逸脱を検出するための実践的な監査フレームワークIMMACULATEを提案する。 IMMACULATEは、検証可能な計算を用いて少数のリクエストを選択的に監査し、暗号オーバーヘッドを償却しながら強力な検出保証を達成する。
  論文  参考訳（メタデータ） (2026-02-26T07:21:02Z)
• An Empirical Study on Remote Code Execution in Machine Learning Model Hosting Ecosystems [4.409447722044799]
  モデルローディング中の信頼できないコードの実行は、モデル共有プラットフォームに対するセキュリティ上の懸念である。 5つの主要なモデル共有プラットフォームにわたるカスタムモデルローディングプラクティスに関する、最初の大規模な実証的研究を行います。
  論文  参考訳（メタデータ） (2026-01-20T17:13:42Z)
• Agentic AI for Autonomous Defense in Software Supply Chain Security: Beyond Provenance to Vulnerability Mitigation [0.0]
  本論文は,自律型ソフトウェアサプライチェーンセキュリティに基づくエージェント人工知能(AI)の例を含む。 大規模言語モデル(LLM)ベースの推論、強化学習(RL)、マルチエージェント調整を組み合わせている。 その結果、エージェントAIは、自己防衛的で積極的なソフトウェアサプライチェーンへの移行を促進することが示されている。
  論文  参考訳（メタデータ） (2025-12-29T14:06:09Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。 本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
  論文  参考訳（メタデータ） (2025-10-02T06:25:10Z)
• 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)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• 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)

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

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