|
従来，プログラム理論やソフトウェア工学の分野においては，ソフトウェアの正しさを論理的に検証する手法（形式手法，数理的技法とも呼ばれる）が研究されており，当該分野の中心テーマの一つとなっている．なかでも，暗号プロトコルを対象とした形式手法が世界的な注目を集めており，秘匿性（盗聴した暗号文をどのように組み合わせても平文を取り出せないこと）などが研究されている．
本研究では，セキュリティの重要な性質である「プライバシ」を，形式手法を用いて自動検証する技術を確立することで，安全・安心なICT社会の構築に貢献することを目指している．本年度は，プライバシの条件（トレース匿名性）およびその前提条件を自動検証するために，I/O-オートマトンモデルとして記述されたふたつの分散システムのトレース一致の十分条件（フォワードシミュレーション）を，SAT-ソルバ上で記述した．これは，昨年度に行った「トレース包含の条件の記述」の拡張となっている．さらに，拡張された電話システムを例題として，ふたつのシステムのトレース一致の検証実験を行った．プライバシは「分散システム」と「その分散システムに対して自明にプライバシが成り立つシステム」の間のトレース一致として，定式化することができる．すなわち，ふたつのシステムのトレース一致の条件をSAT-ソルバで自動検証する方法を明らかにすることを通じて，本研究では，プライバシの全自動検証の基礎づけを行うことができた．
プライバシの検証を行った分散システム仕様は，さまざまなプログラミング言語を用いて実装されることになる．本研究では，実装に向けた試みとして，I/O-オートマトンモデルで記述されたシステムの仕様を，直接分散環境下で実装する手法についても検討した．また，組み込みシステムを実装するための言語処理系について，試作を行った．
|
