論文の概要: Safety Verification of Declarative Smart Contracts

• arxiv url: http://arxiv.org/abs/2211.14585v3
• Date: Wed, 2 Aug 2023 09:43:06 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-24 14:08:06.900145
• Title: Safety Verification of Declarative Smart Contracts
• Title（参考訳）: 宣言的スマートコントラクトの安全性検証
• Authors: Haoxian Chen, Lan Lu, Brendan Massey, Yuepeng Wang, Boon Thau Loo
• Abstract要約: 本稿では,DeCon で記述された宣言型スマートコントラクトを対象とした自動安全検証ツール DCV を提案する。 20のベンチマークコントラクトに対する評価は,DCVがパブリックリポジトリから適応したスマートコントラクトの検証に有効であることを示し,他のツールがサポートしていないコントラクトの検証が可能であることを示唆している。
• 参考スコア（独自算出の注目度）: 4.303272418564008
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Smart contracts manage a large number of digital assets nowadays. Bugs in these contracts have led to significant financial loss. Verifying the correctness of smart contracts is, therefore, an important task. This paper presents an automated safety verification tool, DCV, that targets declarative smart contracts written in DeCon, a logic-based domain-specific language for smart contract implementation and specification. DCV proves safety properties by mathematical induction and can automatically infer inductive invariants using heuristic patterns, without annotations from the developer. Our evaluation on 20 benchmark contracts shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools. Furthermore, DCV significantly outperforms baseline tools in verification time.
• Abstract（参考訳）: smart contractsは近年、多数のデジタル資産を管理している。 これらの契約のバグは大きな損失をもたらした。 スマートコントラクトの正しさを検証することは重要なタスクである。 本稿では,スマートコントラクトの実装と仕様のためのロジックベースのドメイン固有言語であるdeconで記述された宣言型スマートコントラクトを対象とする,自動安全検証ツールdcvを提案する。 DCVは、数学的誘導によって安全性を証明し、開発者からのアノテーションなしでヒューリスティックパターンを用いて誘導不変性を自動推論することができる。 20のベンチマークコントラクトに対する評価では,DCVはパブリックリポジトリから適応したスマートコントラクトの検証に有効であり,他のツールがサポートしていないコントラクトの検証が可能である。 さらに、DCVは検証時間においてベースラインツールを著しく上回る。

関連論文リスト

• Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
  Code-Development Benchmark (Codev-Bench)は、細粒度で現実世界、リポジトリレベル、開発者中心の評価フレームワークです。 Codev-Agentは、リポジトリのクローリングを自動化し、実行環境を構築し、既存のユニットテストから動的呼び出しチェーンを抽出し、データ漏洩を避けるために新しいテストサンプルを生成するエージェントベースのシステムである。
  論文  参考訳（メタデータ） (2024-10-02T09:11:10Z)
• Versioned Analysis of Software Quality Indicators and Self-admitted Technical Debt in Ethereum Smart Contracts with Ethstractor [2.052808596154225]
  本稿では、バージョン管理されたスマートコントラクトのデータセットを収集する最初のスマートコントラクト収集ツールであるEthstractorを提案する。 収集されたデータセットは、スマートコントラクトの脆弱性の指標として、コードメトリクスの信頼性を評価するために使用される。
  論文  参考訳（メタデータ） (2024-07-22T18:27:29Z)
• Effective Targeted Testing of Smart Contracts [0.0]
  スマートコントラクトは不変であるため、バグを修正することはできない。 我々のフレームワークであるGriffinは、テストデータを生成するためにターゲットとなるシンボル実行技術を用いて、この欠陥に対処する。 本稿では、スマートコントラクトがターゲットとなるシンボル実行におけるレガシーソフトウェアとどのように異なるのか、そしてこれらの違いがツール構造に与える影響について論じる。
  論文  参考訳（メタデータ） (2024-07-05T04:38:11Z)
• Solvent: liquidity verification of smart contracts [2.680854115314008]
  スマートコントラクト検証ツールの現在の制限は、暗号資産の交換に関する流動性特性の表現と検証に効果がないことである。 我々は,これらの特性の検証を目的とした溶剤について提案する。これは,Solidityの既存の検証ツールの範囲を超えている。
  論文  参考訳（メタデータ） (2024-04-27T10:54:50Z)
• Vulnerabilities of smart contracts and mitigation schemes: A Comprehensive Survey [0.6554326244334866]
  本稿では,開発者がセキュアなスマート技術を開発するのを支援することを目的とした,文献レビューと実験報告を組み合わせる。 頻繁な脆弱性とそれに対応する緩和ソリューションのリストを提供する。 サンプルのスマートコントラクト上でそれらを実行し、テストすることで、コミュニティが最も広く使用しているツールを評価します。
  論文  参考訳（メタデータ） (2024-03-28T19:36:53Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Automated Invariant Generation for Solidity Smart Contracts [2.4181711081104282]
  本稿では,Solidityスマートコントラクトのための新しい不変生成フレームワークINVCON+を提案する。 INVCON+は既存の不変検出器であるInvConを拡張して、検証された契約不変量を自動生成する。 我々は、361 ERC20と10 ERC721実世界の契約と、一般的なERC20脆弱性ベンチマークに基づいてINVCON+を評価する。
  論文  参考訳（メタデータ） (2024-01-01T03:37:30Z)
• Formally Verifying a Real World Smart Contract [52.30656867727018]
  われわれは、Solidityの最新バージョンで書かれた現実世界のスマートコントラクトを正式に検証できるツールを検索する。 本稿では,最近のSolidityで書かれた実世界のスマートコントラクトを正式に検証できるツールについて紹介する。
  論文  参考訳（メタデータ） (2023-07-05T14:30:21Z)
• Detecting Logical Relation In Contract Clauses [94.85352502638081]
  契約における節間の論理的関係の抽出を自動化する手法を開発する。 結果として得られたアプローチは、コントラクト作者が節間の潜在的な論理的衝突を検出するのに役立つだろう。
  論文  参考訳（メタデータ） (2021-11-02T19:26:32Z)
• Exploring Robustness of Unsupervised Domain Adaptation in Semantic Segmentation [74.05906222376608]
  クリーンな画像とそれらの逆の例との一致を、出力空間における対照的な損失によって最大化する、逆向きの自己スーパービジョンUDA(ASSUDA)を提案する。 i) セマンティックセグメンテーションにおけるUDA手法のロバスト性は未解明のままであり, (ii) 一般的に自己スーパービジョン(回転やジグソーなど) は分類や認識などのイメージタスクに有効であるが, セグメンテーションタスクの識別的表現を学習する重要な監視信号の提供には失敗している。
  論文  参考訳（メタデータ） (2021-05-23T01:50:44Z)
• 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)

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

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