(Full Color): Preformatted Design and Template Items

検出漏れのない割込み干渉検出システムの開発
(株)豊田中央研究所
安全･情報システム研究部
アイシン精機(株)
ソフトウェアセンター
稲森 豊
山田信幸
8th Workshop on Critical Software (WOCS)
18-19 January 2011
概要
テストでは発見困難な不具合要因である割込み干渉について
Cソースコード作成段階で自動検出するシステムを開発した
目次
1.
2.
3.
4.
5.
6.
割込み干渉とは
システム開発の目的
割込み干渉検出手法の概要
割込み干渉検出手法の詳細
システム開発と評価
おわりに
8th Workshop on Critical Software (WOCS)
18-19 January 2011
検出漏れのない割込み干渉検出システムの開発
1. 割込み干渉とは
車載ソフトウェアにおける割込み処理
車両運動制御系
サスペンション制御
ブレーキ制御
エンジン制御
高速応答性
→
割込み処理
3／28
検出漏れのない割込み干渉検出システムの開発
1. 割込み干渉とは
割込み干渉
割込み処理に起因するデータ競合
＝
メイン処理
void main() {
... readアクセス
if (x > ...) {
...
y = x + ...;
}
readアクセス
...
}
二つの処理が同時に同一メモリにアクセス
and
少なくとも一つの writeアクセスがある
割込み
同一メモリ
x
割込み処理
void interrupt(){
...
x = ...;
...
writeアクセス
}
同時アクセス
不具合の原因 になり得る
4／28
検出漏れのない割込み干渉検出システムの開発
2. システム開発の目的
割込み干渉の未然防止
不具合混入の防止
不具合の発見･除去
要求分析
ｼｽﾃﾑﾃｽﾄ
ｵｰﾄｸﾙｰｽﾞｼｽﾃﾑの要求仕様
･ｵｰﾄｸﾙｰｽﾞ中にﾌﾞﾚｰｷ
⇒ｵｰﾄｸﾙｰｽﾞ解除しﾌﾞﾚｰｷ
･ｵｰﾄｸﾙｰｽﾞ中にｱｸｾﾙ
⇒ｵｰﾄｸﾙｰｽﾞ解除し加速
…
デザインレビュー
バグ
ｿﾌﾄｳｪｱ設計
ｿﾌﾄｳｪｱﾃｽﾄ
割込み干渉の
原因となるコード
テスト
実装
コードインスペクション
高い信頼性 を確保
5／28
検出漏れのない割込み干渉検出システムの開発
2. システム開発の目的
解決すべき問題
二つの処理は割込み干渉を起こすか？
→ ＹＥＳ？／ＮＯ？
割込み
①
…
if(x =
実装
…
コードインスペクション
実際に動作させることなく、
目で見て検証する作業
②
？
…
x = 0;
…
③…
x = 3;
…
高負荷 な作業
工数大
→
割込み干渉となる実行パスが存在するか？
割込み禁止命令で保護していないか？
・・・
6／28
検出漏れのない割込み干渉検出システムの開発
2. システム開発の目的
開発するシステム
▶ ソースコードを対象に割込み干渉を自動検出
少ない誤検出
最小限の人手の介在
手作業によるアサーション挿入等を
不要とする
誤検出箇所の人手による再チェック
工数を軽減する
誤検出箇所
検出
割込み干渉の
真の原因箇所
漏れのない検出
割込み干渉の原因を
テスト工程以降に残さない
7／28
検出漏れのない割込み干渉検出システムの開発
3. 割込み干渉検出手法の概要
割込み干渉の定義
低優先関数
void main() {
... ① readアクセス
if (x > ...) {
...
y = x + ...;
}
③ readアクセス
...
}
割込み
同一メモリ
x
高優先関数
void interrupt(){
...
x = ...;
...
② writeアクセス
}
同時アクセス
A) と B) が共に成立すること
A) 低優先関数*が短時間**の間に共有メモリに2回アクセスする（①，③）間
に割込みが発生し，高優先関数*が同一メモリ***にアクセスする（②）
* 低優先関数〔高優先関数〕 ：割り込まれた側の関数〔割り込んだ側の関数〕
** 短時間
：低優先関数の実行開始から終了までの時間
***同一メモリ
：ビット単位で同じメモリ（共用体，ﾋﾞｯﾄﾌｨｰﾙﾄﾞ使用を考慮）
B) 上記アクセス（①，②，③）のうち少なくとも一つは writeアクセスである
8／28
検出漏れのない割込み干渉検出システムの開発
3. 割込み干渉検出手法の概要
関連研究
動的解析
バグ発見に
主眼
データ競合
検出
LOCKSMITH (*1)
マルチスレッドプログラムを対象に，共有メモリを ロック
によって整合的に保護しているかを検証
静的解析
漏れの無い検出に
主眼
拡張C言語 nesC (*2)
共有メモリへのアクセスが atomic領域内にない場合，
割込み干渉の可能性のある箇所として検出
特定のアクセス保護手段に関して検証するが，
別の手段による保護については解析を行わない
||
ex.) フラグ変数によるアクセス制御
誤検出
*1: Pratikakis, P. et al.: LOCKSMITH: Context-Sensitive Correlation Analysis for Race Detection, Proc. of PLDI'06, pp. 320-331, 2006.
*2: Gay, D. et al.: The nesC Language: A Holistic Approach to Networked Embedded Systems, Proc. of PLDI, 2003
9／28
検出漏れのない割込み干渉検出システムの開発
3. 割込み干渉検出手法の概要
手法の概要（１／２）
Cプログラム
割込み干渉の可能性のある箇所を網羅的に列挙
共通の大域変数にアクセスする処理の組（低優先関数・高優先関数）を求め，
変数名，アクセス箇所（行番号），アクセス種類（read/write），等の情報を得る
判定項目リスト
低優先関数
判定結果
高優先関数
判定 共有
アクセス② 呼出し元
アクセス① アクセス③ 呼出し元
干渉なし／
関数
関数
項目 変数
優先
処理
処理
優先
行番
行番
行番
干渉の可能性
名
名
種類
種類
種類
度
名
名
度
号
号
号
あり
1
x
fun1 110 read 113 read main
0
sub1
15 write int1
3
?
2
y
sub1
22 read int2
5
?
…
…
…
…
…
53 write 54
write int1
3
sub2
…
…
…
…
…
…
…
メイン処理 main から呼び出される func1() の 110行目の readアクセス と 113行目の readアクセス の間に，
①
③
割込み処理 int1 から呼び出される sub1() の 15行目の writeアクセス が起こるか？
②
10／28
検出漏れのない割込み干渉検出システムの開発
3. 割込み干渉検出手法の概要
手法の概要（２／２）
各判定項目を判定
判定項目リスト
判定結果
高優先関数
低優先関数
アクセス② 呼出し元
判定 共有
アクセス① アクセス③ 呼出し元
干渉なし／
関数
項目 変数 関数 行番
処理 優先 干渉の可能性
処理 優先 名 行番
行番
名
種類
種類
種類
度
名
名
度
号
号
号
あり
0
sub1
15 write int1
3
?
53 write 54
write int1
3
sub2
22 read int2
5
?
…
…
…
…
…
…
1
x
fun1 110 read 113 read main
2
y
sub1
…
…
…
…
…
…
アクセスパターン判定
no
割込み干渉なし
アクセス種類と回数の条件を満たすか？
yes
アクセス同時性判定
no
割込み干渉なし
低優先関数のアクセス①，③は
同一制御フロー上か？
異なる視点で，
割込み干渉なし or
割込み干渉の可能性あり
を判定
検出漏れ防止
誤検出を抑制
yes
割込み禁止状態判定
no
割込み干渉なし
低優先関数のアクセス①，③は
割込み禁止命令で保護していないか？
yes
メモリ一致性判定
no
割込み干渉なし
アクセス箇所①，②，③はビット単位で
同一のメモリにアクセスしているか？
yes
実行パス存在性判定
割込み干渉を発生させる実行パス
（①→②→③）は存在するか？
no
割込み干渉なし
yes
割込み干渉の可能性あり
11／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
割込み禁止状態判定（１／５）
条件1：①の直前が割込み禁止状態
①～③の間ずっと割込み禁止状態 ＝
and
条件2：①～③の間に割込み許可命令が無い
低優先関数（割り込まれる側の関数）
…
func1()
条件2を「①～③の間の全ての文について，実行前，実行後
とも割込み禁止状態」とした場合，誤検出例あり
条件1：
実行前に割込み禁止状態
①
割込み状態の特定手法
（次頁以降で説明）
ブロック
（Ｃプログラムの文）
③
…
… …
func2();
条件2：
割込み許可命令が無い
（関数呼出しにも無い）
割込み許可命令の探索
（説明は省略）
12／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
割込み禁止状態判定（２／５）
割込み状態の特定における技術ポイント
▶ ループ文，関数呼出し文，分岐文に
対応できること
▶ 呼出し元が異なる場合の割込み状態
を正確に特定できること
sub1()
禁止
ループ文
禁止
func1()
func1()
①
func1()
③
許
…
許可状態
禁止状態 関数呼出し文
禁
①
sub2()
許可
…
func1()
end
func1()
…
許可
…
13／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
割込み禁止状態判定（３／５）
割込み状態の特定手法：抽象解釈を応用
関数毎に，各文の実行前割込み状態・実行後割込み状態を演算によって求める
割込み状態に関する抽象領域
func1()
許 or禁 or継
継
継
禁止 禁
継
継
禁
禁
禁 or継
許可
許
end
許 or禁
許
許 or継
禁
禁 or継
継
許：割込み許可状態
禁：割込み禁止状態
継：継承状態
関数呼出し元の状態を
継承する
nil
継承状態の導入により，関数毎の解析を可能としている
特定の処理から呼び出された場合の割込み状態を，
後工程の解析で求めることができる
割込み状態のOR演算
合流時の割込み状態を計算する
ORifg (禁，禁 ) =禁 ／ ORifg (許or継，許 ) =許or継 ／ ORifg (許or継，禁 ) =許or禁or継 ／ …
14／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
割込み禁止状態判定（４／５）
func()
割込み状態の収束計算
継
禁止 禁
ループ文内の割込み状態を繰返し計算により算出する
禁 許or禁
禁 許or禁
① 禁 許or禁
…
禁 許or禁
③ 禁 許or禁
禁 許or禁
func1()
許
1.
ループ文内の割込み状態を算出する
2.
ループ文の分岐式における割込み状態を算出する
3.
ループ文の分岐式における割込み状態が，
変化した場合， 1 に戻って再計算
それ以外の場合，ループ文内の計算終了
（次の文へ移る）
func1()
継
継
…
許可
end
許
15／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
割込み禁止状態判定（５／５）
main()
sub1()
func1()
…
継
禁止
禁
sub1()
func1()
…
…
sub2()
sub2()
継
継
禁
禁
①
許
…
…
許可
継
禁止 禁
func1()
③
禁 or継 ＝ ORifg(禁，ORifg(禁，許))
＝ 許 or 禁
…
①の実行前割込み状態が
許可状態である可能性があり，
「割込み干渉の可能性あり」
割込み状態の特定
①の実行前割込み状態が継 を含む場合，
1.
コールグラフの参照により，関数呼出し元の割込み状態を特定
2.
割込み状態のOR演算で，①の実行前割込み状態を特定
16／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
メモリ一致性判定（１／５）
低優先関数
void main() {
...
① readアクセス
if(u.byte > ・・・) {
...
f = p->b0;
>b0
}
③ readアクセス
...
}
割込み
uu
pp ff
高優先関数
void interrupt(){
...
u.bit.b0 = ON;
... ② writeアクセス
}
同一メモリ？
①,②,③で同一メモリにアクセス ⇒ 割込み干渉の可能性あり
要件：
• ビット単位で一致性を判定できること
• 標準的なＣ言語のあらゆる式に対応できること
• ポインタに（ある程度）対応できること
17／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
メモリ一致性判定（２／５）
手順１：構文解析時に，変数の宣言からメモリモデルを構築
手順１
メモリモデル
変数宣言
unsigned char x;
x(SimpleStorage)
データ型 ：unsigned char
幅
：8 (bit)
オフセット ：0 (bit)
幅：8 (bit)
a(ArrayStorage)
unsigned char a[2];
a[0] a[1]
データ型 ：unsigned char [2]
幅
：16 (bit)
オフセット ：0 (bit)
SimpleStorage:a[1]
オフセット：8 (bit)
unsigned char *p;
p (PointerStorage)
データ型 ：unsigned char
幅
：8 (bit)
オフセット ：8 (bit)
データ型 ：unsigned char *
幅
：32 (bit) （ﾏｲｺﾝ依存）
オフセット ：0 (bit)
18／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
メモリ一致性判定（３／５）
変数宣言
struct stag {
unsigned char e0;
unsigned char a[2];
} s;
union utag {
unsigned char byte;
struct {
unsigned char b0:1;
…
unsigned char b7:1;
} bit;
} u;
式
メモリモデル
s (StructStorage)
a
e0 a[0] a[1]
u (UnionStorage)
byte (SimpleStorage)
s1(StructStorage) s2(〃)
bit (StructStorage)
e0 e1
b0…b7
…
ps_table(ArrayStorage)
メモリモデル
x
&x
e0 e1
ps_table[0] ps_table[1]
pe0 pe1 pe0 pe1
&x (StorageAddr)
19／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
メモリ一致性判定（４／５）
手順２：判定箇所(
①,②,③)の式がアクセスするメモリを求め，
手順２
メモリの一致性を判定する
• 構文木からメモリモデルへのマッピングを行う関数を用意
u (UnionStorage)
① u.byte
u
② u.bit.b0
u
byte
bit
③ p->b0
byte (SimpleStorage)
bit (StructStorage)
b0 b0 b1 ……………… b7
b0
->
p
p (PointerStorage)
ポインタ変数の解析
&(u.bit)
①,②,③のアクセスメモリ一致 ⇒ 割込み干渉の可能性あり
20／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
メモリ一致性判定（５／５）
ポインタ変数の解析：
ポインタ変数の解析
▶
▶
解析条件：以下のポインタ変数の使用方法に限り解析
•
判定対象である変数のアドレスは局所ポインタ変数にしか代入されず，
•
局所ポインタ変数の加算代入，減算代入(p+=1等)や， 当てはまらない場合は解析不能
局所ポインタ変数同士の代入(p1=p2 等)は無い
(割込み干渉の可能性ありと判定)
解析方法の概要：
1.
局所ポインタ変数の初期値，および，局所ポインタ変数への代入式の右辺を求める
2.
1.で求めた各値について，以下を実行する
a. 1.で求めた値をメモリモデル上の局所ポインタ変数に設定する
b. 局所ポインタ変数を使用している式のアクセスメモリを調べ，記憶する
u (UnionStorage)
byte (SimpleStorage)
代入
代入
p (PointerStorage)
&(u.bit)
bit (StructStorage)
b0 b1 ……………… b7
21／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
実行パス存在性判定（１／４）
割込み干渉なし
＝ 実行パス ①→②→③ が存在しない
低優先関数
void main() {
... ① readアクセス
if (x > ...) {
...
y = x + ...;
}
③ readアクセス
...
}
割込み
同一メモリ
x
モデル検査
高優先関数
void interrupt(){
...
x = ...;
...
② writeアクセス
}
同時アクセス
22／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
実行パス存在性判定（２／４）
モデル検査における技術ポイント
▶ 割込みを含めたあらゆる実行パスを網羅的に検査できること
低優先関数
高優先関数
void interrupt(){
void main() {
...
... ① readアクセス
x = ...;
if (x > ...) {
...
...
② writeアクセス
}
y = x + ...;
}
③ readアクセス
あらゆるタイミングの割込み
...
}
多重割込み
▶ 数万行規模のCプログラムを検査できること
23／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
実行パス存在性判定（３／４）
SPIN（promelaコード）による多重割込みのモデル化
メイン処理
割込み処理
void main() {
... ① readアクセス
if (x > ...) {
...
y = x + ...;
}
③ readアクセス
...
}
void interrupt(){
...
x = ...;
...
② writeアクセス
}
メイン処理のプロセス
多重割込み
割込み処理のプロセス化
動作条件を provided節に記述
・割込みが許可されている(起動条件），または，
自プロセスが現在実行中である（実行継続条件）
動作条件を provided節に記述
・割込み処理が動作していない
24／28
検出漏れのない割込み干渉検出システムの開発
4. 割込み干渉検出手法の詳細
実行パス存在性判定（４／４）
①
実行パス解析のためのスライシング
手順１：３つのアクセス箇所（①，②，③）と
割込み関連命令文を必要コードとする
手順２：関数先頭から必要コードに到達する際に
必ず通る分岐条件式を必要コードに加える
手順３：手順２で得られた分岐条件式に
含まれる変数に関して，
変数への代入文を必要コードに加える
手順４：手順３で得られた代入文の
右辺に現れる変数に関して，
変数への代入文を必要コードに加える
：アクセス箇所 ／
f==1
i=1;
手順
1, 2
f==1
①
i=1;
手順
3
g==1
①
g==1
h==1
h==1
f=1; j=0; j=1;
f=1; j=0; j=1;
手順
2
f==1
手順５：手順３，４で新たに必要コードが得られた場合は
手順２に戻り，それ以外の場合は手順６へ進む
手順６：必要コード以外を削除する
：必要コード
f==1
①
g==1
i=1;
手順
5, 6
①
g==1
h==1
手順２’：関数先頭から必要コードに到達する際に
必ず通る分岐条件式のうち，
特定条件を満たすもののみを必要コードに加える
f=1;
f=1; j=0; j=1;
25／28
検出漏れのない割込み干渉検出システムの開発
5. システム開発と評価
開発したシステム
割込み干渉検出システム
判定項目リスト
判定
項目
No
出力
入力
Cプログラム
高優先関数
呼出し元
処理名
優先
度
関数名
行
番号
ｱｸｾｽ
種類
1
interrupt
3
interrupt
9
R
2
interrupt
3
interrupt
9
R
3
interrupt
3
interrupt
9
R
4
interrupt
3
interrupt
9
R
共有
変数名
.C
前
処
理
構文木
制御フロー
メモリモデル
判定結果
低優先関数
呼出し
元
処理名
優先
度
x
main
0
x
main
x
main
x
x
x
関数名
行
番号
ｱｸｾｽ
種類
判定
結果
main
9
W
0
main
10
W
○
0
func0000
12
W
？
▲
main
0
func0000
13
W
○
main
0
func0001
17
W
○
main
0
func0001
18
W
○
○
x
main
0
func0002
22
W
▲
？
x
main
0
func0002
24
W
○
判定項目生成
字句
シンボル
参照
Cプログラム Understand
データベース
(*1)
判定結果
判定
・・・
割込み禁止状態判定
・・・
実行パス存在性判定
割込み干渉検出システム (Rubyで実装 (*3)）
判定理由
L:9,9
L:9,10
○
○
DIL(Start)
DIL(Start)
L:10,10
○
DIL(Start)
L:12,12
L:12,13
？
○
▲
w(once)
wwr
L:13,13
○
w(once)
L:17,17
L:17,18
○
○
DIL(L:16)
DIL(L:16)
L:18,18
○
DIL(L:16)
L:22,22
L:22,24
？
○
▲
w(once)
wwr
L:24,24
○
DIL(L:23)
判定項目
判定結果
判定結果ファイル
モデル検査用コード
.pml
SPIN (*2)
.txt
モデル検査結果
*1: Scientific Toolworks社 Understand 2.0 を使用 *2: SPIN 5.2.0 を使用 *3: Ruby 1.9.1 を使用
26／28
検出漏れのない割込み干渉検出システムの開発
5. システム開発と評価
開発技術の評価結果
1. 自動判定率（割込み干渉なしと自動で判定できた率）
判定項目数
目標値：
自動判定率 90%以上
評価結果：
自動判定率 94.3%
→ 目標値以上の
自動検出率
2. 検出漏れ (割込み干渉の
発生箇所を見逃さないか？）
予め仕込まれた約20種類の割込み干渉のパターンを
「割込み干渉の可能性あり」と正しく判定
抽出された
判定項目
自動判定
項目数
（目標値）
自動判定
項目数
（評価結果）
→ 検出漏れなし
27／28
検出漏れのない割込み干渉検出システムの開発
6. さいごに
さいごに
▶ 単一プロセッサ上でOS無しに動作するCプログラムを対象に，
割込み干渉の発生箇所を，
• 抜け漏れなく
• 誤検出を少なく
自動検出する手法を開発し，システムを試作した
▶ 評価結果，性能面での実用性を確認したため，
現在，実用化に向け，事例を増やして評価中である
▶ 技術的課題：誤検出の更なる削減
• ポインタ解析，モデル検査の精度向上
▶ 今後は，割込み干渉を含めたタイミングに起因する問題について，
設計・検証の両面から解決する枠組みについて研究する予定である
28／28