論文の概要: HornFuzz: Fuzzing CHC solvers
- arxiv url: http://arxiv.org/abs/2306.04281v2
- Date: Thu, 8 Jun 2023 14:19:55 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-24 04:15:11.000702
- Title: HornFuzz: Fuzzing CHC solvers
- Title（参考訳）: HornFuzz: ファジィCHCソルバ
- Authors: Anzhela Sukhanova, Valentyn Sobol
- Abstract要約: 我々はCHCソルバのバグを検出するための変異ベースのグレーボックスファジリング技術であるHhornFuzzを提案する。
ファジッカーを高性能CHCソルバの1つであるスペーサーで評価し、スペーサーでいくつかのバグを発見した。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Many advanced program analysis and verification methods are based on solving
systems of Constrained Horn Clauses (CHC). Testing CHC solvers is very
important, as correctness of their work determines whether bugs in the analyzed
programs are detected or missed. One of the well-established and efficient
methods of automated software testing is fuzzing: analyzing the reactions of
programs to random input data. Currently, there are no fuzzers for CHC solvers,
and fuzzers for SMT solvers are not efficient in CHC solver testing, since they
do not consider CHC specifics. In this paper, we present HornFuzz, a
mutation-based gray-box fuzzing technique for detecting bugs in CHC solvers
based on the idea of metamorphic testing. We evaluated our fuzzer on one of the
highest performing CHC solvers, Spacer, and found a handful of bugs in Spacer.
In particular, some discovered problems are so serious that they require fixes
with significant changes to the solver.
- Abstract（参考訳）: 多くの高度なプログラム解析と検証手法は、制約付きホーンクロース(CHC)の解法に基づいている。
chcソルバのテストは、その作業の正確性が解析されたプログラムのバグが検出されるか見逃されるかを決定するため、非常に重要である。
ソフトウェア自動テストの確立された効率的な方法の1つはファジングであり、ランダムな入力データに対するプログラムの反応を分析することである。
現在、CHCソルバのファズーは存在せず、SMTソルバのファズーはCHC特異性を考慮していないため、CHCソルバのテストでは効率が良くない。
本稿では,変成テストの考え方に基づいて,CHCソルバのバグを検出する変異ベースのグレーボックスファジリング技術であるHhornFuzzを提案する。
ファジッカーを高性能なCHCソルバの一つであるスペーサーで評価し、スペーサーでいくつかのバグを発見した。
特に、発見された問題のいくつかは非常に深刻であるため、解決法に大きな変更を加える修正が必要となる。
関連論文リスト
- FuzzCoder: Byte-level Fuzzing Test via Large Language Model [46.18191648883695]
我々は,攻撃を成功させることで,入力ファイルのパターンを学習するために,微調整された大言語モデル(FuzzCoder)を採用することを提案する。
FuzzCoderは、プログラムの異常な動作を引き起こすために、入力ファイル内の突然変異位置と戦略位置を予測することができる。
論文 参考訳（メタデータ） (2024-09-03T14:40:31Z) - HuntFUZZ: Enhancing Error Handling Testing through Clustering Based Fuzzing [19.31537246674011]
本稿では,SFIベースのファジィフレームワークであるHuntFUZZを紹介する。
我々はHuntFUZZを42のアプリケーションで評価し、HuntFUZZは162の既知のバグを明らかにし、そのうち62のバグはエラー処理に関連している。
論文 参考訳（メタデータ） (2024-07-05T06:58:30Z) - 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) - Cal-DETR: Calibrated Detection Transformer [67.75361289429013]
本稿では,Deformable-DETR,UP-DETR,DINOのキャリブレーション検出トランス(Cal-DETR)のメカニズムを提案する。
我々は、不確実性を利用してクラスロジットを変調する不確実性誘導ロジット変調機構を開発する。
その結果、Cal-DETRは、ドメイン内およびドメイン外の両方を校正する競合する列車時間法に対して有効であることがわかった。
論文 参考訳（メタデータ） (2023-11-06T22:13:10Z) - Fuzzing for CPS Mutation Testing [3.512722797771289]
本稿では, ファジテストを利用した突然変異検査手法を提案し, C および C++ ソフトウェアで有効であることが証明された。
実験により, ファジテストに基づく突然変異試験は, シンボル実行よりも高い頻度で生存変異体を殺傷することが明らかとなった。
論文 参考訳（メタデータ） (2023-08-15T16:35:31Z) - Systematic Assessment of Fuzzers using Mutation Analysis [20.91546707828316]
ソフトウェアテストでは、テスト品質を評価するためのゴールドスタンダードは突然変異解析である。
突然変異解析は、様々なカバレッジ対策を仮定し、大規模で多様な障害セットを提供する。
複数の突然変異をプールし、初めて(初めて)ファジィを突然変異解析と比較する現代の突然変異解析技術を適用します。
論文 参考訳（メタデータ） (2022-12-06T15:47:47Z) - ADPTriage: Approximate Dynamic Programming for Bug Triage [0.0]
オンラインバグトリアージタスクのためのマルコフ決定プロセス(MDP)モデルを開発した。
私たちはADPTriageと呼ばれるADPベースのバグトリアージソリューションを提供しています。
以上の結果から, 代入精度と固定時間の観点から, ミオピックアプローチよりも有意な改善が見られた。
論文 参考訳（メタデータ） (2022-11-02T04:42:21Z) - Rethinking Transformer-based Set Prediction for Object Detection [57.7208561353529]
実験の結果,提案手法は元のDETRよりもはるかに高速に収束するだけでなく,検出精度の点でDTRや他のベースラインよりも優れていた。
論文 参考訳（メタデータ） (2020-11-21T21:59:42Z) - Detecting Rewards Deterioration in Episodic Reinforcement Learning [63.49923393311052]
多くのRLアプリケーションでは、トレーニングが終了すると、エージェント性能の劣化をできるだけ早く検出することが不可欠である。
我々は,各エピソードにおける報酬が独立でもなく,同一に分散した,マルコフでもない,エピソード的枠組みを考察する。
平均シフトは、時間信号の劣化(報酬など)に対応する方法で定義し、最適な統計的パワーでこの問題の試行を導出する。
論文 参考訳（メタデータ） (2020-10-22T12:45:55Z) - Counterfactual Variable Control for Robust and Interpretable Question
Answering [57.25261576239862]
ディープニューラルネットワークに基づく質問応答(QA)モデルは、多くの場合、堅牢でも説明もできない。
本稿では、因果推論を用いてQAモデルのこのような突発的な「能力」を検証する。
本稿では,任意のショートカット相関を明示的に緩和する,CVC(Counterfactual Variable Control)という新しい手法を提案する。
論文 参考訳（メタデータ） (2020-10-12T10:09:05Z) - Selective Question Answering under Domain Shift [90.021577320085]
モデルがドメイン外の入力に対して過度に信頼されているため、モデルのソフトマックス確率のみに基づくアテンションポリシーは不適切である。
キャリブレータをトレーニングして、QAモデルがアースする入力を識別し、エラーを予測した場合に停止する。
提案手法は,80%の精度を維持しながら56%の質問に回答するが,それに対してモデルの確率を直接使用する場合,80%の精度で48%しか回答しない。
論文 参考訳（メタデータ） (2020-06-16T19:13:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。