論文の概要: Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for Smart Contract Transactions
- arxiv url: http://arxiv.org/abs/2408.06478v1
- Date: Mon, 12 Aug 2024 20:27:41 GMT
- ステータス: 処理完了
- システム内更新日: 2024-08-14 19:17:34.802765
- Title: Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for Smart Contract Transactions
- Title（参考訳）: Theorem-Carrying-Transaction: スマートコントラクトトランザクションの安全性を保証するランタイム認証
- Authors: Nikolaj S. Bjørner, Ashley J. Chen, Shuo Chen, Yang Chen, Zhongxin Guo, Tzu-Han Hsu, Peng Liu, Nanqing Luo,
- Abstract要約: 我々は、この野心的な目標に向けて、コミュニティに実行可能な技術ロードマップを提示します。
我々の技術はTheorem-Carrying-Transaction (TCT)と呼ばれ、具体的実行と記号的証明の利点を組み合わせたものです。
我々のプロトタイプは、最先端のアプローチよりも2桁低い、無視可能なランタイムオーバーヘッドを発生させます。
- 参考スコア（独自算出の注目度）: 8.32630869646569
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Security bugs and trapdoors in smart contracts have been impacting the Ethereum community since its inception. Conceptually, the 1.45-million Ethereum's contracts form a single "gigantic program" whose behaviors are determined by the complex reference-topology between the contracts. Can the Ethereum community be assured that this gigantic program conforms to its design-level safety properties, despite unforeseeable code-level intricacies? Static code verification is inadequate due to the program's gigantic scale and high polymorphism. In this paper, we present a viable technological roadmap for the community toward this ambitious goal. Our technology, called Theorem-Carrying-Transaction (TCT), combines the benefits of concrete execution and symbolic proofs. Under the TCT protocol, every transaction carries a theorem that proves its adherence to the specified properties in the invoked contracts, and the runtime system checks the theorem before executing the transaction. Once a property is specified in a contract, it can be treated confidently as an unconditional guarantee made by the contract. As case studies, we demonstrate that TCT secures token contracts without foreseeing code-level intricacies like integer overflow and reentrancy. TCT is also successfully applied to a Uniswap codebase, showcasing a complex decentralized finance (DeFi) scenario. Our prototype incurs a negligible runtime overhead, two orders of magnitude lower than a state-of-the-art approach.
- Abstract（参考訳）: スマートコントラクトのセキュリティバグとトラップドアがEthereumコミュニティに影響を与えている。
概念的には、1.45億ドルのEthereumの契約は、契約間の複雑な参照トポロジーによって振舞いが決定される単一の「巨大プログラム」を形成する。
Ethereumコミュニティは、この巨大なプログラムが、予期せぬコードレベルの複雑さにもかかわらず、設計レベルの安全性特性に準拠していることを保証することができるだろうか?
静的コード検証は、プログラムの巨大スケールと高い多型のために不十分である。
本稿では、この野心的な目標に向けて、コミュニティに実行可能な技術ロードマップを提示する。
我々の技術はTheorem-Carrying-Transaction (TCT)と呼ばれ、具体的実行と記号的証明の利点を組み合わせたものです。
TCTプロトコルの下では、全てのトランザクションは呼び出したコントラクトの特定のプロパティへの準拠を証明する定理を持ち、ランタイムシステムはトランザクションを実行する前にその定理をチェックする。
一度契約でプロパティが特定されると、契約によってなされる無条件保証として確実に扱われる。
ケーススタディでは,TTTが整数オーバーフローや再帰といったコードレベルの複雑さを予見することなく,トークン契約を保証していることを示す。
TCTはUnixwapのコードベースにもうまく適用されており、複雑な分散金融(DeFi)シナリオを示している。
我々のプロトタイプは、最先端のアプローチよりも2桁低い、無視可能なランタイムオーバーヘッドを発生させます。
関連論文リスト
- Effective Targeted Testing of Smart Contracts [0.0]
スマートコントラクトは不変であるため、バグを修正することはできない。
我々のフレームワークであるGriffinは、テストデータを生成するためにターゲットとなるシンボル実行技術を用いて、この欠陥に対処する。
本稿では、スマートコントラクトがターゲットとなるシンボル実行におけるレガシーソフトウェアとどのように異なるのか、そしてこれらの違いがツール構造に与える影響について論じる。
論文 参考訳（メタデータ） (2024-07-05T04:38:11Z) - Scalable UTXO Smart Contracts via Fine-Grained Distributed State [0.8192907805418581]
UTXOベースのスマートコントラクトプラットフォームは、効率のボトルネックに直面している。
コントラクトに送信されるすべてのトランザクションは、更新されたコントラクト状態全体を指定する必要があります。
本稿では,拡張UTXOブロックチェーン上でのスマートコントラクトの効率的な実行手法を提案する。
論文 参考訳（メタデータ） (2024-06-11T20:28:27Z) - Specification Mining for Smart Contracts with Trace Slicing and Predicate Abstraction [10.723903783651537]
過去の取引履歴から契約仕様を推測するための仕様マイニング手法を提案する。
提案手法は,トランザクション履歴から統計的に推測されるプログラム不変量とともに,関数呼び出しの高レベルな挙動自動化を導出する。
論文 参考訳（メタデータ） (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) - Automated Invariant Generation for Solidity Smart Contracts [2.4181711081104282]
本稿では,Solidityスマートコントラクトのための新しい不変生成フレームワークINVCON+を提案する。
INVCON+は既存の不変検出器であるInvConを拡張して、検証された契約不変量を自動生成する。
我々は、361 ERC20と10 ERC721実世界の契約と、一般的なERC20脆弱性ベンチマークに基づいてINVCON+を評価する。
論文 参考訳（メタデータ） (2024-01-01T03:37:30Z) - Blockchain Smart Contract Threat Detection Technology Based on Symbolic
Execution [0.0]
永続性の脆弱性は隠蔽され複雑であり、スマートコントラクトに大きな脅威をもたらす。
本稿では,シンボル実行に基づくスマートコントラクト脅威検出技術を提案する。
実験の結果,本手法は検出効率と精度の両方を著しく向上させることがわかった。
論文 参考訳（メタデータ） (2023-12-24T03:27:03Z) - Formally Verifying a Real World Smart Contract [52.30656867727018]
われわれは、Solidityの最新バージョンで書かれた現実世界のスマートコントラクトを正式に検証できるツールを検索する。
本稿では,最近のSolidityで書かれた実世界のスマートコントラクトを正式に検証できるツールについて紹介する。
論文 参考訳（メタデータ） (2023-07-05T14:30:21Z) - Blockchain Large Language Models [65.7726590159576]
本稿では,異常なブロックチェーントランザクションを検出するための動的,リアルタイムなアプローチを提案する。
提案するツールであるBlockGPTは、ブロックチェーンアクティビティのトレース表現を生成し、大規模な言語モデルをスクラッチからトレーニングして、リアルタイム侵入検出システムとして機能させる。
論文 参考訳（メタデータ） (2023-04-25T11:56:18Z) - Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。
我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文 参考訳（メタデータ） (2022-03-03T10:07: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) - Quantum copy-protection of compute-and-compare programs in the quantum random oracle model [48.94443749859216]
計算・比較プログラム(Computer-and-compare program)として知られる回避関数のクラスに対する量子コピー保護スキームを導入する。
我々は,量子乱数オラクルモデル(QROM)において,完全悪意のある敵に対する非自明なセキュリティを実現することを証明した。
補完的な結果として、「セキュアソフトウェアリース」という,ソフトウェア保護の概念の弱さが示される。
論文 参考訳（メタデータ） (2020-09-29T08:41:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。