タグスイッチネットワークのモデル検査による漏曳検査

• Item type: SIG Technical Reports(1)
• 公開日: 2004-05-21
• タイトル: タグスイッチネットワークのモデル検査による漏曳検査
• タイトル / 言語: en
• タイトル: Model Checking Configurations for Tag - Switched Computer Networks
• 言語: eng
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 日本電信電話株式会社NTTコミュニケーション科学基礎研究所
• 著者所属(英): en
• 著者所属(英): NTT Communication Science Laboratories, NTT Corporation
• 著者名: 櫻田, 英樹
• 著者名(英): Hideki, Sakurada
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: タグに従ってパケットが転送されるネットワークでは ノードの設定ミスにより パケットが予期しないセグメントに漏れ出したり 目的のセグメントに到達しないなどのトラブルが生じることがある.パケットの漏れ出しは特に セキュリティを脅かす問題である.本論文では タグに従ってパケットが転送されるネットワークをモデル化し モデル検査によってパケットの到達性を検査する方法について述べる.モデルは記号モデル検査のツールであるNuSMV上で実装される.この方法はノードの設定が実際に用いられる前にその正しさを確認するためや トラブルが起きたときに原因を究明するために有用である.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In tag-switched computer networks, errors in the configurations of the nodes can cause the frames to leak into unexpected segments or not to reach the destination segments. Frame leakage, in particular, can be a security problem. This paper describes a method to model tag-switched networks and check the reachability of frames by model checking. The model is implemented on NuSMV, a tool for symbolic model checking. The method is useful for checking configurations before they are activated and for analyzing the cause of trouble.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11235941
• 書誌情報: 情報処理学会研究報告コンピュータセキュリティ（CSEC）; 巻 2004, 号 54(2004-CSEC-025), p. 49-54, 発行日 2004-05-21
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会