論文の概要: Lie to Me: Finding Bugs in ZK DSL Toolchains with Adversarial Witness Injection
- arxiv url: http://arxiv.org/abs/2608.30648v1
- Date: Mon, 31 Aug 2026 11:50:37 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-01 18:31:31.374859
- Title: Lie to Me: Finding Bugs in ZK DSL Toolchains with Adversarial Witness Injection
- Title（参考訳）: Lie to Me: 逆境性注入によるZK DSLツールチェーンのバグ発見
- Abstract要約: 我々は、ZK DSLプログラムを生成し、敵対的な目撃者注入を通じてバグを公開するテストフレームワークであるLiezzを紹介する。
生成された決定論的プログラムごとに、Liezzは2つの公開入力を異なる出力で実行し、証人をスプリスし、一方の実行の入力と他方の実行の出力を組み合わせる。
制御された分岐と複数の目撃者分離戦略は、不足する制約を明らかにするのに十分な一貫性を維持します。
- 参考スコア（独自算出の注目度）: 3.6756416620917522
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Zero-knowledge domain-specific language (ZK DSL) toolchains compile programs into constraint systems and generate witnesses for cryptographic proofs. Bugs in these toolchains can leave the enforced constraints weaker than the source-program semantics, admitting proofs for invalid executions. Such soundness bugs may remain invisible to valid-execution testing because all valid executions still behave correctly. We present Liezz, a testing framework that generates ZK DSL programs and exposes these bugs through adversarial witness injection. For each generated deterministic program, Liezz executes two public input assignments with different outputs and splices their witnesses, combining the input of one execution with the output of the other. The resulting witness is invalid by construction. A correct toolchain must reject it; acceptance exposes a soundness bug. Controlled divergence and multiple witness-splicing strategies preserve enough consistency to expose missing constraints. Liezz also generates parameterized standard-library calls to reach complex functionality. Liezz supports Circom, Corset, Gnark, and Noir. It finds 13 bugs, including seven with soundness impact. Several are reachable only through generated standard-library calls. Under the same testing budget, a valid-execution baseline does not expose any of the soundness failures revealed by accepted injected witnesses, showing that adversarial witness injection reaches failures missed by valid-execution testing.
- Abstract（参考訳）: ゼロ知識ドメイン固有言語(ZK DSL)ツールチェーンは、プログラムを制約システムにコンパイルし、暗号証明の証人を生成する。
これらのツールチェーンのバグは、強制された制約をソースコードのセマンティクスよりも弱くし、無効な実行の証明を認めることができる。
このような健全性バグは、有効な実行テストには見えません。
本稿では,ZK DSLプログラムを生成するテストフレームワークであるLiezzを紹介する。
生成された決定論的プログラムごとに、Liezzは2つの公開入力を異なる出力で実行し、証人をスプリスし、一方の実行の入力と他方の実行の出力を組み合わせる。
その証人は建設によって無効になる。
正しいツールチェーンはそれを拒否しなければならない。
制御された分岐と複数の目撃者分離戦略は、不足する制約を明らかにするのに十分な一貫性を維持します。
Liezzは複雑な機能に到達するためにパラメタライズされた標準ライブラリコールも生成する。
LiezzはCircom、Corset、Gnark、Noirをサポートしている。
13のバグがあり、そのうち7つは音質への影響がある。
いくつかは生成された標準ライブラリ呼び出しを通じてのみアクセス可能である。
同じテスト予算の下では、有効な実行ベースラインは、承認されたインジェクトによって明らかにされた健全性障害を公開せず、敵の目撃インジェクションが有効な実行テストで見逃された障害に到達していることを示す。
関連論文リスト
- RosettaBitcoin: An Artifact-Backed Experience Report on Verification Infrastructure for Agent-Assisted Consensus Validators [0.0]
この体験レポートは、12の個別に実装されたBitcoin testnet4コンセンサスバリデータを構築した、単一開発者プロジェクトであるRosettaBitcoinを調査している。
スナップショットの追跡されたエビデンスデータベース、キュレートされたアーティファクトインデックス、標準適合フィクスチャ、検証スクリプト、ブロッカレコード、バージョン履歴を分析します。
このケースは、明示的な障害記録、フィクスチャ、ポート所有、バリデーションがエージェントアシストシステムをより監査可能にすることを示唆している。
論文 参考訳（メタデータ） (2026-09-01T17:22:07Z) - PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
我々は、スケジューリング、検証、メモリ、ベンチマーク、安全性をシステムレベルのサービスとして提供するPhyAgentOSを紹介します。
セッション中心のセッションは、スケジューリング、互換性、監督された実行、エビデンス収集、受け入れの最小単位として、アクションではなくセッションを扱う。
SessionVerifierは、実行終了とセマンティックタスク完了を、成功、失敗、または再計画のエビデンスに基づいて判断する。
ベンチマークはデプロイメントセッションと検証パスを再利用するので、結果は実際の実行に遡る。
論文 参考訳（メタデータ） (2026-07-18T04:46:53Z) - TTHE: Test-Time Harness Evolution [50.26245555541721]
既存のアプローチでは、デプロイ前、トレーニング前、あるいはテスト時に凍結される固定されたエージェントワークフローの開発データを最適化する。
我々は、エージェントがテスト入力で生成するラベルのない実行トレースのみを使用して、評価自体にハーネスを最適化できるかどうかを問う。
評価中、TTHEは候補ハーネスの人口を維持し、それらの実行トレースの理由をエージェントプロジェクタを通じてそれらを洗練する。
その後、審査員は実行元プロキシ信号から改善されたハーネスをコミットし、選択したプログラムは継続してその後の入力を統治する。
論文 参考訳（メタデータ） (2026-07-09T05:53:39Z) - A Minimal Executable Proof for Multi-Language Contract Traceability [0.0]
本報告ではDAG-TOML契約の検証を意図的に行う。
コントラクト、実装グラフ、トレーサビリティチェーン、レビューゲートが実行可能な目撃者に対してどのようにチェックできるかを示している。
論文 参考訳（メタデータ） (2026-05-27T14:37:26Z) - CIVeX: Causal Intervention Verification for Language Agents [0.0]
我々はCIVeXという因果介入検証器を導入し、提案した動作をコミットされた動作状態グラフ上の構造因果クエリにマッピングする。
Causal-ToolBench (1,890のインスタンス、7つのシード)では、CIVeXは中等度および対向的な共起で観測された偽の実行をゼロにする。
IHDPとZOZO Open Bandit(一様にランダムな真実を持つ実運用ログ)では、CIVeXはOracleの正しい実行と0.1pp以内で一致し、ネイティブなベースラインに対して、実行時の偽実行を>=50倍削減する。
論文 参考訳（メタデータ） (2026-05-09T21:06:15Z) - Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
SPECAは、明示的で分類されたセキュリティプロパティを自然言語仕様から導き出し、実装間で再利用する監査フレームワークである。
RepoAuditのベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化している。
Sherlock Fusaka Audit Contest(10のターゲット、366の応募)では、SPECAが専門家が強化した15の脆弱性をすべて回復し、4つの修正確認バグが浮上した。
論文 参考訳（メタデータ） (2026-04-29T09:57:07Z) - AnyPoC: Universal Proof-of-Concept Test Generation for Scalable LLM-Based Bug Detection [21.99631570872796]
我々は、AnyPoCという一般的なマルチエージェントフレームワークを紹介し、バグレポートを分析し、ファクトチェックする。
AnyPoCは真陽性のバグレポートに対して1.3倍有効なPoCを生成し、偽陽性のバグレポートの9.8倍を拒否する。
これまでにAnyPoCは122の新たなバグ(確認105、すでに86)を発見し、45の生成されたPoCを公式回帰テストとして採用している。
論文 参考訳（メタデータ） (2026-04-13T18:44:02Z) - DuET: Dual Execution for Test Output Prediction with Generated Code and Pseudocode [56.14374797825548]
よりエラー耐性の高い擬似コードに基づいて予測を行うLLMベースの擬似コード実行を提案する。
両手法を機能的多数決で組み合わせた二重実行フレームワークであるDuETを提案する。
LiveCodeBenchでは、DuETは最先端のパフォーマンスを実現し、Pass@1を13.6ppで改善した。
論文 参考訳（メタデータ） (2026-04-13T14:18:58Z) - Scaling Agentic Verifier for Competitive Coding [66.11758166379092]
大規模言語モデル(LLM)は強力なコーディング能力を示しているが、1回の試行で競合するプログラミング問題を正しく解くのに苦戦している。
実行ベースの再ランク付けは、有望なテスト時間スケーリング戦略を提供するが、既存のメソッドは、難しいテストケースの生成または非効率的なランダム入力サンプリングによって制約される。
本稿では,プログラムの動作を積極的に推論し,高い差別性のあるテスト入力を検索するエージェント検証手法を提案する。
論文 参考訳（メタデータ） (2026-02-04T06:30:40Z) - Arguzz: Testing zkVMs for Soundness and Completeness Bugs [4.015374459538631]
私たちは、zkVMの音質と完全性に関するバグをテストする最初の自動化ツールであるArguzzを紹介します。
VMに障害を注入することで、Arguzzは悪意のある、あるいはバグの多いプローバーを模倣し、過度に弱い制約を明らかにする。
論文 参考訳（メタデータ） (2025-09-13T14:36:49Z) - CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
$rm Csmall LEVER$は、リーンにおけるエンドツーエンドのコード生成のための161の問題を、高品質でキュレートしたベンチマークである。
それぞれの問題は、(1)堅実な仕様と一致する仕様を生成するタスク、(2)この仕様を確実に満足するリーン実装を生成するタスクで構成されています。
論文 参考訳（メタデータ） (2025-05-20T05:15:47Z) - GPT-HateCheck: Can LLMs Write Better Functional Tests for Hate Speech Detection? [50.53312866647302]
HateCheckは、合成データに対してきめ細かいモデル機能をテストするスイートである。
GPT-HateCheckは,スクラッチからより多彩で現実的な機能テストを生成するフレームワークである。
クラウドソースのアノテーションは、生成されたテストケースが高品質であることを示しています。
論文 参考訳（メタデータ） (2024-02-23T10:02:01Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。