 |
| ポルトガル ブラガにて |
|
|
河辺 義信（かわべ よしのぶ） |
|
こんにちは！
コンピュータプログラムの形式モデリングや検証に興味を持っています．
とくに最近は，トラスト計算やプロトコルのセキュリティ検証に興味があります．
|
|
研究分野
| SNS上でみつけたこの救助要請は，はたして本物だろうか？ |
| どうしたら正しく動くプログラムを作れるのだろう？ |
| この通信プロトコルは本当に安全なんだろうか？ どうして安全と言えるのだろう？ |
こうした疑問に答えるのが，さまざまなソフトウェアシステムの正しさを証明する手法，フォーマルメソッド（形式手法）です．
たとえば，セキュリティプロトコルから個人情報漏洩（＝バグの一種とみなせます）がないことを，フォーマルメソッドを使って証明することができます．
私の研究は 人やメッセージの信用 (トラスト)・セキュリティプロトコル・Webサービス・分散システム の形式検証に関するもので，これまで次のような研究テーマに関わってきました：
- トラスト計算：
災害発生直後に，SNSで次のようなメッセージを見つけたとしましょう．
緊急を要する「救助要請」は，このうちどれだと思いますか？
| 「豪雨災害の影響で，明日は営業をお休みします」 |
| 「どうかお気をつけて」 |
| 「現在地は○○市××町1-2-3です．水がそこまで迫っています．誰か助けて！」 |
災害時に交換される膨大なメッセージの中から，どのメッセージが「救助要請として信じられるか」を正しく評価し，メッセージを選別してファーストレスポンダ (消防士・警察官など) に届けることが大切です．
私たちは，メッセージ等に対する信用度 (トラスト) を適切に計算し，推論・予測する技術を生み出すべく，研究しています．
トラストの表現方法としては，心理学やファジィ論理の結果を採り入れた新たな表現法 (二次元的トラスト値) を開発しました．
また，プログラム理論や分散アルゴリズム理論で扱われる性質をトラスト計算に適用することで「信用できない状態に至らない」や「いつか信じてもらえるようになる」といった性質をうまく検証できないか，研究を進めています．
- セキュリティ検証：
インターネットでは，個人情報の漏洩は許されません．
たとえば電子投票システムなどを考えてみますと，「誰が誰に投票したか」が第三者に知られないようになっていなければなりません．
この課題を解決するため，私たちは，セキュリティプロトコルの匿名性をフォーマルに検証する手法を開発しました．
また，ケーススタディとして，FOOと呼ばれる電子投票プロトコルの匿名性検証を行いました．
この検証では，数学の問題を解くシステムである「定理証明器」を使い（証明スクリプトはこちら），実際のセキュリティプロトコルにこの手法が十分適用可能であることを確認しました．
- プロセス代数にもとづくネットワークプログラミング言語：
プロセス代数π-計算とは，通信プロセスをある種の数式として扱う理論です．
私たちは，π-計算に基づくネットワークプログラミングシステムNepiを開発しました．
Nepiを使うことで，π-計算の数式として通信プロセスを記述し，正しさを検証し，さらにネットワーク上で直接実行することができます．
また，私たちは，Nepi処理系の分散実装が正しいものであることをフォーマルに証明しました．
この証明でも，定理証明器を使っています．
- 順序ソート項書換え系：
順序ソート項書換え系とは型と部分型の概念を備えた項書換え系で，CafeOBJ，CASL，Maudeなどの仕様記述言語や定理証明系のベースになっています．
私たちは，順序ソート項書換え系の合流性や停止性を証明するための手法を考案し，さらにモジュラリティの証明などに適用しました．
また，これとは別に，高階関数を扱うための変換であるカリー化を，順序ソート項書換え系に導入しています．
最近の業績
- Y. Tsukada, K. Mano, H. Sakurada and Y. Kawabe, "Anonymity, privacy, onymity, and identity: a modal logic approach",
Transactions on Data Privacy, to appear.
- K. Mano, Y. Kawabe, H. Sakurada and Y. Tsukada, "Role interchange for anonymity and privacy of voting",
Journal of Logic and Computation, to appear.
- I. Hasuo, Y. Kawabe and H. Sakurada, "Probabilistic anomymity via coalgebraic simulations",
Theoretical Computer Science, volume 411, No. 22-24, pages 2239-2259, 2010.
- Y. Kawabe, N. Ito and N. Ishii, "On formal modeling of TOPPERS embedded software",
8th International Conference on Software Engineering Research, Management and Applications (SERA '10), pages 93-100. IEEE Computer Society Press, 2010.
- Y. Tsukada, K. Mano, H. Sakurada and Y. Kawabe, "Anonymity, privacy, onymity and identity: a modal logic approach",
IEEE International Conference on Privacy, Security, Risk and Trust (PASSAT-09), pages 42-51. IEEE Computer Society Press, 2009.
- Y. Kawabe, K. Mano, H. Sakurada and Y. Tsukada, "On backward-style anonymity verification",
IEICE Trans., volume E91-A, No. 9, pages 2597-2606, 2008.
- Y. Kawabe and H. Sakurada, "An adversary model for simulation-based anonymity proof",
IEICE Trans., volume E91-A, No. 4, pages 1112-1120, 2008.
- 真野 健, 櫻田 英樹, 河辺 義信, 塚田 恭章, "ゲーム列による安全性証明の形式化と自動化",
応用数理, volume 17, No. 4, pages 38-46, 2007.
- Y. Kawabe and H. Sakurada, "A formal approach to designing anonymous software",
5th International Conference on Software Engineering Research, Management and Applications (SERA '07), pages 203-212. IEEE Computer Society Press, 2007.
- I. Hasuo and Y. Kawabe, "Probabilistic anomymity via coalgebraic simulations",
16th European Symposium on Programming (ESOP '07), Lecture Notes in Computer Science, volume 4421, pages 379-394. Springer-Verlag, 2007.
- Y. Kawabe, K. Mano, H. Sakurada and Y. Tsukada, "Theorem-proving anonymity of infinite state systems",
Information Processing Letters, volume 101, No. 1, pages 46-51, 2007.
- Y. Kawabe, K. Mano, H. Sakurada and Y. Tsukada, "Backward simulations for anonymity",
6th International IFIP WG 1.7 Workshop on Issues in the Theory of Security (WITS '06), pages 206-220.
- Y. Kawabe and K. Mano, "Verifying trace equivalence of a shared-memory-style communication system",
IEICE Trans., volume E88-A, No. 4, pages 915-922, 2005.
- A. Mizuno, K. Mano, Y. Kawabe, H. Kuwabara, S. Yuen and K.
Agusa, "Name-passing style GUI programming in the pi-calculus-based
network language Nepi",
Electronic Notes in Theoretical Computer Science, volume 139, pages 145-168. Elsevier Science, 2005.
- Y. Kawabe, K. Mano, E. Horita and K. Kogure, "Name creation implements restriction in the pi-calculus",
Systems and Computers in Japan, volume 36, No. 2, pages 78-91, 2005.
- K. Mano and Y. Kawabe, "The Nepi network programming system: a programming environment for distributed systems",
3rd IEEE International Symposium on Network Computing and Applications (NCA '04), pages 287-292. IEEE Computer Society Press, 2004.
連絡先住所
〒470-0392 愛知県豊田市八草町八千草1247
愛知工業大学 情報科学部 情報科学科
Email: kawabe [at] aitech.ac.jp
Updated: May 4, 2022