Fugu-MT 論文翻訳(概要): HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types

論文の概要: HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types

arxiv url: http://arxiv.org/abs/2108.12971v1
Date: Mon, 30 Aug 2021 03:02:37 GMT
ステータス: 処理完了
システム内更新日: 2021-08-31 21:33:19.722900
Title: HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types
Title（参考訳）: helmholtz: 改良型に基づいたtezosスマートコントラクトの検証ツール
Authors: Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, Kohei Suenaga, Atsushi Igarashi
Abstract要約: スマートコントラクト(Smart Contract)は、多くの暗号通貨を実装したブロックチェーン上で実行されるプログラムで、トランザクションの自動化に使用されている。この記事では、Mchelsonの型ベースの静的検証ツールHELMHOLTZについて説明する。
参考スコア（独自算出の注目度）: 2.1550839871882017
License: http://creativecommons.org/licenses/by/4.0/
Abstract: A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them. This article describes our type-based static verification tool HELMHOLTZ for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. HELMHOLTZ is designed on top of our extension of Michelson's type system with refinement types. HELMHOLTZ takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. \HELMHOLTZ{} successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.
Abstract（参考訳）: スマートコントラクト(Smart Contract)は、多くの暗号通貨を実装したブロックチェーン上で実行されるプログラムで、トランザクションの自動化に使用されている。スマートコントラクトが処理する金額が膨大であるため,静的かつ形式的に検証可能なメソッドの要求が急増している。この記事では、ブロックチェーンプラットフォームTezosで実行されるスマートコントラクトを記述するための静的型付けスタックベースの言語であるMichelson用の型ベースの静的検証ツールHELMHOLTZについて説明する。 HELMHOLTZは、Michelsonの型システムを改良した拡張の上に設計されている。 HELMHOLTZは、ユーザ定義仕様を入力として洗練型形式で記述したMichelsonプログラムを入力として、精製型システムに基づいてプログラムをタイプチェックし、SMTソルバZ3で生成された検証条件を出力する。我々は,ミシェルソンのコア計算用ミニミシェルソンに対して,複合データ型(リストとペアなど)や高次関数,他のコントラクトの呼び出しといった特徴を取り入れた改良型システムについて,簡単に紹介する。 HELMHOLTZ{}は、口座に送金し、デジタル署名をチェックするものを含む、いくつかの実用的なMichelsonプログラムの検証に成功した。

関連論文リスト

Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for Smart Contract Transactions [8.32630869646569]
我々は、この野心的な目標に向けて、コミュニティに実行可能な技術ロードマップを提示します。我々の技術はTheorem-Carrying-Transaction (TCT)と呼ばれ、具体的実行と記号的証明の利点を組み合わせたものです。我々のプロトタイプは、最先端のアプローチよりも2桁低い、無視可能なランタイムオーバーヘッドを発生させます。
論文参考訳（メタデータ） (2024-08-12T20:27:41Z)
Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
不確実性定量化(英: Uncertainty Quantification、UQ)は、機械学習(ML)アプリケーションにおいて重要なコンポーネントである。最新のUQベースラインの集合を実装した新しいベンチマークを導入する。我々は、9つのタスクにわたるUQと正規化技術に関する大規模な実証的研究を行い、最も有望なアプローチを特定した。
論文参考訳（メタデータ） (2024-06-21T20:06:31Z)
Specification Mining for Smart Contracts with Trace Slicing and Predicate Abstraction [10.723903783651537]
過去の取引履歴から契約仕様を推測するための仕様マイニング手法を提案する。提案手法は,トランザクション履歴から統計的に推測されるプログラム不変量とともに,関数呼び出しの高レベルな挙動自動化を導出する。
論文参考訳（メタデータ） (2024-03-20T03:39:51Z)
Multi-Candidate Speculative Decoding [82.05519287513444]
大規模な言語モデルは、様々なNLPタスクで印象的な機能を示してきたが、その生成は自動回帰的に時間を要する。これは高速なドラフトモデルから候補セグメントを生成し、ターゲットモデルによって並列に検証する。本稿では,複数の候補をドラフトモデルから抽出し,検証のためにバッチにまとめる手法を提案する。対象モデルの分布を維持しつつ,効率的な多候補検証のためのアルゴリズムを設計する。
論文参考訳（メタデータ） (2024-01-12T17:15:23Z)
Which Syntactic Capabilities Are Statistically Learned by Masked Language Models for Code? [51.29970742152668]
精度に基づく測定に依存することで、モデルの能力が過大評価される可能性があることを強調する。これらの問題に対処するために,SyntaxEval in Syntactic Capabilitiesというテクニックを導入する。
論文参考訳（メタデータ） (2024-01-03T02:44:02Z)
Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文参考訳（メタデータ） (2023-09-25T15:42:18Z)
Hot or Cold? Adaptive Temperature Sampling for Code Generation with Large Language Models [54.72004797421481]
コード生成に特化したデコード戦略を検討するために、最初の体系的な研究を行う。以上の知見に触発されて,適応温度(AdapT)サンプリング法を提案する。その結果,AdapTサンプリングは最先端の復号化戦略を著しく上回っていることがわかった。
論文参考訳（メタデータ） (2023-09-06T06:27:33Z)
SigRec: Automatic Recovery of Function Signatures in Smart Contracts [40.20115707680234]
デバッグ情報も型情報もバイトコードには存在しないため、コントラクトバイトコードから関数シグネチャを復元することは難しい。我々は,ソースコードや関数シグネチャデータベースを必要とせずに,コントラクトバイトコードから関数シグネチャを復元する新しいツールであるSigRecを開発した。
論文参考訳（メタデータ） (2023-05-11T18:03:39Z)
TypeT5: Seq2seq Type Inference using Static Analysis [51.153089609654174]
本稿では,型予測をコード入力タスクとして扱う新しい型推論手法を提案する。本手法では静的解析を用いて,型シグネチャがモデルによって予測されるコード要素毎に動的コンテキストを構築する。また,モデルの入力コンテキストに事前の型予測を組み込んだ反復復号方式を提案する。
論文参考訳（メタデータ） (2023-03-16T23:48:00Z)
A formal model for ledger management systems based on contracts and temporal logic [0.0]
台帳のような第2世代のブロックチェーンは、スマートコントラクトと結合される。任意のプログラミング構造としてのスマートコントラクトの現在の実装は、危険なバグを受けやすいものにしている。本稿では,有限状態オートマトンとしてモデル化された契約の概念を形式化し,データベースの分割と信頼性の回復を提案する。
論文参考訳（メタデータ） (2021-09-30T15:34:28Z)
A Bytecode-based Approach for Smart Contract Classification [10.483992071557195]
ブロックチェーンプラットフォームにデプロイされるスマートコントラクトの数は指数関数的に増えているため、ユーザは手動のスクリーニングによって望ましいサービスを見つけることが難しくなっている。スマートコントラクト分類に関する最近の研究は、契約ソースコードに基づく自然言語処理(NLP)ソリューションに焦点を当てている。本稿では,これらの問題を解決するために,ソースコードの代わりにコントラクトバイトコードの特徴に基づく分類モデルを提案する。
論文参考訳（メタデータ） (2021-05-31T03:00:29Z)

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

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