CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 8: アセンブラで記述された組込みシステムのモデル検査による検証事例


実施年度2007
概要 原因不明の不正な振る舞いが報告されている組込みソフトウェアに対し,モデ ル検査による検証を行い,モデル化の過程で,脆弱性を一つ発見した.検査対 象は,アセンブラで記述されたソースコードおよび詳細なフローチャートを中 心とする仕様書である.モデル検査は2段階にわけて行った.ソースコードから 半自動的に変換した詳細モデルによる検査と,発見した脆弱性が不正な振る舞 いに繋がるか否かを解析するため抽象モデルによるモデル検査である.詳細モ デルのモデル化の過程でアドレスと値を取り違える不正代入の脆弱性を発見し た.モデル検査器のシミュレーションモードでも脆弱性を確認したが,モデル 検査は,状態爆発により終わらなかった.発見した脆弱性が不正な振る舞いに 繋がるか否かを調べるために,脆弱性に関わる機能の振る舞いをフローチャー トから抽出して作成した抽象モデルによるモデル検査実験を行い,不正代入は 不正な振る舞いには繋がらないであろうという考察をえた.
担当者 高井 利憲,吉田 聡
班名 フィールドワーク6班
寄与 (非公開)
関連する事例

題材

領域 組込みソフトウェア
題材の詳細
システム全体のソフトウェアのソースコードが、アセンブラで一万行程度の
組込みシステム。
形態 ソースコードと詳細なフローチャートを中心とした仕様書
言語 C言語,日本語,フローチャート
規模 ソースコードは10,000行,仕様書は50ページほど
題材の情報源 (非公開)

検証のデータ

目的
原因不明の不正な振る舞いの解析へのモデル検査の応用,
アセンブラのソースコードに対する検証技法の確立
検証内容
ソースコードが仕様書通りに実装されているか(具体的な検証内容は非公開),
値とアドレスを取り違えるなどの不正代入の検出

モデルは,詳細モデルと抽象モデルの2種類作成
結果
モデル化の過程で,値とアドレスを取り違えるなどの不正代入を一つ発見
検証手法 モデル検査
モデル化法 モデル化は,ソースコードからの半自動変換によるものと, 注目機能に着目した,フローチャートからの手作業でのモデル化の2種類
使用ツール Spin,Perl (アセンブラからPromela への半自動変換に使用)
スケジュール、
労力、時間など
産総研側参加者2名,4週間ほど
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表
口頭発表 高井利憲, 吉田聡: アセンブラプログラムのモデル検査による検証事例,第5回 ディペンダブルシステムワークショップ(DSW07_summer), 2007年7月.
知的財産
その他

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