論文の概要: Automated Invariant Generation for Solidity Smart Contracts

• arxiv url: http://arxiv.org/abs/2401.00650v1
• Date: Mon, 1 Jan 2024 03:37:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-01-03 16:34:41.678275
• Title: Automated Invariant Generation for Solidity Smart Contracts
• Title（参考訳）: 固体スマートコントラクトの自動不変生成
• Authors: Ye Liu, Chengxuan Zhang, Yi Li. (Nanyang Technological University, Singapore)
• Abstract要約: 本稿では,Solidityスマートコントラクトのための新しい不変生成フレームワークINVCON+を提案する。 INVCON+は既存の不変検出器であるInvConを拡張して、検証された契約不変量を自動生成する。 我々は、361 ERC20と10 ERC721実世界の契約と、一般的なERC20脆弱性ベンチマークに基づいてINVCON+を評価する。
• 参考スコア（独自算出の注目度）: 2.4181711081104282
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Smart contracts are computer programs running on blockchains to automate the transaction execution between users. The absence of contract specifications poses a real challenge to the correctness verification of smart contracts. Program invariants are properties that are always preserved throughout the execution, which characterize an important aspect of the program behaviors. In this paper, we propose a novel invariant generation framework, INVCON+, for Solidity smart contracts. INVCON+ extends the existing invariant detector, InvCon, to automatically produce verified contract invariants based on both dynamic inference and static verification. Unlike INVCON+, InvCon only produces likely invariants, which have a high probability to hold, yet are still not verified against the contract code. Particularly, INVCON+ is able to infer more expressive invariants that capture richer semantic relations of contract code. We evaluate INVCON+ on 361 ERC20 and 10 ERC721 real-world contracts, as well as common ERC20 vulnerability benchmarks. The experimental results indicate that INVCON+ efficiently produces high-quality invariant specifications, which can be used to secure smart contracts from common vulnerabilities.
• Abstract（参考訳）: スマートコントラクトは、ユーザ間のトランザクション実行を自動化するためにブロックチェーン上で動作するコンピュータプログラムである。 コントラクト仕様の欠如は、スマートコントラクトの正当性検証に真の課題をもたらします。 プログラム不変量は実行中に常に保存されるプロパティであり、プログラムの振る舞いの重要な側面を特徴付ける。 本稿では,Solidityスマートコントラクトのための新しい不変生成フレームワークINVCON+を提案する。 INVCON+は既存の不変検出器であるInvConを拡張し、動的推論と静的検証の両方に基づいて検証された契約不変量を自動生成する。 INVCON+と異なり、InvConは高い確率で保持できる可能性のある不変量しか生成しないが、まだ契約コードに対して検証されていない。 特に、INVCON+は、より表現力のある不変性を推論することができ、契約コードのより豊かな意味関係を捉えることができる。 我々は、361 ERC20と10 ERC721実世界の契約と、一般的なERC20脆弱性ベンチマークに基づいてINVCON+を評価する。 実験結果から,INVCON+は,共通脆弱性からスマートコントラクトを確保するために,高品質な不変仕様を効率よく生成できることが示唆された。

関連論文リスト

• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  コード補完モデルによって生成されたSolidityスマートコントラクトの機能的正しさを評価するベンチマークであるSolBenchを紹介する。 本稿では,スマートコントラクトの機能的正当性を検証するための検索拡張コード修復フレームワークを提案する。 その結果、コード修復と検索技術は、計算コストを削減しつつ、スマートコントラクト完了の正しさを効果的に向上することを示した。
  論文  参考訳（メタデータ） (2025-03-03T01:55:20Z)
• SmartInv: Multimodal Learning for Smart Contract Invariant Inference [10.468390413756863]
  We present SmartInv, a accurate and fast smart contract invariant inference framework。 私たちの重要な洞察は、スマートコントラクトの期待される振る舞いは、マルチモーダル情報に対する理解と推論に依存している、ということです。 SmartInvを実世界の契約で評価し、数百万ドルの損失をもたらしたバグを再発見しました。
  論文  参考訳（メタデータ） (2024-11-14T06:28:57Z)
• Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
  Code-Development Benchmark (Codev-Bench)は、細粒度で現実世界、リポジトリレベル、開発者中心の評価フレームワークです。 Codev-Agentは、リポジトリのクローリングを自動化し、実行環境を構築し、既存のユニットテストから動的呼び出しチェーンを抽出し、データ漏洩を避けるために新しいテストサンプルを生成するエージェントベースのシステムである。
  論文  参考訳（メタデータ） (2024-10-02T09:11:10Z)
• Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for Smart Contract Transactions [8.32630869646569]
  我々は、この野心的な目標に向けて、コミュニティに実行可能な技術ロードマップを提示します。 我々の技術はTheorem-Carrying-Transaction (TCT)と呼ばれ、具体的実行と記号的証明の利点を組み合わせたものです。 我々のプロトタイプは、最先端のアプローチよりも2桁低い、無視可能なランタイムオーバーヘッドを発生させます。
  論文  参考訳（メタデータ） (2024-08-12T20:27:41Z)
• Effective Targeted Testing of Smart Contracts [0.0]
  スマートコントラクトは不変であるため、バグを修正することはできない。 我々のフレームワークであるGriffinは、テストデータを生成するためにターゲットとなるシンボル実行技術を用いて、この欠陥に対処する。 本稿では、スマートコントラクトがターゲットとなるシンボル実行におけるレガシーソフトウェアとどのように異なるのか、そしてこれらの違いがツール構造に与える影響について論じる。
  論文  参考訳（メタデータ） (2024-07-05T04:38:11Z)
