論文の概要: Bithoven: Formal Safety for Expressive Bitcoin Smart Contracts

• arxiv url: http://arxiv.org/abs/2601.01436v1
• Date: Sun, 04 Jan 2026 08:48:34 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-06 16:25:22.346689
• Title: Bithoven: Formal Safety for Expressive Bitcoin Smart Contracts
• Title（参考訳）: Bithoven: 表現力のあるBitcoinスマートコントラクトの形式的安全性
• Authors: Hyunhum Cho, Ik Rae Jeong,
• Abstract要約: 本稿では,表現性と形式的安全性のギャップを埋めるための高水準言語Bithovenを紹介する。 厳密な型チェッカーとリソースのライブネスアナライザとセマンティックコントロールフローアナライザを統合することで、Bithovenはコンセンサスとロジックの欠陥の主要なカテゴリを排除している。
• 参考スコア（独自算出の注目度）: 0.6187780920448871
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The rigorous security model of Bitcoin's UTXO architecture often comes at the cost of developer usability, forcing a reliance on manual stack manipulation that leads to critical financial vulnerabilities like signature malleability, unspendable states and unconstrained execution paths. Industry standards such as Miniscript provide necessary abstractions for policy verification but do not model the full imperative logic required for complex contracts, leaving gaps in state management and resource liveness. This paper introduces Bithoven, a high-level language designed to bridge the gap between expressiveness and formal safety. By integrating a strict type checker and a resource liveness analyzer with a semantic control-flow analyzer, Bithoven eliminates major categories of consensus and logic defects defined in our fault model prior to deployment. Our results indicate that this safety comes at modest cost: Bithoven compiles to Bitcoin Script with efficiency comparable to hand-optimized code, demonstrating that type-safe, developer-friendly abstractions are viable even within the strict byte-size constraints of the Bitcoin blockchain.
• Abstract（参考訳）: BitcoinのUTXOアーキテクチャの厳格なセキュリティモデルは、しばしば開発者の使いやすさの犠牲となり、手動のスタック操作に頼らざるを得ない。 Miniscriptのような業界標準は、ポリシー検証に必要な抽象化を提供するが、複雑な契約に必要な完全な命令ロジックをモデル化せず、状態管理とリソースの活力にギャップを残している。 本稿では,表現性と形式的安全性のギャップを埋めるための高水準言語Bithovenを紹介する。 厳密な型チェッカーとリソースのライブネスアナライザとセマンティックコントロールフローアナライザを統合することで、Bithovenはデプロイメント前に私たちのフォールトモデルで定義されたコンセンサスとロジックの欠陥の主要なカテゴリを排除します。 Bithovenは手動で最適化されたコードに匹敵する効率でBitcoin Scriptにコンパイルし、型安全で開発者フレンドリな抽象化が、Bitcoinブロックチェーンの厳格なバイトサイズの制約の中でも実現可能であることを実証します。

関連論文リスト

• Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
  Etherscanの78,047,845のスマートコントラクトがデプロイされているにも関わらず(2025年5月26日現在)、わずか767,520 (1%)がオープンソースである。 この不透明さは、オンチェーンスマートコントラクトバイトコードの自動意味解析を必要とする。 バイトコードを可読でセマンティックに忠実なSolidityコードに変換する,先駆的な逆コンパイルパイプラインを導入する。
  論文  参考訳（メタデータ） (2025-06-24T13:42:59Z)
• BlockScan: Detecting Anomalies in Blockchain Transactions [16.73896087813861]
  BlockScanはブロックチェーントランザクションの異常検出用にカスタマイズされたTransformerである。 この研究は、ブロックチェーンデータ分析にTransformerベースのアプローチを適用するための新しいベンチマークを設定する。
  論文  参考訳（メタデータ） (2024-10-05T05:11:34Z)
• FORAY: Towards Effective Attack Synthesis against Deep Logical Vulnerabilities in DeFi Protocols [7.413607595641641]
  我々は,DeFiプロトコルの深い論理的バグに対して,非常に効果的な攻撃合成フレームワークであるForayを紹介する。 DSLに基づいて、まず指定されたDeFiプロトコルをトークンフローグラフにコンパイルします。 そこで我々は,特定の攻撃目標に対する攻撃スケッチを合成する効率的なスケッチ生成手法を設計した。
  論文  参考訳（メタデータ） (2024-07-08T19:35:48Z)
• Secure compilation of rich smart contracts on poor UTXO blockchains [0.8192907805418581]
  UTXOモデルのための中間レベル言語であるILLUMを提案する。 コンパイラをILLUMから、ループフリースクリプトでベアボーンのUTXOブロックチェーンに定義する。 コベナント(covenants)は、トランザクションのチェーンに沿ってスクリプトを保存するメカニズムです。
  論文  参考訳（メタデータ） (2023-05-16T15:40:18Z)
• A formal model for ledger management systems based on contracts and temporal logic [0.0]
  台帳のような第2世代のブロックチェーンは、スマートコントラクトと結合される。 任意のプログラミング構造としてのスマートコントラクトの現在の実装は、危険なバグを受けやすいものにしている。 本稿では,有限状態オートマトンとしてモデル化された契約の概念を形式化し,データベースの分割と信頼性の回復を提案する。
  論文  参考訳（メタデータ） (2021-09-30T15:34:28Z)
• 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 Multi-Solution Bernoulli Search with Applications to Bitcoin's Post-Quantum Security [67.06003361150228]
  作業の証明(英: proof of work、PoW)は、当事者が計算タスクの解決にいくらかの労力を費やしたことを他人に納得させることができる重要な暗号構造である。 本研究では、量子戦略に対してそのようなPoWの連鎖を見つけることの難しさについて検討する。 我々は、PoWs問題の連鎖が、マルチソリューションBernoulliサーチと呼ばれる問題に還元されることを証明し、量子クエリの複雑さを確立する。
  論文  参考訳（メタデータ） (2020-12-30T18:03:56Z)

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

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