”形式的検証”と”組み合わせ爆発”から学ぶ入力バリデーション

形式的検証とは

形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである

英語ではFormal Verificationとされ

formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

と説明されています。形式手法として紹介されることも多いです。

参考： 形式検証入門 （PDF）

形式的検証は、記述として検証する方法から数学的にプログラムが正しく実行されることを検証する仕組みまで含みます。数学的な形式的検証では、可能な限り、全ての状態を検証できるようにしてプログラムが正しく実行できることの証明を試みます。

参考：ソフトウエアは硬い （日経XTECHの記事）

契約プログラミング（契約による設計 – Design by Contract, DbC）も形式的検証の１つの方法です。

形式検証の仕組みを知ると、厳格な入力バリデーションが無いと”組み合わせ爆発”により、誤作動（≒ セキュリティ問題）の確率も爆発的に増えることが解ります。

形式的検証の歴史

形式的検証の歴史はとても古くBC1800年ころ¹のバビロニアンの時代まで遡ります。BC400年ころにはPlatoも研究¹していたようです。もっと身近な20世紀前半の1930年頃には「コンピューター」の開発に取り組んでいたアラン・チューリング、フォン・ノイマンらにより盛んに研究¹されるようになります。

形式的手法の研究と実践は既に50、60年代の欧州では盛んだった²そうです。コンピューターシステムエンジニアリングに於ける形式的検証は70年代に欧州を中心に仕様記述方法として発展し、80年代にモデル検査手法も開発されます。1990年代にはモデル検査と手法ツールの「SPIN」「SMV」「Uppaal」などが無償で公開されます。モデル検査手法のBDD（Binary Decision Diagram）は状態を0と1で表せる為、コンピューターハードウェア設計と相性がよくデジタル回路設計で実用的に利用されてきました。ソフトウェアの分野ではPartial Order Reductionによる通信プロトコルの検証などが行われています。

ソフトウェア分野では出遅れていた感が拭えない日本でしたが、2000年代にUMLが流行り出した頃、形式的検証もモデルやコードを検証する仕組みとして一部の企業では導入されています。SONY（フェリカネットワークス）がモバイルFeliCaを開発した際には仕様を10万行にも及ぶVDM++を記述し、仕様段階で440件のバグを修正した³としています。

あまり聞きなれない方も多いかもしれない形式的検証ですが、契約プログラミング（契約による設計）はソフトウェア開発者の多くが知っていると思います。これも形式的検証手法の一種です。

形式的検証は、デジタル回路設計に於ては確立した実用的な手法であり、ソフトウェア設計でも実用的に使われています。

形式的検証の入門

先に参考資料として紹介済みの形式検証入門 を借りて簡単に紹介します。

契約プログラミング ⁴を知っている方なら「基本的には契約プログラミングと同じだ」と理解ると思います。条件（ASSERT）が成立することを検証（確認）することにより、プログラムが正しく実行されることを検証（証明）できるようにすること形式検証では求めます。

プログラムが正しく実行されることを検証（証明）するには、全ての状態（入力を処理の結果）を検証（証明）しなければなりません。

基本的な考え方としては次の図のような検証を行い、正しく実行されることを証明します。

推論による証明は”全てのケースを総当たりせず”に正しく実行を可能であることを証明します。

生成による証明は”全てのケースを総当たりして”、正しく実行を可能であることを証明します。

全てのコードを推論によって簡単に「正しさを証明」できるなら良いのですが、現実のプログラムはそういうモノではありません。もし簡単に推論により証明できるなら既に、バグがないソフトウェアを保証するツール、が世の中の常識になっているでしょう。

全てのケースを総当たりして正しさを検証せざるを得ない、が現状です。このため実際に総当たり的に検証する、といったアプローチが取られています。

※ Unitテストも”総当たり型”の検証方法ですが、形式的検証とは考えられていません。

形式検証で発生する組み合わせ爆発問題

全てのケースを総当たりして正しさを検証せざるを得ない、このため実際に総当たり的に検証する、といっても簡単なプログラムならまだしも実用的なプログラムになると、「全てのケースを総当たり」する「組み合わせ」は簡単に膨大な数になります。

例えば、ある入力が32bit整数だとします。この場合、-2^31 〜 2^31-1 まで、約43億のパターンがあります。別の32bit整数入力と一緒に処理されるとすると

• 43億 x 43億

になり、およそ1.8e+19のパターンを総当たりすることになります。既に膨大な数ですが、実用的なプログラムの入力は32bit整数が2つではありません。整数のみでなく文字列やもっと複雑な構造体的なデータを当たり前に取り扱います。

ごく単純なケースを少し考えただけで、

• まともに真の総当たりで検証することは不可能

と解ります。計算できない程の大量のパターンが爆発的に発生する問題が「組み合わせ爆発」問題です。実用的なプログラムの複雑性だと簡単に「組み合わせ爆発」が発生します。

このため、総当たり的な形式検証では「組み合わせ爆発」が起きない様、仕組み的な工夫はもちろん、必要でない入力は徹底的に廃除します。

