スライド 1

データ競合を検出するための
割込み自動生成
井上研究室 M2 東 誠
2010/2/15
修士論文発表会
1
Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
発表概要
• 目的:割込みを用いたプログラムのテスト支援
• 手段:割込みを自動的に生成することで,割
込みによる欠陥の一種(データ競合)を検出
• 結果:割込みの生成タイミングを手動で調整
することなしに,OSの障害を再現
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
2
2010/2/15
割込みを用いたプログラム
• 発生タイミングが判らないイベントを処理する
ために,割込みを利用するプログラムがある
割込み:プログラムに現在実行中の処理を中断さ
せ,より優先度の高い処理を実行させる要求
プログラムの動作に関係なく,いつでも発生する
• 例:デバイスドライバ,タイマー処理
通常処理
handler(void) 割込みハンドラ
main(void)
割込み
op = 1
割込み
return
op = 0
修士論文発表会
return
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
3
2010/2/15
割込みを用いたプログラムに
存在する欠陥
割込みハンドラと通常処理の間に存在する
データ競合
– 通常処理が利用しているメモリの値が,意図しな
いタイミングで,割込みハンドラによって変更され
てしまうという欠陥
以降,割込みによるデータ競合を単にデータ競合と呼ぶ
– データ競合による障害の例
放射線医療機器の事故[1]
データ競合を発見し,除去する必要がある
[1] N. G. Leveson. An investigation of the therac-25 accidents. IEEE Computer, 26:1841, 1993.
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
4
2010/2/15
データ競合の例
x が 0 以外なら除算を実行
通常処理
divide(void)
割込み
x != 0
no
割込み
return
x が 0 になるのに
除算を実行
変数
x
使用
使用
yes
割込み
割込みハンドラ
使用
interrupt_handler(void)
x=0
ret = 100 / x
割込み
return
データ競合をテストによって発見したい
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
5
2010/2/15
テストでデータ競合を発見する
際の問題
• 割込みを利用しないプログラムのテスト手順
•障害を起こしそう
– 入力を与える
– 正しい出力を返すことを確認 •系統的に
• 割込みを利用するプログラムのテストの問題
– 通常処理だけではなく,割込みハンドラとの組で
テストを行わなければならない
– 通常処理の中で割込みが発生するタイミングが
膨大である
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
6
2010/2/15
本研究の着目点
データ競合が存在する条件
– 通常処理で1つの変数を2回使用
• 1回目は読み込みか書き出し
• 2回目は読み込み
– 2回使用する変数の値が同じことを通常処理が
仮定
– 1回目と2回目の間で割込みが発生し,割込みハ
ンドラが変数の値を変更
x != 0
no
x が0以外
であること を仮定
割込み
ret = 100 / x
が3
return
であること
を仮定
Department of Computer Science, Graduate School of Information Science
and Technology, Osaka
University
修士論文発表会x
x=3
割込み
7
ret = 100 / x
2010/2/15
本研究の目的と手段
• 目的:データ競合が存在しうる箇所で割込み
を発生させる
• 手段:メモリを使用する任意の2つの命令間で
割込みを生成する
メモリを使用する全ての命令を実行した後に生成
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
8
2010/2/15
提案手法
機械語命令
CPUエミュレータ
テスト対象の
プログラム
割込み
割込み生成部
命令実行部
割込み
生成指示
実行した
命令
設定ファイル
プログラムの実行前に
割込みの種類を
ユーザが記述
割込み自動生成機構
指定
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
実行した命令が
読み込みまたは
書き出し
であるか判断
9
2010/2/15
実験内容
提案手法をCPUエミュレータskyeyeに実装し,
データ競合が存在するプログラムに適用
– 実験の目的
• 提案手法でデータ競合が実際に発見できることを確認
• データ競合の発見に必要な作業を調査
– 適用対象は実際に使われているOSの過去の
バージョン
• uClinux
• TinyOS
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
10
2010/2/15
uClinux のデータ競合
デバイスドライバでキューのデータ送信時に,
範囲外を参照
キューのデータ数を確認後,データを送信
→ 確認後に割込みが発生すると,割込みハンドラ
が送信
通常処理
割込みハンドラ
キューのデータ数が1
if (xmit_cnt <= 0 || ……)
return; 割込み
・
if (xmit_cnt <= 0 || ……)
return;
・
xmit_cnt--;
xmit_cnt--;
・
・
・
・
・
・
キューの範囲外を参照
修士論文発表会
キューのデータ数が0
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
11
2010/2/15
データ競合の発見に必要な作業
• テスト対象の通常処理を呼び出す
• 通常処理を呼び出す前に,キューにデータを
5個格納しておく
データ数の確認前に割込みが計4回発生
通常処理
Static void rs_flush_chars(struct tty_struct *tty){
割込み
割込み
struct m68k_serial
*info = ……;
m68328_uart *uart = ・……; 割込み
割込み
if (xmit_cnt <= 0 || ……)
return;
・
・
・
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
12
2010/2/15
提案手法によるテスト手順
1. データ競合が存在しうる組を特定
1. メモリの値を書き換える割込みハンドラを特定
2. そのメモリの値を2回使用する通常処理を特定
2. テストする通常処理への様々な入力を用意
例:使用しているメモリの値が配列の添字なら,
値を使用するタイミングで上限や下限に設定
3. 提案手法により,割込みを自動的に生成
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
13
2010/2/15
まとめと今後の課題
• データ競合を検出するため,メモリを使用す
る全ての命令の直後で割込み自動生成
割込みの生成タイミングを手動で調整することな
しに,データ競合による障害が再現できた
• 今後の課題
– データ競合が存在しうる箇所の自動特定
– データ競合の発見に必要な変数の値の自動特定
– データ競合の発見に不必要な割込み生成の除去
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
14
2010/2/15
2010/2/15
修士論文発表会
15
Software Engineering Laboratory, Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
割込み生成時の無限ループ防止
現在の
保存された
割込み生成機構
プログラム
プログラム
メモリの利用
カウンタの値 現在のプログラムカウンタが カウンタの値
割込み発生直前の値と
プログラム
割込み発生
同じか判定する
LDR ADDR
直前の
ADD
プログラム
MOV
比較結果
・
カウンタ
・
・
・
の値
・
プログラムカウンタが
・
Interrupt handler:
割込み発生直前のと
現在の
・
・
同じであれば,
プログラムカウンタ
・
割込み
・
・
割込みを発生させない
の値
・
RET
割込みハンドラ
同じ箇所で何度も割込みが発生し、
無限ループに陥る
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
16
2010/2/15
TinyOSのデータ競合
• 配列にデータ格納時に,添字が上限を越える
配列の添字を加算後,上限を越えたら初期化
→ 加算直後に割込みが発生すると,初期化され
ていない添字を用いて配列を利用
• データ競合の発見に必要な作業
– 通常処理としてADC.dataReady関数を呼び出す
– 配列の添字を上限に設定
割込みハンドラ(ADC.dataReady関数)
pack->data[packetReadingNumber++] = data;
割込み
if (packetReadingNumber == BUFFER_SIZE) {
修士論文発表会
packetReadingNumber
= 0;
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
・
・
.
17
2010/2/15
メモリの値をすり替える手順
読み込み命令
CPUエミュレータ
メモリ
プログラム メモリアドレスにアクセスする
メモリアドレスにアクセスする
アクセスする
LDR ADDR
ADD
MOV
・
・
・
・
・
・
新しい値を
注入する
値すり替え機構
読み込み命令の読み込み元
が指定された箇所か調べる
読み込み元が指定箇所なら
受け取った値を破棄し,
新しい値を設定する
値を渡す
値を渡す
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
18
2010/2/15
提案手法で検出できない例
1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
unsigned int len = 0;
void str_cpy(char *buf, char *str);
{
len = strlen(str);
if((0 < len) && (len <= strlen(str)))
memcpy(buf,str,len+1);
}
void interrupt_handler(void){
len++;
}
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
19
2010/2/15
修士論文発表会
Department of Computer Science, Graduate School of Information Science and Technology, Osaka University
20
2010/2/15