|
まず不変性だけでなく、その一般化である安全性の検証を行うために、安全性をBuchiオートマトンで定式化した。安全性を帰納法により証明するため、証明義務の定式化を行い、不動点帰納法で実装するための手続きを定義した。また、不変性に対する不動点帰納法で行っていた補題発見法が、同様に適用できることを確認した。と同時に、残念ながら安全性に対する補題発見は、多くの場合、組み合わせ爆発により計算量が増大しやすいことも明らかになった。同様の問題は、不変性検証においても起こりうるものであり、実際、NSLPKプロトコルを不変性検証器で検証したときに、認証性と秘匿性を同時に与えたときは、証明に成功したものの、認証性のみでは同様の原因で証明に失敗した。しかしながら定式化した結果から、不変性に対する証明法から自然に安全性に対する証明法へ拡張できることも確認できたため、まず不変性に対して、SMTによる検証能力の向上と、並列化による検証の効率化を図る方針へと変更した。
変更した方針に基づいて実装を開始した。多くのSMTの実装では、充足可能性を検査するのに必要最低限のインタフェースしか提供しておらず、最弱事前条件計算に利用できなかった。幸いソースコードが公開されたSMTの実装としてCVC3を得ることができたため、CVC3を利用することにした。SMTを用いて不動点帰納法を実現することは容易であると期待したが、充足可能性を検査するための最適化と、最弱事前条件を計算するための最適化は大きく異なり、予想以上にSMTの振る舞いを変更する必要があることが明らかになった。CVC3上で簡易的な不動点帰納法を実装したものの、この最適化の違いにより最弱事前条件を求めることができなかった。この最適化を抑制するためには、CVC3をより詳細に理解する必要があり、現状ではこの調査を行っている。
またBuchiオートマトンで安全性を定式化する過程で、安全性・余安全性に対する全反例を、有限オートマトンに対する手続きにより、効率的に求められることを明らかにし、システム検証の科学技術シンポジウムにて発表した。
|