• Specification Mining for Smart Contracts with Trace Slicing and Predicate Abstraction [10.723903783651537]
  過去の取引履歴から契約仕様を推測するための仕様マイニング手法を提案する。 提案手法は,トランザクション履歴から統計的に推測されるプログラム不変量を伴って,関数呼び出しの高レベルな振る舞い自動を導出する。 SMCONは、高いコードカバレッジと最大56%のスピードアップを達成するためのスマートコントラクトのシンボリック分析を強化するために、合理的に正確な仕様をマイニングしている。
  論文  参考訳（メタデータ） (2024-03-20T03:39:51Z)
• Contract Usage and Evolution in Android Mobile Applications [45.44831696628473]
  JavaやKotlinで記述されたAndroidアプリケーションにおけるコントラクトの存在と使用に関する,最初の大規模な実証的研究を紹介する。 F-Droidリポジトリから2,390のAndroidアプリケーションを解析し,51,749 KLOC以上を処理した。 私たちの発見は、JavaとKotlinでコントラクト仕様を標準化するライブラリを持つことが望ましいことを示しています。
  論文  参考訳（メタデータ） (2024-01-25T15:36:49Z)
• Formally Verifying a Real World Smart Contract [52.30656867727018]
  われわれは、Solidityの最新バージョンで書かれた現実世界のスマートコントラクトを正式に検証できるツールを検索する。 本稿では,最近のSolidityで書かれた実世界のスマートコントラクトを正式に検証できるツールについて紹介する。
  論文  参考訳（メタデータ） (2023-07-05T14:30:21Z)
• Enhancing Smart Contract Security Analysis with Execution Property Graphs [48.31617821205042]
  ランタイム仮想マシン用に特別に設計された動的解析フレームワークであるClueを紹介する。 Clueは契約実行中に重要な情報をキャプチャし、新しいグラフベースの表現であるExecution Property Graphを使用する。 評価結果から, クリューの真正率, 偽正率の低い優れた性能が, 最先端のツールよりも優れていた。
  論文  参考訳（メタデータ） (2023-05-23T13:16:42Z)
• Toward Adversarial Training on Contextualized Language Representation [78.39805974043321]
  本稿では, PLMエンコーダが出力する文脈化言語表現の観点から, 対人訓練(AT)について検討する。 そこで我々は, テキストコンテキスト適応型表現-逆訓練(CreAT)を提案し, 攻撃を明示的に最適化し, エンコーダの文脈化表現を逸脱させる。 CreATは幅広いタスクで一貫したパフォーマンス向上を実現しており、エンコーダ部分のみを下流タスクに保持する言語事前トレーニングに有効であることが証明されている。
  論文  参考訳（メタデータ） (2023-05-08T08:56:51Z)
• Safety Verification of Declarative Smart Contracts [4.303272418564008]
  本稿では,DeCon で記述された宣言型スマートコントラクトを対象とした自動安全検証ツール DCV を提案する。 20のベンチマークコントラクトに対する評価は,DCVがパブリックリポジトリから適応したスマートコントラクトの検証に有効であることを示し,他のツールがサポートしていないコントラクトの検証が可能であることを示唆している。
  論文  参考訳（メタデータ） (2022-11-26T15:02:37Z)
• ContrastVAE: Contrastive Variational AutoEncoder for Sequential Recommendation [58.02630582309427]
  本稿では,コントラスト学習を変分オートエンコーダの枠組みに組み込むことを提案する。 ContrastELBOは,従来のシングルビューELBOを2ビューケースに拡張した,新しいトレーニング目標である。 また、コントラストELBOの具体化として、コントラスト正規化を備えた2分岐VAEモデルであるContrastVAEを提案する。
  論文  参考訳（メタデータ） (2022-08-27T03:35:00Z)
• Speculative Decoding: Exploiting Speculative Execution for Accelerating Seq2seq Generation [80.2267931231335]
  本稿では,自己回帰(AR)デコーディングを高速化する投機的実行のアイデアを活用するための投機的デコーディング(SpecDec)を提案する。 SpecDecには2つのイノベーションがある。Spec-Drafter - 効率的なドラフトのために特別に最適化された独立モデル、Spec-Verification - ドラフトされたトークンを効率的に検証するための信頼性の高い方法である。
  論文  参考訳（メタデータ） (2022-03-30T17:27:09Z)
• HCC: A Language-Independent Hardening Contract Compiler for Smart Contracts [5.379572824182189]
  我々は,HCCと呼ばれる,最初の実用的なスマートコントラクトコンパイラを提案する。 HCCは、新しい言語に依存しないコードプロパティグラフ(CPG)の表記に基づいて、ソースコードレベルでのセキュリティ強化チェックを挿入する。
  論文  参考訳（メタデータ） (2022-03-01T11:25:32Z)
• ESCORT: Ethereum Smart COntRacTs Vulnerability Detection using Deep Neural Network and Transfer Learning [80.85273827468063]
  既存の機械学習ベースの脆弱性検出方法は制限され、スマートコントラクトが脆弱かどうかのみ検査される。 スマートコントラクトのための初のDeep Neural Network(DNN)ベースの脆弱性検出フレームワークであるESCORTを提案する。 ESCORTは6種類の脆弱性に対して平均95%のF1スコアを達成し,検出時間は契約あたり0.02秒であることを示す。
  論文  参考訳（メタデータ） (2021-03-23T15:04:44Z)
• Profiling Gas Consumption in Solidity Smart Contracts [3.0378875015087567]
  本稿では,ガス消費の観点から,スマートコントラクトのコード品質を静的に評価するためのメトリクススイートであるGasMetを提案する。 2,186のスマートコントラクトを含む実験では、提案されたメトリクスがデプロイメントコストと直接関連していることが示されている。
  論文  参考訳（メタデータ） (2020-08-12T17:26:55Z)

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

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