論文の概要: Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking

• arxiv url: http://arxiv.org/abs/2311.05281v1
• Date: Thu, 9 Nov 2023 11:25:24 GMT
• ステータス: 処理完了
• システム内更新日: 2023-11-10 15:27:16.425015
• Title: Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking
• Title（参考訳）: 有界モデルチェックによるオープンソースcプロジェクトのソフトウェア脆弱性発見
• Authors: Janislley Oliveira de Sousa and Bruno Carvalho de Farias and Thales Araujo da Silva and Eddie Batista de Lima Filho and Lucas C. Cordeiro
• Abstract要約: 我々は,汎用ソフトウェアシステムの脆弱性を効果的に検出できる境界モデル検査手法を提唱する。 我々は,最先端の有界モデルチェッカーを用いて,大規模ソフトウェアシステムを検証する手法を開発し,評価した。
• 参考スコア（独自算出の注目度）: 2.9129603096077332
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Computer-based systems have solved several domain problems, including industrial, military, education, and wearable. Nevertheless, such arrangements need high-quality software to guarantee security and safety as both are mandatory for modern software products. We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems. However, such an approach struggles to scale up and verify extensive code bases. Consequently, we have developed and evaluated a methodology to verify large software systems using a state-of-the-art bounded model checker. In particular, we pre-process input source-code files and guide the respective model checker to explore them systematically. Moreover, the proposed scheme includes a function-wise prioritization strategy, which readily provides results for code entities according to a scale of importance. Experimental results using a real implementation of the proposed methodology show that it can efficiently verify large software systems. Besides, it presented low peak memory allocation when executed. We have evaluated our approach by verifying twelve popular open-source C projects, where we have found real software vulnerabilities that their developers confirmed.
• Abstract（参考訳）: コンピュータベースのシステムは、産業、軍、教育、ウェアラブルなど、いくつかのドメイン問題を解決した。 それでも、これらのアレンジメントは、セキュリティと安全性を保証するために高品質なソフトウェアを必要としている。 我々は,汎用ソフトウェアシステムの脆弱性を効率的に検出できる境界モデルチェック技術を提案する。 しかし、このようなアプローチはスケールアップと広範なコードベースの検証に苦労している。 そこで我々は,最先端境界モデルチェッカーを用いた大規模ソフトウェアシステムの検証手法を開発し,評価した。 特に、入力ソースコードファイルを前処理し、各モデルチェッカーをガイドして体系的に検討します。 さらに,提案手法は,重要度尺度に従って,コードエンティティに容易に結果を提供する機能的優先順位付け戦略を含む。 提案手法の実際の実装による実験結果から,大規模ソフトウェアシステムの有効性が示された。 さらに、実行時のピークメモリ割り当ても低かった。 私たちは12の人気のあるオープンソースCプロジェクトを検証することで、私たちのアプローチを評価しました。

関連論文リスト

• A Combined Feature Embedding Tools for Multi-Class Software Defect and Identification [2.2020053359163305]
  本稿では,GraphCodeBERTとGraph Convolutional Networkを組み合わせた実験手法であるCodeGraphNetを提案する。 この方法は、機能間の複雑な関係船をキャプチャし、脆弱性のより正確な識別と分離を可能にする。 決定木とニューラルネットワークのハイブリッドであるDeepTreeモデルは、最先端のアプローチよりも優れています。
  論文  参考訳（メタデータ） (2024-11-26T17:33:02Z)
• Divide and Conquer based Symbolic Vulnerability Detection [0.16385815610837165]
  本稿では,シンボル実行と制御フローグラフ解析に基づく脆弱性検出手法を提案する。 提案手法では,無関係なプログラム情報を除去するために,分割・分散アルゴリズムを用いる。
  論文  参考訳（メタデータ） (2024-09-20T13:09:07Z)
• Patch2QL: Discover Cognate Defects in Open Source Software Supply Chain With Auto-generated Static Analysis Rules [1.9591497166224197]
  本稿では,SASTルールの自動生成によるOSSのコグネート欠陥の検出手法を提案する。 具体的には、プリパッチバージョンとポストパッチバージョンから重要な構文と意味情報を抽出する。 我々はPatch2QLというプロトタイプツールを実装し、それをC/C++の基本OSSに適用した。
  論文  参考訳（メタデータ） (2024-01-23T02:23:11Z)
• Causative Insights into Open Source Software Security using Large Language Code Embeddings and Semantic Vulnerability Graph [3.623199159688412]
  オープンソースソフトウェア(OSS)の脆弱性は、不正アクセス、データ漏洩、ネットワーク障害、プライバシー侵害を引き起こす可能性がある。 最近のディープラーニング技術は、ソースコードの脆弱性を特定し、ローカライズする上で大きな可能性を示しています。 本研究は,従来の方法に比べてコード修復能力が24%向上したことを示す。
  論文  参考訳（メタデータ） (2024-01-13T10:33:22Z)
• 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)
• CodeLMSec Benchmark: Systematically Evaluating and Finding Security Vulnerabilities in Black-Box Code Language Models [58.27254444280376]
  自動コード生成のための大規模言語モデル(LLM)は、いくつかのプログラミングタスクにおいてブレークスルーを達成した。 これらのモデルのトレーニングデータは、通常、インターネット(例えばオープンソースのリポジトリから)から収集され、障害やセキュリティ上の脆弱性を含む可能性がある。 この不衛生なトレーニングデータは、言語モデルにこれらの脆弱性を学習させ、コード生成手順中にそれを伝播させる可能性がある。
  論文  参考訳（メタデータ） (2023-02-08T11:54:07Z)
• Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
  本稿は、正式に認証されたシステムを作成し、実際に使用するためにデプロイした各種のアプリケーション分野のプロジェクトについて検討する。 使用する技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
  論文  参考訳（メタデータ） (2023-01-05T18:18:46Z)
• Evaluating Model-free Reinforcement Learning toward Safety-critical Tasks [70.76757529955577]
  本稿では、国家安全RLの観点から、この領域における先行研究を再考する。 安全最適化と安全予測を組み合わせた共同手法であるUnrolling Safety Layer (USL)を提案する。 この領域のさらなる研究を容易にするため、我々は関連するアルゴリズムを統一パイプラインで再現し、SafeRL-Kitに組み込む。
  論文  参考訳（メタデータ） (2022-12-12T06:30:17Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。 次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。 これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
  論文  参考訳（メタデータ） (2022-08-23T05:02:09Z)
• Increasing the Confidence of Deep Neural Networks by Coverage Analysis [71.57324258813674]
  本稿では、異なる安全でない入力に対してモデルを強化するために、カバレッジパラダイムに基づく軽量な監視アーキテクチャを提案する。 実験結果から,提案手法は強力な対向例とアウト・オブ・ディストリビューション・インプットの両方を検出するのに有効であることが示唆された。
  論文  参考訳（メタデータ） (2021-01-28T16:38:26Z)
• Dos and Don'ts of Machine Learning in Computer Security [74.1816306998445]
  大きな可能性にもかかわらず、セキュリティにおける機械学習は、パフォーマンスを損なう微妙な落とし穴を引き起こす傾向がある。 我々は,学習ベースのセキュリティシステムの設計,実装,評価において共通の落とし穴を特定する。 我々は,落とし穴の回避や軽減を支援するために,研究者を支援するための実用的な勧告を提案する。
  論文  参考訳（メタデータ） (2020-10-19T13:09:31Z)

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

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