概要

多くの端末がネットワークに繋がるようになるにつれ,スイッチなどを含むネットワークファンクションの重要性が増している.スイッチはネットワークとユーザーの端末を繋ぐ機能があり,管理が容易なソフトウェアスイッチにおいても安全なソフトウェアスイッチの設計は重要である.しかし,ソフトウェアスイッチではしばしばバグやエラーなどにより通信障害が発生するため,動作の検証が必要である.Coq は定理証明支援系言語であり,定義された関数や式の正しさをプログラム上で証明可能である.本論文では,パケットハンドリング機構の一つである Raw Socket を用いて各端末の MAC アドレスを管理するソフトウェアスイッチの設計と実装を行った.特に,MAC アドレスの管理については Coq で動きを検証した.この結果,形式的に検証されたソフトウェアスイッチの基礎実装を実現した.

Top