バグの無いソフトウェアを開発するための技術：証明スコア

【ポイント】

• 証明スコアは、バグの無いソフトウェアを開発するための技術の一つとして注目されている技術
• 過去数十年に渡り研究されてきた証明スコアによる形式検証の概観をまとめた
• 証明スコアの弱点及び克服方法を示すとともに、より多くの研究者に普及させるための改善案の提案

【研究概要】

　現代社会において、ヒトの営みはデジタル技術に大きく依存しています。その傾向は、今後ますます大きくなることは疑いようがありません。デジタル技術の大半はソフトウェア（あるいはプログラム）で占められています。私たちの生活の質はソフトウェアの品質に大きく依存しているともいえます。そのため、生活の質を上げるにはソフトウェアのバグを可能な限り無くすことが不可欠です。
　バグの無いソフトウェアを開発するための技術の一つとして注目されているのが証明スコアです。北陸先端科学技術大学院大学を中心に過去数十年に渡り研究されてきたこの技術について、同大学コンピューティング科学研究領域緒方教授の研究グループなどが概観をまとめた論文を国際学術誌ACM Computing Surveysに発表しました。
　証明スコアは、ソフトウェアシステム（以降、システム）が望みの性質を満たすかどうかを、定理証明^*1に基づき形式的に検証することを可能とします。中でも証明スコアは、他の定理証明に基づく形式検証技術と異なり、プログラムのように記述できる柔軟性が優れた特徴を有しています。その一方、ヒューマンエラーが起こり得るという弱点も併せ持っています。

　また、証明スコアは、代数仕様言語と呼ばれるプログラミング言語、特にOBJファミリーの言語（OBJ3， CafeOBJ， Maude等）を用いて記述されます。証明スコアを記述するにあたり、システムと性質を代数仕様言語で記述します。証明スコアの目的は、システムが性質を満たすことを厳密に（あるいは科学的に、あるいは数学的・論理学的に）確認（形式検証）することです。

　なお、証明スコアは、1990年代に研究者ジョセフ・A・ゴーギャンによって初めて提案されました。当初は、スタック等の基本的なデータ構造にしか応用されなかったため、理論的には美しいが実用的な応用例が無いといった批判がありました。しかし、その後、北陸先端科学技術大学院大学の元教授である二木博士、緒方教授らにより、セキュリティプロトコル等の実践的な分野に応用され、この批判に応える成果が生まれました。さらに、本研究成果では、耐量子暗号プロトコル等、最新の応用例も紹介しています。

　一方で、証明スコアはヒトが書く必要があるためヒューマンエラーを避けることができないという弱点もありましたが、マドリード・コンプルテンセ大学のアドリアン・リエスコ准教授と緒方教授により開発された、証明スコアから証明支援系^*2の入力である証明スクリプトを自動生成するCiMPGというツール、および北陸先端科学技術大学院大学のトラン・ドゥオング・ディン特任助教と緒方教授により開発された、証明スコアの大半を自動生成するIPSGというツールにより、この弱点を克服しました。

　このように、証明スコアは、プログラムのように柔軟に記述できるという利点があり、かつ二つのメジャーな批判にもうまく対応してきました。しかしながら、産業界のみならずアカデミアにおいても広く普及しているとは言えないのが現状です。これに対応するには、本研究グループは、プログラムを開発する際に利用されている統合開発環境（IDE）に相当するものを証明スコア用に用意する必要があると、提案しています。IDEはプログラムの管理のためのグラフィカルでインタラクティブなサポートを提供します。証明スコア用のIDEを準備することで、より多くの研究者に証明スコアに関する研究に取り組んでもらえるようにすることが可能になると考えられます。

【論文情報】

【用語説明】

令和7年5月7日