Coqにおける分散交換の形式化【JST・京大機械翻訳】

Nielsen Eske Hoy; Annenkov Danil; Spitters Bas

プレプリント

J-GLOBAL ID：202202219798610534 整理番号：22P0304666

Coqにおける分散交換の形式化【JST・京大機械翻訳】

Formalising Decentralised Exchanges in Coq

出版者サイト {{ this.onShowPLink() }} 複写サービスで全文入手
高度な検索・分析はJDreamⅢで

この文献はプレプリントです。プレプリントについてはこちらをご確認ください。

著者 (3件)： , ,
資料名：
発行年： 2022年03月11日プレプリントサーバーでの情報更新日： 2022年03月11日
JST資料番号： O7000B 資料種別：プレプリント
記事区分：プレプリント発行国：アメリカ合衆国 (USA) 言語：英語 (EN)

攻撃と事故の個数は,停留の重大な損失につながる。連鎖分解によると,2021年には,約14億ドルが様々な事故により失われ,この数は分散Finance(DeFi)アプリケーションによって支配されている。これらの問題に取り組むために,1つは監査から形式的方法までのツールの収集を用いることができる。形式的検証を用いて,契約相互作用を捕捉する基礎証明支援におけるDeFi契約の最初の形式化を提供した。著者らは,EthereumのUniswapに類似したTezosネットワークのための分散的非-custodial交換であるDexter2に焦点を当てた。Dexter実装はいくつかのスマート契約から成る。これは,複雑な契約相互作用による形式化のユニークな挑戦である。定式化は,Dexterの実装に含まれる契約に対する非公式仕様に関する機能的正当性の証明を含む。さらに,著者らの定式化は,分散交換の相互作用スマート契約の安全特性の証明の最初の特徴である。CoqからCameLIGOコードへの契約を抽出し,Tezosブロックチェーンに展開できる。UniswapとDexterは,類似の契約の収集のためのパラダイムである。このように,著者らの方法論は,類似の相互作用パターンを特徴とするDeFiアプリケーションを実装し,検証することを可能にする。【JST・京大機械翻訳】

, , , , , , ,
, , 【Automatic Indexing@JST】

計算機システム開発 , 計算機網 , データ保護

前のページに戻る