CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コースニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

◆ サブ メニュー ◆
Web版 システム検証の事例報告集

Web版 トップ頁へ

▼ 一覧から探す
  1. 項目一覧

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 24: ソフトウェア更新システムのモデル検査器を使った安全性の検証


実施年度2005
概要 近年のコンピューターネットワークの発達に従い、そのセキュリティの確保が改 めて課題となっている。 ネットワーク上でのセキュリティを確保するためには、まずシステムの設計自体 が正しいことが必要であ る。したがって、設計上の誤りをあらかじめ発見する手法が必要とされる。形式 手法は、設計を数学的にモ デル化し、モデルが期待される性質を数学的に証明する。これにより、形式手法 は原理的にはすべての誤り を検出できる。本研究では、株式会社イシダと共同で、形式手法を用いて、同社 の大型商品処理装置内蔵プ ログラムの遠隔更新システムプロトタイプのセキュリティを検証した。まずBAN- logic を用いて、通信さ れる情報がセキュリティを確保するのに十分であることを確かめた。次に、シス テムの詳細仕様書から作 成したモデルを対象にモデル検査を行い、送受信された情報が正しく取り扱われ ているか検証した。
担当者 斎藤正也, 山形頼之
班名 フィールドワーク3班
寄与 株式会社イシダ
関連する事例

題材

領域 Java で記述された通信プロトコル
題材の詳細
シーケンスチャートで記述された通信プロトコルの仕様
通信プロトコル.
形態 仕様
言語 寄与者独自のシーケンスチャート
規模
題材の情報源

検証のデータ

目的


検証内容
商品処理装置、中継機器、管理サーバの3者が検証対象の通信プロトコルで通信
している
とする。また、これらの装置はクラッキングされる可能性があるものとする。
(1) 安全性についての検証
セッション終了時の状態が、以下のいづれかに限られること
1. 商品処理装置が正規の更新プログラムを受信する。
2. エラーが生じる。
3. 商品処理装置が何も受信しない。
(2) 秘匿性についての検証
不正な商品処理装置を用いて管理サーバから正常な商品処理装置の更新プログラムが
取得できないこと。
結果
(1)は成立する。(2)は成立しない。この通信プロトコルでは、最初に更新プログ
ラムの種類
を指定するための情報を送る。この内容は電子署名による保護が行われていない
ために、

更新プログラムの種類を偽ることができることが原因である。
検証手法 モデル検査
モデル化法 基本的にシーケンスチャートに従ってモデルを記述した。ただし、開発の進行と ともにシーケンスチャートと実装とに乖離が見られるようになったので、適宜 実装も参考にした。手動。
使用ツール Spin
スケジュール、
労力、時間など
3人で二ヶ月ぐらい
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
PS-2007-008, ソフトウェア更新システムのモデル検査によるセキュリティ, Yoriyuki Yamagata, Masaya Saitou, http://unit.aist.go.jp/cvs/tr-data/PS2007-008.pdf
論文発表
口頭発表
知的財産 2005年度に関連する特許を出願した。
その他

産総研ホーム >  組織 >  研究センター >  システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.