文献

J-GLOBAL ID：202202266479489882   整理番号：22A0507989

SolType:固体性における算術オーバーフローのための精密化型【JST・京大機械翻訳】

SolType: refinement types for arithmetic overflow in solidity

著者 (5件)： Tan Bryan (University of California at Santa Barbara, USA) ,  Mariano Benjamin (University of Texas at Austin, USA) ,  Lahiri Shuvendu K. (Microsoft Research, USA) ,  Dillig Isil (University of Texas at Austin, USA) ,  Feng Yu (University of California at Santa Barbara, USA)
資料名： Proceedings of the ACM on Programming Languages  (Proceedings of the ACM on Programming Languages)
巻： 6  号： POPL  ページ： 1-29  発行年： 2022年 
JST資料番号： W5683A  ISSN： 2475-1421  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 金融取引におけるスマート契約利得の採用として,それらがバグとセキュリティ脆弱性がないということを確実にすることがますます重要になっている。この文脈における特別な関連性は,整数が,しばしば,バランスを考慮した金融資産を表現するために使われるので,算術オーバフローバグである。この観測によって動機づけられて,本論文は,スマート契約における演算過剰およびアンダーフローを防止するために使用できるSolidityのための精密化型システムであるSolタイプを提示した。ゾルタイプは,開発者が精密化型アノテーションを追加することを可能にし,演算が過剰およびアンダーフローをもたらさないことを証明するためにそれらを使用する。Solタイプは,複雑なデータ構造の整数値と凝集特性の間の関係を表現できる精密化項の豊富な語彙を組み込んだ。さらに,固体と呼ばれる実装は,タイプ推論エンジンを組み込み,非自明な契約不変量を含む有用なタイプアノテーションを自動的に推論できる。このタイプのシステムの有用性を評価するために,合計120のスマート契約の算術安全性を証明するために,固体を使用した。完全自動化モード(すなわち,固体型推論能力を用いる)で使用するとき,固体は,オーバフローに対して保護するために使用する冗長なランタイムチェックの86.3%を除去できる。また,VeriSmartと呼ばれる最先端の算術安全検証者に対する固体を比較し,固体が有意に低い偽陽性率を持ち,一方,検証時間に関してかなり速いことを示した。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 凝集 ,  冗長性 ,  データ構造 ,  演算 ,  金融 ,  語彙 ,  利得 ,  不変量 ,  精密化 ,  ソフトウェア障害 ,  オーバフロー ,  セキュリティ ,  型推論 ,  *アノテーション
準シソーラス用語： 型システム , 【Automatic Indexing@JST】

著者キーワード (3件)： 整数オーバフロー ,  精密化型推論 ,  スマート契約

分類 (2件)： データ保護  (JD01020V) ,  計算機システム開発  (JD02010R)

タイトルに関連する用語 (4件)： 固体 ,  算術 ,  オーバーフロー ,  精密化