さきがけ研究の一環として、JAXA （宇宙航空研究開発機構）の小林努博士に来てもらい Formal Method について講演して頂きました。

Formal Method とはシステムの性質を数学的に証明する手法です。 Spectre などのサイドチャネル攻撃は対策手法が出てはそれをすり抜ける攻撃が現れ…の繰り返しです。 そこに一石を投じるものとして以下の論文ではあるキャッシュ構造がサイドチャネル攻撃を「完全に防げている」ことを Formal Method で示そうとしており、 我々のさきがけ研究でも類似のことができないか考えています。

Ke Jiang, Tianwei Zhang, David Sanán, Yongwang Zhao, Yang Liu: “A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures”, ICFEM’22

講演では「証明とは何か」といった基本的な考え方から実際の定理証明支援系でできることなどを幅広くお話頂き、 上記論文の意義も理解できるようになるなど大変有意義な会でした。