データベースを用いるWebアプリケーション

Fixpoint Lemma Theorem Proof Qed intro intros case unfold fold induction reflexivity rewrite elim inversion apply assumption

お客さんがWebブラウザを使って、入力項目をデータベースに登録したり、データベースからデータを取ってきたりする仕組みは、多くの場所に存在するだろう。
このような仕組みは比較的簡単に提供することができ、かつ、利用する人の生活を便利にしてくれる。インターネットでお買い物ができたり、アパートを探したり、はてな日記みたいに日記を書いて公開したりすることができるのも、このような仕組みのおかげだ。
しかし、便利さの裏に危険性が伴っていることをご存じだろうか？　悪意のあるユーザからの思わぬ入力によって、提供者のデータベースを破壊されたり、他のユーザの個人情報が公開されたりするかもしれない。例えば、お買い物サイトなどでは、利用者のクレジット番号や銀行口座番号が不特定多数に知られてしまうかもしれないのだ。
この危険性を回避するため多くのシステムでは、運用する前に十分テストを行っているだろう。でもテストだけでよいのだろうか？
世の中には白箱テストや黒箱テストなどいろいろなテストの方法が考えられており、実践されているが、一般にテストだけでは100パーセント大丈夫なんて保証できないからだ。
今回はCoqを使ってデータベースに入力する文字列のエンコード処理を形式化し、証明した。

Fixpoint encode (esc:ascii)(keys:list ascii)(s:string){struct s} : string :=
  match s with
  | EmptyString => EmptyString
  | String hd tl =>
      match in_dec_ascii hd keys with
      | left _ => String esc (String hd (encode esc keys tl))
      | right _  => String hd (encode esc keys tl)
      end
  end.

Lemma l : forall (k a:ascii) (s:string),
  In k keys ->  not (IsMember k (escape esc (encode esc keys s))) ->
   k <> a -> not (IsMember k (escape esc (encode esc keys (String a s)))).
Proof.
intros.
unfold encode in |- *.
case (in_dec_ascii a keys).
 intro; fold encode in |- *.
   unfold escape in |- *.
   case (ascii_dec esc esc).
  intro; fold escape in |- *.
    assumption.
  intro neq; elim neq; reflexivity.
 intro; fold encode in |- *.
   unfold escape in |- *.
   case (ascii_dec esc a).
  intro eq; rewrite <- eq in n.
    elim n; apply HH.
  intro neq; fold escape in |- *.
    intro.
    inversion H2.
   elim H1; assumption.
   elim H0; assumption.
Qed.

Theorem m : forall (k:ascii)(s:string), 
  List.In k keys -> not (IsMember k (escape esc (encode esc keys s))).
Proof.
intros.
induction s.
 intro.
   unfold encode in H0.
   unfold escape in H0.
   inversion H0.
 case (ascii_dec k a).
  intro eq; rewrite <- eq.
    unfold encode in |- *.
    unfold in_dec_ascii in |- *.
    case (In_dec ascii_dec k keys).
   intro; fold encode in |- *.
     unfold escape in |- *.
     case (ascii_dec esc esc).
    intro; fold escape in |- *.
      apply IHs.
    intro neq; elim neq; reflexivity.
   intro not; elim not; assumption.
  apply l.
   assumption.
   assumption.
Qed.

今回は非常に簡単で些細なことに思えるかもしれないが、このような些細なことの積み重ねでプログラムの安全性や信頼性が増していくと思っている。
世の中のすべてのシステムが、少しでも安全に利用できるようになっていってほしいものだ。