例えば、先ほどの32bit整数2つを入力として持つプログラムは”0〜100″までの値しか取らない場合、”0〜100″だけの入力を考えます。この場合、組み合わせ数は

• 100 x 100

たったの1万になり容易に検証可能な組み合わせ数になります。

※ 実際に形式検証で処理の正しさを証明しようとすると、パラメーターのパターンの掛け算になるので、個々のパラメーターの範囲がかなり絞られていてもかなり簡単に「組み合わせ爆発」が起きます。

実際にはプログラムの実行経路は多数の組み合わせがあります。一つ一つの関数（ローレベルのライブラリなども含む）が受け入れる変数の範囲は膨大だからです。それが何千、何万も存在します。”無効な入力”の動作まで含めて”正しく処理”しよう、とするのは無謀と言えます。

参考： 経路の組み合わせ爆発

プログラムの場合、経路の組み合わせに加え、”状態の組み合わせ”がある。この為、プログラムでは簡単に組み合わせ爆発が発生する。

プログラムに与える入力値は厳格に入力バリデーションする

プログラムに与える入力値は厳格に入力バリデーションする、これはセキュアコーディングの第1原則です。

プログラムが受け入れるべきでない入力値に対して、正しく動作することを証明しようとすること、は無駄でしかありません。仕様として”絶対に正しく実行できない”ことが判っているからです。こういった不要な値（≒クライアントやUIが送ってこれない値 ⁵ ）は、形式的検証でも、実際のプログラムでも廃除しなければなりません。

セキュアコーディングの入力バリデーションで廃除される入力は、上記の図の赤い部分（不正な入力値）です。

そして形式的検証で「本来検証の必要がないパターンを生む入力」とは「入力バリデーションで廃除される入力」です。

「本来検証の必要がないパターンを生む入力」（不正な入力）、をプログラム中の処理に渡す事は全くの無駄であるだけでなく、不要な複雑性を生み、不必要なバグやセキュリティ問題の原因となります。

参考：バリデーションには3種類のバリデーションがある – よく入力とロジックのバリデーションが混同されています。勘違いしないよう注意。セキュアなアプリケーション構造のイメージ図は以下のようになります。

参考：

バリデーションには3種類のバリデーションがある 〜 セキュアなアプリケーションの構造 〜

エンジニア必須の概念 – 契約による設計と信頼境界線

まとめ

厳格な入力バリデーションは形式的検証の主要な要素ではありませんが、形式的検証には絶対に欠かせない前提条件です。

他のプログラムの複雑な要素と比べれば、厳格に入力バリデーションを行うことは簡単なことです。厳格な入力バリデーションをやらずに「プログラムの正しさを証明」しようとしても、原理的に無理です。

• 原理：コンピュータは妥当な入力でしか正しく動作できない

この原理は変えられません。整数として「1234 + “apple”」の正しい答えは求めようがありません。⁶

「脆弱性があったら、その脆弱性だけに着目して局所的に対策するの良い（入力検証はオマケ）」とする考え方もあります。しかし、この考え方では正しく動作することを網羅的に検証し証明することは非常に困難です。適切な入力検証がない場合、不具合を発生させる入力の組み合わせ数はコンピューターで処理することさえ不可能なほど膨大になります。これを漏れ無く人間が管理することは不可能です。更に、正しく動作できなくなる状況、を完全に解消することも不可能です。 ^{7 8 9}

「見つけた脆弱性をその場限り、場当たり的、尚かつ入力バリデーションなし、で一つ一つ潰していく」はベストプラクティスどころか、非論理的／非現実的なアンチプラクティスです。^{7 10}

入力バリデーションは、非常に重要ですが、セキュアなソフトウェア構築のほんの入り口に過ぎません。しかし、入り口から間違えてしまうと出口が遠くなるばかりです。⁸

アプリケーションレベルでの入力バリデーションはセキュアなソフトウェア開発の基礎の基礎ですが、入力バリデーションがセキュリティ対策ではない、と勘違いさせられている開発者も少なくないと思います。10年以上も情報セキュリティ機関であるIPAが誤ったセキュアプログラミングを啓蒙し続けた影響は小さくないでしょう。

参考：IPAは基礎的誤りを明示し、正しい原則を開発者に啓蒙すべき

科学的なアプローチのセキュリティの基本概念は難しくありません。基本概念を知っているだけでも格段にセキュアなソフトウェアが作れるようになります。簡単な説明でしたが、形式検証の仕組みを知ると、厳格な入力バリデーションを行うと問題となる”組み合わせ”が大幅に現状するため、誤作動（≒ セキュリティ問題）の可能性が大幅に減少することが理解ったと思います。

参考：ほぼ全てのインジェクション攻撃を無効化／防止する入力バリデーション

科学的、論理的に正しいソフトウェアセキュリティの構築には形式的検証の概念が役立ちます！基本的な考え方は簡単です！

参考： セキュリティ対策が論理的に正しいか検証する方法