arXiv search: November 08, 2024
Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
目的:
この論文は、自然言語(NL)から時間論理仕様(TSL)への変換を行うプロセスを改善し、形式的検証を用いたコード生成を通じて、プロジェクト内の未検証コードの行数を減少させることを目的としています。また、大規模なコードベースにおける検証済みコードの統合を容易にすることを目指しています。
使用したデータや情報:
この論文では、自然言語で記述された問題の概要、システムの振る舞いに関する詳細な記述、およびデータと制御を分離するための関数と述語用語が使用されています。これらは、TSL仕様を生成し、それを用いて正しい構造のコードを合成するための入力として用いられています。
新規性や解決できた問題:
このアプローチの新規性は、LLM（大規模言語モデル）を使用して自然言語からTSLへの変換を行い、形式的方法に基づくプログラム合成を利用する点にあります。これにより、開発者は手動での検証負担を軽減しつつ、検証済みのコードを大規模なコードベースに統合できるようになりました。また、TSLの導入によって、データと制御の分離が強化され、より複雑な条件文をコンパクトな構文表現でエンコードできるようになりました。
未解決問題:
未解決の問題としては、LLMが生成するコードの正確性をさらに向上させるための研究が必要です。また、より複雑なリアクティブシステムに対して、TSLパイプラインを使用したソリューションの生成を進化させることも課題とされています。これには、TSL仕様のさらなる洗練や、LLMの能力を最大限に活用するための新たな手法の開発が含まれます。
url:
https://arxiv.org/abs/2410.19736
title:
Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
authors:
William Murphy, Nikolaus Holzer, Feitong Qiao, Leyi Cui, Raven Rothkopf, Nathan Koenig, Mark Santolucito
date:
18 September, 2024;
Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods
目的:
与えられた論文は、プログラムの仕様生成プロセスにおいて、PathCrawlerを使用して得られたテストケースからACSLアノテーションを生成する方法を分析し、改善することを目的としています。このプロセスを通じて、プログラムのバグを特定し、プログラムの正確性を向上させることが目標です。
使用されたデータや情報:
この論文では、PathCrawlerによって生成されたCSVファイルが使用されています。このCSVファイルには、プログラム関数「testme」のために生成されたテストケースが含まれており、各テストケースは入力値として「len」、「input_buffer」、「input_msg」を持ち、出力値も記録されています。また、プログラムの挙動を分析し、特定のパターンを認識してACSLアノテーションとして表現するために、LLM（大規模言語モデル）が使用されています。
新規性や解決できた問題:
この研究の新規性は、大規模言語モデルを用いてプログラムのテストケースから直接ACSLアノテーションを生成する方法を探求している点にあります。これにより、プログラムの仕様を自動的に生成し、人間のプログラマが行う必要のある手作業を削減することが可能になります。また、テストケースとプログラムの挙動の間の論理的なギャップを埋めることで、より正確なプログラム仕様の提示が可能になり、プログラムの信頼性が向上しました。
未解決問題:
未解決の問題としては、生成されたACSLアノテーションが常にプログラムの全ての実行パスを網羅しているわけではないため、仕様の過剰近似が発生する可能性が残されています。また、異なるプログラムやより複雑なプログラムに対してもこの手法が効果的であるかどうかの検証が必要です。さらに、自動生成された仕様が実際のプログラム開発プロセスにおいてどのように有用であるかを評価するための実用的な研究も求められています。
url:
https://arxiv.org/abs/2406.15540
title:
Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods
authors:
George Granberry, Wolfgang Ahrendt, Moa Johansson
date:
18 September, 2024;
Inductive Learning of Logical Theories with LLMs: A Complexity-graded Analysis
目的:
この研究の主な目的は、言語モデル（LLM）を使用して、背景知識と訓練例に基づいて理論を誘導するプロセスを評価することです。具体的には、異なるルールセットの複雑さ（CHAIN, RDG, DRDGなど）に対応する合成データセットを生成し、LLMが生成した理論を形式的推論エンジンからのフィードバックを用いて反復的に洗練する方法を提案しています。
使用データ・情報:
この研究では、背景知識（BK）、正の例（E+）、負の例（E-）を含む合成データセットを使用しています。これらのデータは、言語モデルが理論を誘導するための入力として機能し、生成された理論の評価と洗練の基盤となります。
新規性・解決した問題:
この研究の新規性は、LLMを用いて論理理論を誘導し、形式的推論エンジン（Prolog）を使用してこれらの理論を評価し、反復的に洗練する方法をシステマティックに評価する点にあります。これにより、LLMの理論誘導の能力を定量的に評価し、異なるルールセットの複雑さに対するその効果を検証しました。
未解決問題:
将来の課題としては、より多様な背景知識や例を用いたデータセットでのLLMのパフォーマンスの検証、理論誘導の過程での言語モデルの限界とその改善策の探求、さらに複雑なルールセットやリアルワールドのシナリオへの適用が挙げられます。これらの課題に取り組むことで、LLMの理論誘導能力をさらに向上させ、実用的な応用範囲を広げることが期待されます。
url:
https://arxiv.org/abs/2408.16779
title:
Inductive Learning of Logical Theories with LLMs: A Complexity-graded Analysis
authors:
João Pedro Gandarela, Danilo S. Carvalho, André Freitas
date:
15 August, 2024;
Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
目的:
本論文は、自然言語の意図を形式的なメソッドの事後条件に変換できるかどうかを評価することを目的としています。具体的には、LLM（Large Language Models）を使用して、プログラムの意図を正確に捉え、形式的な仕様として表現できるかどうかを検証しています。
使用したデータや情報:
この研究では、EvalPlusとDefects4Jという2つの異なるベンチマークを使用しています。EvalPlusはPythonの問題が含まれており、それぞれに関数のスタブと自然言語記述があります。Defects4Jは、実際のプロジェクトから抽出されたJavaのバグが含まれており、より複雑な関数やプロジェクト間の結合を含んでいます。
新規性や解決できた問題:
この研究の新規性は、LLMを用いて自然言語から形式的なメソッド事後条件を生成するアプローチをシステマティックに評価した点にあります。特に、GPT-4やStarChatなどのモデルを使用して、自然言語の仕様からプログラムの意図を捉え、形式的な事後条件を生成する能力を検証しました。また、生成された事後条件が実際のバグを特定できるかどうかも評価しました。
未解決問題:
LLMが生成する事後条件の複雑性と正確性のバランスを取ること、特に複雑なプログラムや実世界のアプリケーションにおける性能の向上が未解決の課題として残っています。また、異なるプログラミング言語や環境におけるモデルの適用性をさらに検証する必要があります。さらに、事後条件が実際のプログラミング環境でどのように役立つか、その実用性を高めるための研究も必要です。
url:
https://arxiv.org/abs/2310.01831
title:
Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
authors:
Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, Shuvendu K. Lahiri
date:
15 April, 2024;
Utilizing Large Language Models to Translate RFC Protocol Specifications to CPSA Definitions
目的:
この論文は、大規模言語モデル（LLM）を使用して、インターネットプロトコルの安全性を向上させるために、RFC（Request for Comments）プロトコル仕様をCPSA（Cryptographic Protocol Shapes Analyzer）の形式に翻訳する方法を提案しています。これにより、プロトコル分析の複雑さと労力を減らし、形式的手法分析のアクセシビリティを向上させることを目的としています。
使用されたデータや情報:
この研究では、Code Llamaという名前のLLMが使用されており、このモデルは公開されているコード、コードに関する議論、自然言語の質問や回答に含まれるコードスニペットから構成される5000億トークンの初期データセットで訓練されています。さらに、RFC、CPSAプロトコル定義、プロトコル要件とCPSAプロトコル定義のマッチングペアを含むファインチューニングデータセットを使用しています。
新規性や解決できた問題:
この研究の新規性は、NLP（自然言語処理）とGenAI（生成AI）の最近の進歩を活用して、RFCプロトコル仕様を自動的にCPSAに適合する構造化されたプロトコル定義に変換するシステムを提案した点にあります。これにより、プロトコルの仕様を手動で解析し、形式的手法ツールで使用可能な形式に変換する必要がある従来の課題を解決しています。
未解決問題:
LLMによって生成された出力は、最終的なCPSA処理前にドメインエキスパートによる修正が必要であるため、完全な自動化には至っていません。将来的には、より精度の高い自動翻訳と、エキスパートの介入を最小限に抑えるための改善が求められます。また、異なる形式のプロトコル分析ツールへの適応性も拡大する必要があります。
url:
https://arxiv.org/abs/2402.00890
title:
Utilizing Large Language Models to Translate RFC Protocol Specifications to CPSA Definitions
authors:
Martin Duclos, Ivan A. Fernandez, Kaneesha Moore, Sudip Mittal, Edward Zieglar
date:
30 January, 2024;
Automated SELinux RBAC Policy Verification Using SMT
目的:
この論文の主な目的は、SELinuxのRBACポリシーを自動的に検証するツールを使用して、セキュリティの脆弱性を特定し、修正することです。特に、システムアップデートのディレクトリである/data/incrementalに対する過剰なアクセス許可を持つポリシーを検証し、不正なアプリケーションのインストールを防ぐことを目指しています。
使用したデータや情報:
論文では、SELinuxのタイプエンフォースメントポリシー設定ファイルを解析するために、SMT (Satisfiability Modulo Theories) ソルバーを使用しています。具体的には、system_appやapk_data_fileといったSELinuxのタイプ、インストールやリカバリなどの特定のプリンシパルに関連する属性を定義し、これらの情報を基にアクセス制御ポリシーの正確性を自動的に検証しています。
新規性や解決した問題:
この研究の新規性は、SELinuxのポリシーを手動で検証する代わりに、SMTソルバーを利用して自動化する点にあります。これにより、大量のポリシー設定ファイルにわたる複雑な検証作業を効率化し、人的ミスを減らすことができます。解決した問題は、過剰なアクセス許可によるセキュリティリスクを特定し、システムのセキュリティを強化することです。
未解決問題:
将来的には、SELinuxのポリシー設定が進化し続けるため、新しいタイプや属性、アクセス制御ルールを定期的に更新し、ツールの検証能力を維持する必要があります。また、他のセキュリティシステムや異なるプラットフォームでの応用可能性についても検討することが挙げられます。
url:
https://arxiv.org/abs/2312.04586
title:
Automated SELinux RBAC Policy Verification Using SMT
authors:
Divyam Pahuja, Alvin Tang, Klim Tsoutsman
date:
4 December, 2023;
A Framework for Programmability in Digital Currency
目的:
この論文は、異なるレベルのプログラム可能性を持つブロックチェーンシステムを分析し、それぞれのシステムがどのように機能し、どのような特徴を持つかを詳細に説明することを目的としています。具体的には、トランザクションのプライバシーを保持する暗号通貨や、より複雑なスマートコントラクトが可能なシステムなど、異なるレベルでのプログラム可能性を比較しています。
使用されたデータや情報:
この論文では、Bitcoin、Ethereum、Zcash、Monero、Mimblewimbleなど、異なるブロックチェーンプラットフォームの技術的な仕様や機能を用いています。また、これらのプラットフォームがどのようにトランザクションを処理し、どのようなスクリプトやスマートコントラクトが可能かという点に焦点を当てて分析しています。
新規性や解決できた問題:
この論文の新規性は、異なるブロックチェーンシステムのプログラム可能性のレベルを体系的に分類し、それぞれのレベルで可能な機能や制限を明確にした点にあります。また、プライバシーを重視する暗号通貨がスクリプトをほとんど使用しない理由や、Ethereumのような高度なスマートコントラクトが可能なシステムの特徴を詳細に解析することで、ブロックチェーン技術の理解を深めることができました。
未解決問題:
将来的には、より高度なプログラム可能性とプライバシー保護を両立させるブロックチェーンシステムの開発が求められています。また、スマートコントラクトの安全性を向上させるための新しいアプローチや、異なるブロックチェーン間でのスムーズな相互運用性を実現する技術の開発も重要な課題となっています。
url:
https://arxiv.org/abs/2311.04874
title:
A Framework for Programmability in Digital Currency
authors:
Nikhil George, Thaddeus Dryja, Neha Narula
date:
8 November, 2023;
Pre-deployment Analysis of Smart Contracts -- A Survey
目的:
この論文の主な目的は、スマートコントラクトの脆弱性と事前展開分析方法を分類し、プログラム特性の概念を用いることで、既存の調査と比較して新たな視点を提供することです。これにより、スマートコントラクトの安全性を向上させるための分析手法の理解と適用を促進することを目指しています。
使用されたデータや情報:
この論文では、スマートコントラクトの事前展開分析に関する既存の文献を広範囲にレビューし、35のプログラム特性を詳細に分析しました。また、静的型付け、抽象解釈、制御フロー法、汚染分析、シンボリック実行など、さまざまな分析方法が検討されています。
新規性や解決できた問題:
この論文の新規性は、スマートコントラクトの脆弱性と分析方法をプログラム特性に基づいて体系的に分類するアプローチにあります。これにより、脆弱性と分析方法の関係を明確にし、それぞれの方法の特徴や強みを詳細に理解することができます。また、形式的手法が生存特性を証明する利点を提供するなど、具体的な分析方法の効果も明らかにしました。
未解決問題:
一部のプログラム特性に対してはまだ形式化が行われていないため、これらの特性の形式化と厳密な扱いにはさらなる研究が必要です。また、機械学習手法がプロパティに強い保証を提供できる可能性についても、さらなる調査が求められています。さらに、非イーサリアムスマートコントラクトに対する静的型付け以外の従来の分析方法の適用とその効果についても、今後の研究課題として挙げられます。
url:
https://arxiv.org/abs/2301.06079
title:
Pre-deployment Analysis of Smart Contracts -- A Survey
authors:
Sundas Munir, Walid Taha
date:
30 June, 2023;
Security Defense For Smart Contracts: A Comprehensive Survey
目的:
この論文は、スマートコントラクトのセキュリティ防御に関する包括的な調査を行い、脅威緩和ソリューションの概要とその方法論を提供することを目的としています。具体的には、さまざまな脅威緩和手法がどのようにスマートコントラクトの脆弱性を検出、防御し、解析するかを概説し、それぞれの手法のワークフローと入出力のデータマッピングを詳細に解説しています。
使用されたデータや情報:
この論文では、スマートコントラクトのソースコード、バイトコード、ブロックチェーン上のデータ、セキュリティ仕様など、さまざまな入力データを使用しています。また、脅威緩和ソリューションの出力としては、人間が読めるセキュリティレポート、機械が読めるメタデータ、防御行動、脆弱性の証明などがあります。
新規性と解決できた問題:
この調査の新規性は、スマートコントラクトの脅威緩和ソリューションを網羅的に分析し、それぞれの手法がどのように機能するかの詳細なワークフローを提供する点にあります。これにより、脆弱性の特定、防御策の提案、セキュリティの向上に寄与しています。また、異なる入力と出力を持つ脅威緩和ソリューションの比較が可能になり、適切なソリューション選択の支援を行っています。
未解決問題:
未解決問題としては、脅威モデルのさらなる精密化、新たな攻撃手法に対応する脅威緩和ソリューションの開発、実用化に向けた性能と効率の向上、異なるブロックチェーンプラットフォーム間での互換性の確保などが挙げられます。また、新しい脆弱性や攻撃手法が常に出現するため、継続的な研究と更新が必要です。
url:
https://arxiv.org/abs/2302.07347
title:
Security Defense For Smart Contracts: A Comprehensive Survey
authors:
Nikolay Ivanov, Chenning Li, Qiben Yan, Zhiyuan Sun, Zhichao Cao, Xiapu Luo
date:
9 May, 2023;
OpenSCV: An Open Hierarchical Taxonomy for Smart Contract Vulnerabilities
目的:
与えられた論文は、スマートコントラクトの脆弱性に関して包括的かつ階層的な分類体系を提供することを目的としています。この分類体系は、スマートコントラクトのセキュリティ問題をより体系的に理解し、対策を講じるための基盤となることを意図しています。
使用したデータや情報:
この研究では、過去の研究文献、既存のセキュリティ問題のデータベース、そしてスマートコントラクトの実際のセキュリティインシデントの分析結果を用いています。これにより、実際の脆弱性事例と理論的な知見を組み合わせ、より実用的な分類体系を構築しています。
新規性や解決できた問題:
この研究の新規性は、スマートコントラクトの脆弱性に対する階層的な分類体系を提案している点にあります。多くの既存研究が個別の脆弱性に焦点を当てていたのに対し、この研究では脆弱性を体系的に整理し、関連性や類似性に基づいてグループ化しています。これにより、開発者や研究者が脆弱性をより総合的に理解し、対策を立てやすくなるという問題を解決しています。
未解決問題:
将来取り組むべき未解決問題としては、新たに発見される脆弱性への迅速な対応や、分類体系の更新が挙げられます。スマートコントラクトの技術や利用の仕方が進化するにつれて、新しいタイプの脆弱性が発生する可能性があります。そのため、分類体系を定期的に見直し、新しい脆弱性情報を統合することが重要です。また、実際の脆弱性対策の効果を検証し、分類体系の有用性を評価することも必要です。
url:
https://arxiv.org/abs/2303.14523
title:
OpenSCV: An Open Hierarchical Taxonomy for Smart Contract Vulnerabilities
authors:
Fernando Richter Vidal, Naghmeh Ivaki, Nuno Laranjeiro
date:
7 April, 2023;
Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
目的:
この論文は、関数revとsnocの契約の妥当性を検証することを目的としています。具体的には、CHC（制約付きホーン節）ソルバーを用いて、リストの逆順と要素の追加処理に関する契約が満たされるかどうかの証明を試みています。
使用したデータや情報:
論文では、プログラム関数revとsnocに関するCHCと、それらの関数の契約を表すゴールとして表現されたCHCを使用しています。また、状態最先端のCHCソルバーであるEldaricaとSPACERが、リストに関する帰納的推論やsnocの契約の妥当性を用いないため、その証明に失敗することが指摘されています。
新規性や解決できた問題:
この論文の新規性は、リストやブール項を含まない新しいCHCセットTransfReverseを導入することにより、帰納的推論を必要とせずに契約の妥当性を証明できる点にあります。これにより、TransfReverseが充足可能であれば、元のReverseも充足可能であると証明できます。これは、従来のCHCソルバーが直面していた問題を解決するものです。
未解決問題:
将来的には、この検証方法を実用的に適用するために、プログラムや契約をCHCに自動変換する翻訳器を開発することが計画されています。また、検証条件を様々な論理理論でチェックするために、SMTソルバーをバックエンドとして使用する検証器の使用も検討されています。
url:
https://arxiv.org/abs/2205.06236
title:
Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
authors:
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
date:
7 September, 2022;
Logically Consistent Adversarial Attacks for Soft Theorem Provers
目的:
この研究の主な目的は、自然言語処理における論理的整合性の問題に対処することです。具体的には、テキストの意味関係が小さな摂動によってどのように影響を受けるかを検討し、攻撃モデルがこれをどのように利用できるかを探求しています。また、攻撃者が生成するサンプルの論理的整合性を確保するための方法論も提案しています。
データや情報:
この研究では、自然言語の文とそれに関連する論理プログラムを用いています。攻撃モデルは、これらの入力から摂動を適用し、変更されたサンプルの論理的整合性を再計算するためにシンボリックソルバーを使用します。また、トランスフォーマーを用いたエンコーダーを利用して、入力データから隠れ状態を生成し、攻撃戦略に基づいてカテゴリカルなパラメータを出力します。
新規性や解決できた問題:
この研究は、論理的整合性を考慮したテキストの摂動生成に焦点を当てており、特に論理的な意味を持つデータに対する攻撃の成功率と転移性を向上させることに成功しています。また、攻撃生成プロセスにシンボリックソルバーを組み込むことで、生成された攻撃サンプルの論理的整合性を保証する方法を提案しており、これにより無効な攻撃例の生成を防ぐことができます。
未解決問題:
将来的には、攻撃者が定量的なルールを合成する能力を持たせることで、より広範な脆弱性を露呈させることが期待されます。また、論理プログラムの意味特性をより深く理解し、STP（論理定理証明器）の開発において脆弱性を特定し、デバッグするためのフレームワークとしてLA V Aを活用することも今後の課題です。
url:
https://arxiv.org/abs/2205.00047
title:
Logically Consistent Adversarial Attacks for Soft Theorem Provers
authors:
Alexander Gaskell, Yishu Miao, Lucia Specia, Francesca Toni
date:
29 April, 2022;
Pacta sunt servanda: legal contracts in Stipula
与えられた論文の目的:
この論文は、スマート法的契約のためのプログラミングモデル「Stipula」を提案し、それを用いて法的義務や約束をエンコードする方法を示しています。具体的には、資産の移動や時間に依存するイベントのスケジューリングなど、スマートコントラクトの運用におけるセマンティクスを定義しています。
使用されたデータや情報:
論文では、スマートコントラクトの例として「Bike Rental」契約を用いています。この契約では、貸し手と借り手間の合意から始まり、資産の割り当てや状態の変更などのプロセスが詳細に説明されています。また、プログラムの状態遷移や関数呼び出しのルールが定義されており、具体的な実行例を通じてその動作が説明されています。
新規性や解決できた問題:
Stipulaは、時間依存のイベントや資産の移動を扱うことができる点で新規性があります。これにより、法的契約の自動化とスマートコントラクトの実行における予測可能性が向上します。また、資産が負の値を取ることを防ぐなど、スマートコントラクトにおける安全性の向上も図られています。
未解決問題:
論文では、ランタイムエラーや契約エラーの取り扱いについては将来の研究課題として残されています。これには、例外ケースの実行時の法的問題に関する深い学際的分析が必要とされています。また、契約間の相互参照を可能にする言語拡張についても、今後の研究で取り組む必要があります。
url:
https://arxiv.org/abs/2110.11069
title:
Pacta sunt servanda: legal contracts in Stipula
authors:
Silvia Crafa, Cosimo Laneve, Giovanni Sartor
date:
21 October, 2021;
SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts
目的:
この論文では、Standard ML (SML) の抽象構文木（AST）をCoqのGallina言語のASTに変換することが目的です。この変換を通じて、SMLのコードを形式検証可能なCoqコードへと変換し、プログラムの正確性を保証することを目指しています。
使用したデータや情報:
変換プロセスでは、SMLの構文とセマンティクスを定義するための情報、Coqの言語仕様、そして両言語間の型システムや機能の違いに関する詳細な情報が使用されています。また、EquationsプラグインやHaMLetなどのツールが利用されており、これにより依存型を用いたパターンマッチングや多相型の扱いが可能になっています。
新規性や解決できた問題:
この研究の新規性は、SMLとCoqの間での直接的なコード変換を可能にすることにあります。特に、多相型やパターンマッチング、例外処理など、言語間で異なる概念をどのように翻訳するかについて具体的な解決策を提供しています。また、非再帰的な関数やインフィックス関数の翻訳に関しても詳細な方法が示されており、これによりSMLのコードをCoqで形式検証可能な形に変換することができます。
未解決問題:
未解決の問題としては、例外処理や副作用の取り扱いが挙げられます。Gallinaは純粋な言語であり、副作用を直接的にはサポートしていないため、SMLの例外処理をどのようにGallinaに翻訳するかは依然として課題です。また、翻訳されたCoqコードの性能最適化や、より複雑なSMLプログラムへの対応も今後の課題とされています。
url:
https://arxiv.org/abs/2107.07664
title:
SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts
authors:
Laila El-Beheiry, Giselle Reis, Ammar Karkour
date:
15 July, 2021;
Online Abstract Dynamic Programming with Contractive Models
目的:
この論文では、時間変動する抽象動的プログラミング（DP）問題に対するオンラインアルゴリズムを開発し、その理論的分析を提供することを目的としています。具体的には、オンライン環境での価値反復（VI）アルゴリズムや方策反復（PI）アルゴリズムのパフォーマンスを解析し、時間変動する最適コストや方策を追跡する問題に取り組んでいます。
使用データ・情報:
論文からは具体的なデータセットの使用についての言及はありませんが、一般に抽象DPの問題では状態空間、行動空間、コスト関数、遷移確率などの情報がモデルの定義に用いられます。また、時間変動する抽象マッピングや環境の不確実性に対応するための理論的分析が行われています。
新規性・解決問題:
この研究の新規性は、時間変動する抽象DPマッピングに対してオンラインアルゴリズムを適用し、その理論的な解析を行った点にあります。具体的には、オンライン価値反復、オンライン方策反復、オンライン最適主義方策反復など、複数のオンラインアルゴリズムを開発し、それらの追跡誤差の限界を明らかにしました。これにより、時間変動するコスト関数や方策に対応するための理論的基盤が提供されています。
未解決問題:
将来の研究としては、より一般的な状況や複雑な環境におけるオンラインアルゴリズムの適用性を高めること、さらに実世界の応用例に即した詳細なケーススタディの実施、アルゴリズムの実装や実行時の最適化などが挙げられます。また、異なるタイプのコスト関数や制約条件を持つ問題設定に対するアプローチの開発も重要な課題です。
url:
https://arxiv.org/abs/2107.01383
title:
Online Abstract Dynamic Programming with Contractive Models
authors:
Xiuxian Li, Lihua Xie
date:
3 July, 2021;
Inverted and programmable Poynting effects in metamaterials
目的:
この研究の主な目的は、ねじれと圧縮の下でプログラム可能な非線形弾性率を持つメタマテリアルを設計することです。具体的には、ねじれによる軸方向の圧縮が非線形ねじれを誘発する新しいタイプの逆ポインティング効果を示すシステムを開発し、構造のポインティング率を初期の負の値からゼロおよび正の値にプログラムする方法を示します。
使用されたデータや情報:
本研究では、複数の実験とモデリングを通じてデータを収集しました。具体的には、固定負荷および固定ギャップの条件下でのねじれ角に対する軸方向ひずみとせん断力の変化を測定し、これらのデータを用いてポインティング率とせん断率を計算しました。また、ヤング率で規格化されたこれらの率を、予圧縮ひずみの関数としてプロットしました。
新規性や解決できた問題:
この研究の新規性は、特定のプリコンプレッションを適用することにより、メタマテリアルのポインティング応答をプログラム可能であり、その符号と大きさを調整できる点にあります。従来の材料では見られなかった、負のポインティング率を示す材料の設計も可能としました。これにより、シアーと通常の応答の間の複雑なカップリングを理解し、それを利用する方法が提供されます。
未解決問題:
将来的には、異なる材料や構造を用いた場合のポインティング効果のさらなる調査が必要です。また、実際の応用において、これらのメタマテリアルがどのように機能するかを詳細に調べる必要があります。さらに、より複雑な荷重条件下での挙動の理解も、今後の課題として残されています。
url:
https://arxiv.org/abs/2102.10904
title:
Inverted and programmable Poynting effects in metamaterials
authors:
Aref Ghorbani, David Dykstra, Corentin Coulais, Daniel Bonn, Erik van der Linden, Mehdi Habibi
date:
18 May, 2021;
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in Obsidian
目的:
この研究は、ObsidianとSolidityという2つのプログラミング言語を使用してスマートコントラクトを作成する際の学習効果と実装の安全性を比較することを目的としています。特に、Obsidianの所有権、タイプステート、アセットなどの概念を学ぶことがプログラマーのエラー発生率やセキュリティ対策にどのように影響するかを検証しています。
使用したデータや情報:
この研究では、参加者にObsidianとSolidityのプログラミング言語を用いてスマートコントラクトを作成させ、そのプロセスでのエラーレートやセキュリティ違反を記録しました。参加者は事前にオンラインでJavaに関する基本的な質問に答えることで選ばれ、その後、特定の言語に関するウェブベースのチュートリアルを受けました。このチュートリアルには、理解を深めるための練習問題が含まれていました。
新規性や解決できた問題:
この研究の新規性は、Obsidianという比較的新しいプログラミング言語がSolidityと比較してどのような利点や欠点を持つかを実証的に評価した点にあります。特に、Obsidianが提供する所有権やタイプステートといった概念がプログラマーのエラー発生率を下げ、より安全なスマートコントラクトの実装を促進するかどうかを検証しました。
未解決問題:
この研究では、ObsidianとSolidityを用いたスマートコントラクトの開発における学習曲線や初期のエラー発生率に焦点を当てましたが、長期的なメンテナンスやスケーラビリティに関する問題は解決されていません。また、異なる背景を持つプログラマーに対する言語の適用性についてもさらに研究が必要です。
url:
https://arxiv.org/abs/2003.12209
title:
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in Obsidian
authors:
Michael Coblenz, Jonathan Aldrich, Joshua Sunshine, Brad A. Myers
date:
15 October, 2020;
sFuzz: An Efficient Adaptive Fuzzer for Solidity Smart Contracts
目的:
この論文では、EVM（Ethereum Virtual Machine）スマートコントラクトのためのアダプティブファジングエンジンであるsFuzzの開発と評価が主な目的です。sFuzzは、スマートコントラクトの脆弱性を効率的かつ効果的に特定することを目指しています。
使用したデータや情報:
sFuzzの評価のために、4112個のスマートコントラクトを用いて実験が行われました。これらのコントラクトは、複数の異なる脆弱性を持つ可能性があるため、sFuzzの有効性を検証するのに適しています。また、テストケースの生成や実行、ブランチカバレッジの計測などに関するデータが収集・分析されました。
新規性や解決できた問題:
sFuzzは、フィードバック誘導型のアダプティブファジング戦略を採用しており、これによりスマートコントラクトのテストの効率と有効性が向上します。具体的には、sFuzzは他のツールよりも高速にテストケースを生成・実行でき、より多くのブランチをカバーすることができました。また、異なる種類の脆弱性に対する詳細な分析と評価が行われ、sFuzzが他のファジングツールやシンボリック実行ツールと比較して優れた性能を示すことが確認されました。
未解決問題:
sFuzzの適用時間を長くすることで、さらに多くのブランチカバレッジや脆弱性の特定が期待されます。また、sFuzzの初期テストケース生成の選択に依存する可能性があるため、初期ポピュレーションの選択方法の改善が必要です。さらに、実際のスマートコントラクトの作者の意図を完全に理解することは困難であるため、コントラクトの意図をより正確に把握する方法の開発も求められています。
url:
https://arxiv.org/abs/2004.08563
title:
sFuzz: An Efficient Adaptive Fuzzer for Solidity Smart Contracts
authors:
Tai D. Nguyen, Long H. Pham, Jun Sun, Yun Lin, Quang Tran Minh
date:
18 April, 2020;
ÆGIS: Shielding Vulnerable Smart Contracts Against Attacks
目的:
与えられた論文では、スマートコントラクトにおける再入可能性攻撃やその他のセキュリティ脆弱性を検出し、防止するための攻撃パターンを検出するシステムの開発に焦点を当てています。このシステムは、Ethereumブロックチェーン上でスマートコントラクトの安全性を向上させることを目指しています。
使用されたデータや情報:
この研究では、EVM（Ethereum Virtual Machine）のオペコード、プログラムカウンター、コールスタックの深さ、実行中のコントラクトのアドレス、スタック上の値、メモリ内の値などの実行トレースデータを用いています。これらのデータを解析し、制御フローやデータフローの抽出を行い、攻撃パターンにマッチするかどうかを判断します。
新規性及び解決できた問題:
本研究の新規性は、動的なタイント追跡と呼ばれる技術を用いて、スマートコントラクトの実行中にデータの流れを追跡し、潜在的なセキュリティ脆弱性をリアルタイムで検出する点にあります。また、再入可能性攻撃だけでなく、他の複数の脆弱性も検出可能な汎用的なフレームワークを提供しています。これにより、スマートコントラクトのセキュリティが大幅に向上しました。
未解決問題:
今後の課題としては、提案されたシステムのスケーラビリティや効率性をさらに向上させること、新たに発見される可能性のある攻撃手法に対する迅速な対応、ブロックチェーン技術の進化に伴うシステムの更新などが挙げられます。また、プライバシー保護と検証可能性を両立させるための研究も重要です。
url:
https://arxiv.org/abs/2003.05987
title:
ÆGIS: Shielding Vulnerable Smart Contracts Against Attacks
authors:
Christof Ferreira Torres, Mathis Baden, Robert Norvill, Beltran Borja Fiz Pontiveros, Hugo Jonker, Sjouke Mauw
date:
12 March, 2020;
A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts
目的:
この論文では、Ethereumベースのスマートコントラクトサービスのセキュリティと信頼性を検証するためのハイブリッド形式の検証システムFSPVM-Eを提案し、実装しています。このシステムは、シンボリック実行と高階論理定理証明を組み合わせて使用しています。
使用されたデータや情報:
FSPVM-Eは、SolidityソースコードレベルでEthereumベースのスマートコントラクトを直接実行および検証できるように設計されています。これには、一般的な形式のメモリモデル、仮想シンボリック実行環境、単一ステートメントユニット評価が含まれます。また、SolidityからLolisaへの自動翻訳や、特定の実行環境に基づいて形式的仕様を生成するツールも提供しています。
新規性と解決できた問題:
FSPVM-Eは、Solidityの大部分の形式的構文と意味論をGADTsで提供する初の検証システムであり、Coqで実装されています。これにより、形式化の一貫性の問題が解決され、スマートコントラクトのサービス行動を厳密にシミュレートすることが可能になります。また、静的、コンコリック、選択的シンボリック実行を同時にサポートし、記憶装置、環境、制約解決の問題に対処しています。
未解決問題:
今後の研究では、さらに多くのSolidityの構文や機能をサポートするためのシステムの拡張、実行効率と自動化の度合いをさらに向上させる方法、さらに複雑なスマートコントラクトに対する検証能力の強化が求められます。また、新しい実行セマンティクスのサポートを拡張することで、新しい抽象構文のLolisaをサポートすることも重要です。
url:
https://arxiv.org/abs/1902.08726
title:
A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts
authors:
Zheng Yang, Hang Lei, Weizhong Qian
date:
22 January, 2020;
Resource-Aware Session Types for Digital Contracts
目的:
与えられた論文では、リソースに敏感なセッション型を使用して、プロセスやメッセージの挙動を分析し、システムのパフォーマンスを向上させることを目的としています。具体的には、プロセス間の通信やリソースの利用を効率的に管理し、デッドロックの回避やリソースの最適化を図ることが目標です。
使用したデータや情報:
この研究では、プロセスやメッセージがどのようにステップを進めるかについての詳細なケーススタディを用いています。各ケースでは、プロセスの状態やメッセージの内容、それらがどのように相互作用するかについての具体的な情報が用いられています。また、リニアロジックやセッション型の理論を基にした形式的な証明やルールが適用されています。
新規性や解決できた問題:
この研究の新規性は、リソースに敏感なセッション型を用いることで、プロセスのリソース使用をより正確にモデル化し、システムの効率を向上させる点にあります。具体的には、プロセスがブロックされることなくスムーズに進行できるようにするためのルールや、デッドロックを防ぐための方法が提案されています。
未解決問題:
将来的には、より複雑なシステムや異なる種類のリソースを扱う場合の分析、プロセスのスケーリングに関する問題など、さらに多くのシナリオでの適用性を高める必要があります。また、実際のシステムへの適用にあたっては、パフォーマンスの測定や最適化の具体的な方法論についても検討する必要があります。
url:
https://arxiv.org/abs/1902.06056
title:
Resource-Aware Session Types for Digital Contracts
authors:
Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, Ishani Santurkar
date:
22 November, 2019;
Vandal: A Scalable Security Analysis Framework for Smart Contracts
目的:
与えられた論文では、Vandalという静的解析ツールを用いて、Ethereumスマートコントラクトにおけるセキュリティ脆弱性を特定し、分析することを目的としています。具体的には、自動的にセキュリティの脆弱性を検出し、スマートコントラクトの安全性を向上させることを目指しています。
使用されたデータや情報:
この研究では、Ethereumブロックチェーン上にデプロイされたすべてのスマートコントラクトのバイトコードを含む141kのユニークなスマートコントラクトを含むコーパスを使用しました。また、Vandalの性能を他の静的解析ツールと比較するために、Oyente、EthIR、Rattle、Mythrilといった他のシステムのパフォーマンスデータも用いています。
新規性や解決できた問題:
Vandalは、特定の脆弱性を検出するための詳細な解析を行う能力において、他の既存ツールよりも優れている点が新規性です。また、平均実行時間においても他のシステムより優れており、効率的な解析が可能であるという点で問題を解決しています。特に、tx.originの使用やunchecked send、reentrancyといった一般的な脆弱性に対して高い検出能力を持っています。
未解決問題:
将来的には、さらに多様な脆弱性に対応するための解析能力の拡張や、解析速度の向上、さらには解析結果の精度を高めるためのアルゴリズムの改善が必要です。また、新たに発見される可能性のある脆弱性に対しても迅速に対応できるように、システムの更新や維持管理が重要となります。
url:
https://arxiv.org/abs/1809.03981
title:
Vandal: A Scalable Security Analysis Framework for Smart Contracts
authors:
Lexi Brent, Anton Jurisevic, Michael Kong, Eric Liu, Francois Gauthier, Vincent Gramoli, Ralph Holz, Bernhard Scholz
date:
11 September, 2018;
A Semantic Framework for the Security Analysis of Ethereum smart contracts
目的:
与えられた論文は、Ethereumのスマートコントラクトにおけるトランザクション処理の正確なモデリングと実行セマンティクスの定義を目的としています。具体的には、トランザクションの各ステップにおける状態変化を正確に記述し、スマートコントラクトの動作を理解しやすくすることを目指しています。
使用されたデータや情報:
この論文では、Ethereumのスマートコントラクト実行環境の詳細な説明、特にメモリー使用量、ガス消費量、アカウントの状態変化などの具体的な計算方法が用いられています。また、トランザクション環境やマシンの状態など、システムの全体像を把握するための情報が整理されています。
新規性や解決できた問題:
この論文の新規性は、Ethereumのトランザクション処理における小ステップセマンティクスの導入にあります。これにより、スマートコントラクトの各命令がどのように実行され、状態がどのように変化するかをより詳細に追跡できるようになりました。また、SELFDESTRUCT命令のような特定の命令の影響を明確にすることで、セキュリティの向上にも寄与しています。
未解決問題:
将来的には、スマートコントラクトのさらなる最適化や、より効率的なガス消費のモデルを開発することが挙げられます。また、新しいタイプのトランザクションや命令が導入された場合に、これらのセマンティクスをどのように拡張するかも重要な課題です。さらに、実際のトランザクションデータを用いた実証研究を行い、モデルの精度を向上させることも求められています。
url:
https://arxiv.org/abs/1802.08660
title:
A Semantic Framework for the Security Analysis of Ethereum smart contracts
authors:
Ilya Grishchenko, Matteo Maffei, Clara Schneidewind
date:
23 April, 2018;
Static Contract Simplification
目的:
この論文では、契約の違反が発生した場合に責任を追及するための「blame」の概念を使用して、プログラム中の異なる部分がどのように相互作用して責任を負うかを詳細に分析することを目的としています。具体的には、様々な契約違反がどのように処理され、それに対する責任がどのように割り当てられるかを明確にすることを目指しています。
使用されたデータや情報:
この論文では、プログラムの構造を詳細に分析するために、制約リストと呼ばれるデータ構造を使用しています。これには、関数契約、交差契約、統合契約など、さまざまなタイプの契約が含まれており、それぞれがプログラムの特定の部分に対する要件を定義しています。また、これらの契約がどのように評価され、満たされるか、または違反されるかについての詳細なルールが定義されています。
新規性や解決できた問題:
この論文の新規性は、異なる契約タイプの相互作用を詳細に分析し、それによって発生する「blame」の割り当てを明確にする点にあります。これにより、プログラムのどの部分が責任を負うべきか、そしてなぜ責任を負うべきかを理解することが容易になります。また、契約の違反が発生した場合に、どのようにして責任を追及するかについての明確なガイドラインを提供しています。
未解決問題:
将来的には、より複雑なプログラム構造や、異なるプログラミング言語やパラダイムにおける契約の概念の適用について検討する必要があります。また、契約違反の自動検出や修正に関する研究も、さらに発展させる余地があります。さらに、実際のプログラム運用における契約の適用や管理に関する実用的な問題も解決する必要があります。
url:
https://arxiv.org/abs/1703.10331
title:
Static Contract Simplification
authors:
Matthias Keil, Peter Thiemann
date:
30 March, 2017;
Automated Fixing of Programs with Contracts
目的:
与えられた論文の主な目的は、オブジェクト指向設計におけるオブジェクトの状態を記述するために、ブール型クエリを利用してプログラムの状態空間を分割する方法を提案することです。これにより、テストやその他のアプリケーションでの効果的な状態の管理が可能になります。
使用したデータや情報:
この研究では、プログラムのテキストから抽出された式や、失敗したルーティンや契約条項から得られる情報を利用しています。具体的には、ルーティンの本文や契約条項に現れるすべての式を分析し、それらを組み合わせて新たなブール型述語を構築しています。
新規性や解決できた問題:
この研究の新規性は、引数なしのクエリを使用してオブジェクトの状態を絶対的に記述し、プログラムの状態空間を効果的に分割する方法を提案した点にあります。これにより、オブジェクト指向設計において重要なクラスのプロパティをモデル化することができ、テストやその他のアプリケーションでの使用が容易になります。
未解決問題:
将来的には、さらに多くのオブジェクト型や状況に対して、この方法を拡張適用する必要があります。また、異なるプログラミング言語や環境での効果的な適用方法についても研究が必要です。さらに、生成された述語の有効性を評価し、より効率的な述語生成アルゴリズムの開発も求められています。
url:
https://arxiv.org/abs/1403.1117
title:
Automated Fixing of Programs with Contracts
authors:
Yu Pei, Carlo A. Furia, Martin Nordio, Yi Wei, Bertrand Meyer, Andreas Zeller
date:
25 April, 2014;
Multi-representation d'une ontologie : OWL, bases de donnees, systèmes de types et d'objets
目的:
本論文では、オントロジーの多様な表現方法について検討し、オントロジーの進化を考慮に入れた上で、異なるパラダイム（OWL、タイプシステム、オブジェクト、データベース）を利用して同一のオントロジーを表現する方法を調査しています。また、これらの概念間の距離が小さいことを観察し、オントロジーとその記述言語が他のコンピュータサイエンス領域からの概念を取り入れることの利点を探求しています。
使用したデータや情報:
本研究では、OWLを用いたオントロジーの具体例を示し、その後でタイプシステム、オブジェクト指向言語、データベースといった異なるパラダイムを用いてオントロジーを表現する方法について検討しています。これにより、各表現方法の特性と限界を明らかにし、オントロジーの進化に伴う影響を評価しています。
新規性や解決できた問題:
この研究の新規性は、オントロジーを異なるパラダイムを用いて表現することで、オントロジーの柔軟性と適用範囲を拡大する方法を探る点にあります。具体的には、オントロジーの進化を踏まえた際の各表現方法の適応性や問題点を明らかにし、それぞれの表現方法がオントロジーの表現にどのように寄与するかを示しています。解決できた問題としては、オントロジーが変化する際に、その変化を各パラダイムがどのように取り扱うかを示し、多様な表現方法の利点と制限を議論しました。
未解決問題:
将来的には、異なるパラダイムを統合することで、より高度なオントロジー表現方法を開発する必要があります。また、オントロジーの進化に伴うデータの一貫性や整合性を保つためのより効果的なメカニズムの開発も求められています。さらに、実際のアプリケーションでのオントロジーの適用事例を増やし、その有効性を検証することも重要な課題です。
url:
https://arxiv.org/abs/1104.2982
title:
Multi-representation d'une ontologie : OWL, bases de donnees, systèmes de types et d'objets
authors:
Mireille Arnoux, Thierry Despeyroux
date:
15 April, 2011;
Edit and verify
目的:
この研究の主な目的は、拡張静的検証（ESC）における自動定理証明の使用パターンを説明し、そのパフォーマンスを改善するための二つのアプローチを提案することです。特に、式の編集と検証のプロセスを自動化し、既に証明された部分を再利用することで、全体の検証プロセスを効率化することを目指しています。
使用したデータや情報:
この研究では、Javaメソッドの日付計算に関する具体的な例（dayOfYearメソッド）を用いて、様々な編集操作が定理証明のパフォーマンスにどのように影響するかを分析しています。具体的には、メソッドの事後条件を強化する編集や、メソッド内に新たなアサーションを追加する編集などが行われ、それぞれの編集が検証時間にどのような影響を与えるかが測定されています。
新規性や解決できた問題:
この研究の新規性は、特にプルーニングアルゴリズムと呼ばれる新しいアプローチを導入した点にあります。このアルゴリズムは、変更された部分のみを再検証することで、不必要な計算を削減し、全体の検証プロセスを高速化します。また、このアルゴリズムは、既存のESC/Java2ツールに対して変更を加えることなく適用可能であり、その適用性と効率性が実証されました。
未解決問題:
未解決の問題としては、プルーニングアルゴリズムのさらなる最適化が挙げられます。現在のアルゴリズムでは、特定のケースでのパフォーマンス向上が見られるものの、全てのシナリオで最適なパフォーマンスを発揮するわけではありません。将来的には、より多様なプログラミングパターンや複雑なコード構造に対しても効率良く動作するようなアルゴリズムの改良が求められます。また、形式的なパフォーマンス分析を行い、アルゴリズムの効果をより詳細に評価することも重要です。
url:
https://arxiv.org/abs/0708.0713
title:
Edit and verify
authors:
Radu Grigore, Michał Moskal
date:
6 August, 2007;
Formal Modeling in a Commercial Setting: A Case Study
目的:
この研究の主な目的は、自然言語仕様から詳細なテストケースを導出するために、システムの振る舞いをモデル化することです。また、より詳細なモデルを使用することで自然言語仕様の問題点を特定することも目指しています。
使用したデータや情報:
この研究では、自然言語で記述された80ページに及ぶ仕様書を使用しています。特に、パスワードチェックコンポーネントに関する5ページの仕様を詳細に分析しており、SDL（Specification and Description Language）を用いてモデル化しています。
新規性や解決できた問題:
新規性としては、SDLを用いて複雑なテレコムアプリケーションの振る舞いをモデル化し、実際のシステムとの環境とのインタラクションをMSC（Message Sequence Chart）で記録する方法を採用しています。これにより、形式的なアプローチを通じてテストケースの内容とカバレッジに自信を持つことができました。また、自然言語仕様のあいまいさや不完全さを明らかにし、それを改善する手助けとなりました。
未解決問題:
自動化されたテストケース導出の実現が挙げられます。現在は手動でSDLモデルをアニメーション化してMSCを記録していますが、このプロセスの自動化により、より効率的かつ広範囲にわたるテストが可能になるでしょう。また、モデルの複雑さを管理しつつ、さらに詳細なテストケースを導出する方法の開発も必要です。
url:
https://arxiv.org/abs/cs/9906032
title:
Formal Modeling in a Commercial Setting: A Case Study
authors:
A. Wong, M. Chechik
date:
29 June, 1999;
この記事が気に入ったらサポートをしてみませんか？