フォーマル検証、使っていますか?

皆さん、フォーマル検証、使っていますか?

最近、「フォーマル検証」という言葉を耳にする、あるいは口にする機会が増えてきた――そのように感じている方も、多いのではないでしょうか。EDAベンダ各社のプレスリリース等を眺めてみると、フォーマル検証を巡る各社の技術動向は、ここ数年で着実な進歩を遂げているように感じられます。アプリケーションが充実し、適用範囲が広がったことで、フォーマル検証への注目度は高まっており、各社のセミナーやユーザー発表も盛り上がりを見せているようです。

例えば、フォーマル検証の応用として近年期待されている分野のひとつに、セキュリティ検証があります。IoTデバイスを狙う「Mirai」ウィルスが猛威を振るったことは記憶に新しいですが、利用できるリソースに限りがあるIoTデバイスにおいては、ソフトウェアに加え、ハードウェアレベルでのセキュリティ対策の重要性が叫ばれています。

出展:IPA

人間が入力パターンを与えることなく、あらゆる入力を考慮して仕様違反の有無を網羅検証するフォーマル検証の手法は、時に想定外のセキュリティパスを発見し、脆弱性の流出を防いでくれます。設計者の「想定外」を突くのがハッカーの攻撃手段なので、このような検証の手法は非常に強力です。そして、ひとたびセキュリティ検証のプロパティが「証明」されれば、それはチップ内に不正アクセスを行う経路が、論理的に一切存在しないことを意味します。

 

さて、セキュリティ検証の話はひとまず横に置いて、最初の質問に戻ります。フォーマル検証?便利だよね、もちろん活用しているよ、というエンジニアの皆さん。今度は少しだけ、質問の仕方を変えてみます。

フォーマル検証、使いこなせていますか?

最初の質問にはYESと即答された方でも、こちらの質問にためらわずYESと言える方は少ないのではないかと思います。「使いこなす」。厄介な言葉です。スマホを使いこなす。Excelを使いこなす。日本語を使いこなす。一体どこまでマスターすれば、「使いこなした」と言えるのでしょうか。もし、「そのツールが持つ全ての機能を自在に使えるようになる」が「使いこなす」の定義なら(手元の辞書を引くと概ねそのようなことが書かれていますが…)、この世にスマートフォンを使いこなしている人間など一人もいません。

携帯電話が単なる電話端末からフィーチャ―フォン(ガラケー)、スマートフォンと進化していくにつれて、使いこなしていると胸を張って言える人が少なくなったのと同じように、フォーマル検証ツールも機能や性能が向上するのに反比例して、使いこなせている、と実感している人は減っているのではないでしょうか。ツールでできることが多くなると、使う側のツールへの期待値も上がります。上で例に挙げたセキュリティ検証も、確かに適用効果は高そうだし、興味深いアプリケーションです。しかし、実際のところ、どう適用すればよいかわからない、適用してみたけど理論通りには上手くいかない(もしかして:収束しない)、と思われている方、いませんでしょうか?ピンとこない方は、「セキュリティ検証」を他の単語に置き換えてみてください。

実現したいことがあって、それに必要なピースも揃っているはずなのに、どうすれば実現できるのかわからない…そんなもどかしさを感じたことはありませんか?

Design Solution Forum 2017では、そんな迷えるフォーマル検証ユーザーのためのディスカッション企画を用意します。EDAベンダ各社のフォーマル検証ツール担当者を特別講師陣に迎え、ツールの持つ多彩なアプリケーションをより活用するアイデアや、ツール性能を引き出すためのテクニックなど、様々なトピックについてざっくばらんに議論・情報共有できる場にしたいと考えています。かつてはフォーマル検証をほとんど使いこなせていた、古参ユーザーの方。これから使いこなしていきたいフォーマル初~中級者の方。あなたのお悩みや体験談をお聞かせください。もちろん、今でも使いこなせている!と自負されている方も大歓迎です。この機会を是非ご活用ください。

「フォーマル検証ディスカッション」企画概要・参加者事前登録はこちら

文:Design Solution Forum 2017 実行委員 酒井 皓太

コメントを残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です

*