On Modeling and Testing Security Properties of

2015/12/16
On Modeling and Testing
Security Properties of
Vehicular Networks
2014 IEEE International Conference on Software Testing, Verification, and Validation Workshops
岩手県立大学ソフトウェア情報学部
情報環境デザイン学講座
0312013050 熊澤正貴
2015/12/15
後期英語論文ゼミ
1
Abstract
• 車両ネットワーク
• 関連研究で様々な種類の車両ネットワークが挙げられ
ている
• 筆者らはDynamic Route Planning (DRP)とのVehicle to
Infrastructure(V2I)通信に着目した
• TestGen-IFツール
• テストケースを自動で生成することが可能
2015/12/15
後期英語論文ゼミ
2
1
2015/12/16
I. INTRODUCTION
• 車両ネットワーク
• 車両，運転手，乗客，歩行者に関連した様々なアプリケーションに実装
• 発展し続けている技術[1],[2],[3]
• Dynamic Route Planning(DRP)
• Intelligent Transportation Systems (ITS)のひとつで運転手の目的地への経路を
示す
• ITS コントロールセンターとの通信によって渋滞，天候，事故などにも対応して
いる
• Vehicle to Infrastructure(V2I)
• DRPに必要な条件
• モデルベーステストによって評価される[4],[5],[6],[7]
• DRPにおいて最も重要な拡張型オートマトンのアプローチを提案
2015/12/15
後期英語論文ゼミ
3
I. INTRODUCTION
• INTER-TRUST
• ネットワークとデバイスの異なるアプリケーションをサポート
するフレームワークの開発を目指すヨーロッパのプロジェクト
の一部
• Implementation Under Test (IUT)
• ソフトウェアの開発のアクティブな研究エリアで試験対象が
仕様を満たしているかテストしている
[8],[9],[10],[11],[12],[13],[14],[15],[16]
• TestGen-IFツール
• 膨大な数のテストをすべて行うわけにはいかないので，
TestGen-IFツールを使用しテスト生成を行う[17],[18],[19]
2015/12/15
後期英語論文ゼミ
4
2
2015/12/16
I. INTRODUCTION
• 変数で増やされる有限オートマトンを用いた，DRP
による車両ネットワークを提案
• TestGen-IFツールを利用して自動的にテストシナリ
オを生成する，新しい方法を提案
2015/12/15
後期英語論文ゼミ
5
II. PRELIMINARIES
• 拡張型オートマトン(EFSM)を補助するために有限オートマトン（FSM）を
導入
• FSMはメッセージ送受信によって状態を変化できる
• EFSMはFSMにコンテキスト変数，入力/出力パラメータ，断定，更
新機能が加わっている
• EFSMは7つの要素の集合M = (S, s0, Sf , I, O, x, T)で定義され，それぞれ
以下の意味を持つ
S＝空集合
s0＝初期状態
Sf＝最終状態
2015/12/15
I＝入力記号
O＝出力記号
X＝ベクトル
T=推移
後期英語論文ゼミ
6
3
2015/12/16
III. MODELING OF THE V2I UNDER
DRP SERVICE
• DRPは，ドライバーが目的地に到着するための最
適なルートを提供
• 天候，道路状態などの随時変化しうる要因が考慮
されている
• 効率的なルートを選んで移動時間の縮小
• コントロールセンターは，ユーザと車両にIDや位置
情報などの情報を要求する必要がある
2015/12/15
後期英語論文ゼミ
7
III. MODELING OF THE V2I UNDER
DRP SERVICE
A.
V2I under DRP simplified scenario
• 車両ネットワークのコンテキストにおいてフォーマルなモデルを
開発するために，管理センターと車両の行動とセキュリティ面を
考慮
• 車両，コントロールセンター，ユーザはFigure1の関係性がある
• このシナリオではアクセス制御を最も考慮
• コントロールセンターはユーザがアクセス権を与えられるかどう
かを確認
→車両にIDと位置情報を要求する
• ユーザは正しいログインとパスワードを設定し，コントロールセ
ンターの対象範囲内の位置にいる場合，アクセス権が得られる
2015/12/15
後期英語論文ゼミ
8
4
2015/12/16
III. MODELING OF THE V2I UNDER
DRP SERVICE
Fig. 1. Main actors in the V2I scenario
2015/12/15
後期英語論文ゼミ
9
III. MODELING OF THE V2I UNDER
DRP SERVICE
• Vehicle internal states
• Off-line：初期状態．
• Wait：車両がユーザからの情報待っている状態．
• Wait for logging：車両がアクセスする際にコントロール
センターからの応答を待っている状態．コントロールセ
ンターは，ユーザからの情報を確認したら，
success_log_inまたはerror_log_inのどちらかを返答す
る．
• Logged in：車両がサービスに接続されている状態．
• Navigation：車両がコントロールセンターによって計算さ
れたルートに従っている状態．
• Error navigation：車両がルートに沿わず，間違ったルー
トを進んでいる状態．
2015/12/15
後期英語論文ゼミ
10
5
2015/12/16
III. MODELING OF THE V2I UNDER
DRP SERVICE
Fig. 2. EFSM of the vehicle under DRP service
2015/12/15
後期英語論文ゼミ
11
III. MODELING OF THE V2I UNDER
DRP SERVICE
B. Vehicle to Infrastructure (V2I) scenario with negotiation
• Trust negotiation scenario
• 相互運用性を満たすために，トラストナビゲーションプロセスを提
案
• このシナリオによって車両とコントロールセンターの信頼性を満た
す
• DRPサービスを起動後，ユーザのアクセス権限をコントロールセンターが
チェック
• アクセスするには，車両がコントロールセンターの対象範囲内にいなけれ
ばならず，そのためには位置情報が必要
• 識別と認証を行うために彼の正しいログインとパスワードが必要
• しかし，セキュリティ上の理由のため，個人情報を送信できない
• したがって，車両がコントロールセンターを信頼する必要がある
2015/12/15
後期英語論文ゼミ
12
6
2015/12/16
III. MODELING OF THE V2I UNDER
DRP SERVICE
• Formalization of the scenario
• Off-line：車両の初期状態．
• Wait：コントロールセンターからの返信を，車両が待機
している状態
• Wait_certificate：車両がサーティフィケイトを待っている
状態
• Wait_decision：車両がユーザの決定を待っている状態
ユーザは，サーティフィケイトの条件に同意し，同意す
るメッセージを送信すること可能
• Wait_info：車両がユーザからログインに必要な情報を
待っている状態
• Wait_access：車両がサービスにアクセス可能かコント
ロールセンターの応答を待っている状態
2015/12/15
後期英語論文ゼミ
13
III. MODELING OF THE V2I UNDER
DRP SERVICE
Fig. 3. EFSM of the vehicle with trust negotiation
2015/12/15
後期英語論文ゼミ
14
7
2015/12/16
IV. TESTING
A. Adaptive Testing
• 初期状態で開始し，IUTの定義された入力を適用
• 入力によって生成された出力に基づいて，テスト
ケースを表し，EFSMを別の状態に移行する
• 観察された結果がEFSMの仕様に準拠している場
合，テストケースは合格とする
2015/12/15
後期英語論文ゼミ
15
IV. TESTING
図4では，次の手順を提示している．
• Step1
• ユーザは，メッセージactivate_service（DRP）を乗り物に
送る
• 車両の返答がrequest_service（DRP）となる場合，テスト
を継続
• Step2
• コントロールセンターは，メッセージrequest_information
を送り，車両側の出力をチェック
• 車両の出力がrequest_certificateの場合，テストを続行
2015/12/15
後期英語論文ゼミ
16
8
2015/12/16
IV. TESTING
• Step3
• 3つのcertificateを定義する
• システムが正常に動作すれば車両は，certificate01を受け入
れ，certificate02を拒否し，certificate03をユーザに委任する
Test1:certificate01
車両がrequire_info_loginと返答した場合，サーティフィケイトを
受け入れ，成功とする
Test2:certificate02
車両がdisagree_certificateと返答した場合，成功とする
Test:3certificate03
車両がdelegate_userと返答した場合，成功とする
2015/12/15
後期英語論文ゼミ
17
IV. TESTING
Fig. 4. Testing scenario
2015/12/15
後期英語論文ゼミ
18
9
2015/12/16
IV. TESTING
• 膨大な数のテストケースの生成は手動ではほぼ
不可能
→2つの手法を提案
• 新しいインタラクティブなアルゴリズムに基づく半自動
式のアプローチ（IV-C）
• 生成プロセスの途中で，ユーザの決定に基づいて，異なるテ
ストケースを生成する
• TestGen-IFを利用した，IF Specificationとテストの目的か
らのテストケース生成（IV-E）
2015/12/15
後期英語論文ゼミ
19
IV. TESTING
B. IF Specification
• シナリオのアクターには車両，ユーザ，コントロー
ルセンターがなりうる
→モデルを単純化するため，車両プロセスの
みを考慮
2015/12/15
後期英語論文ゼミ
20
10
2015/12/16
IV. TESTING
Fig. 5. A sample code of the V2I under DRP system specification in IF.
2015/12/15
後期英語論文ゼミ
21
IV. TESTING
C. A semi-automatic method to get all the test
scenarios
• シミュレーションの数を知り，それらを区別するた
めの提案
• 提案する方法は半自動的
• ユーザは現状からの遷移を手動で選ぶ必要があり，計
算された，期待される出力と予想される次の状態を計
算
2015/12/15
後期英語論文ゼミ
22
11
2015/12/16
IV. TESTING
Fig. 6. Initial phase of interactive simulation
2015/12/15
Fig. 7. Interactive simulation after 2 steps
後期英語論文ゼミ
23
IV. TESTING
D. TestGen-IF tool
• 筆者らの研究チームTelecom SudParisによって開
発された
• テストケースの自動生成を可能にする
• テストの目的に応じて生成される
• C ++コードで記述された自動テスト生成モジュール
Hit-or-Jump[19]を実装している
2015/12/15
後期英語論文ゼミ
24
12
2015/12/16
IV. TESTING
E. Automatic generation of abstract tests with
TestGen-IF
• IV- Aに記載された試験シナリオを実行
• 複数のサーティフィケイトを受信し，サービスにアク
セス，システムの動作を確認するためのテスト
ケースを生成させる
後期英語論文ゼミ
2015/12/15
25
IV. TESTING
Fig. 8. The formal description of test objective OBJ(1)
2015/12/15
後期英語論文ゼミ
26
13
2015/12/16
IV. TESTING
Fig. 9. The test case associated to OBJ(1)
Fig. 10. The test case associated to the vehicle receiving certificte02
Fig. 11. The test case associated to the vehicle receiving certificte03
2015/12/15
後期英語論文ゼミ
27
V. RELATED WORK
• Conformiq：状態遷移モデルベースのテスト設計およ
び自動テスト実行のためのソリューション[26]
• SpecExplorer：反応，オブジェクト指向のためのテスト
生成ツール[27]
• TGV ツール：プロトコルに対するテストスイート生成に
特化[28]
• jTorx：オンラインでのテストの導出と実行に焦点を当て
ている[29]
• 上記のモデルは拡張型オートマトンに対応していない
2015/12/15
後期英語論文ゼミ
28
14
2015/12/16
VI. CONCLUSIONS
• 車両ネットワークにおける動的なルート生成機能
を提案
• テストケースの自動生成が可能
• セキュリティプロパティの追加
• 将来的に以下のINTER-TRUSTプロジェクトの要件を
追加
• プライバシープロセスの強化
• Aspect Oriented Programming (AOP)の利用
• 回帰テストの実装
2015/12/15
後期英語論文ゼミ
29
REFERENCES
•
[1] G. Karagiannis, O. Altintas, E. Ekici, G. Heijenk, B. •
Jarupan, K. Lin, and T. Weil, “Vehicular networking: A
survey and tutorial on requirements, architectures,
challenges, standards and solutions,”
Communications Surveys & Tutorials, IEEE, vol. 13, no.
•
4, pp. 584–616, 2011.
•
[2] H. Moustafa and Y. Zhang, Vehicular networks:
techniques, standards, and applications. Auerbach
publications, 2009.
•
[3] S. Olariu and M. C. Weigle, Vehicular networks:
from theory to practice. CRC Press, 2010.
•
[4] J. Tretmans and A. Belinfante, “Automatic testing
with formal methods,” 1999.
•
•
[5] D. P. Sidhu and T.-K. Leung, “Formal methods for
protocol testing: A detailed study,” Software
Engineering, IEEE Transactions on, vol. 15, no. 4, pp.
413–426, 1989.
•
•
[6] L. Apfelbaum and J. Doyle, “Model based testing,”
in Software Quality Week Conference, 1997, pp. 296–
300.
•
[7] S. R. Dalal, A. Jain, N. Karunanithi, J. Leaton, C. M.
Lott, G. C. Patton, and B. M. Horowitz, “Model-based
testing in practice,” in Proceedings of the 21st
international conference on Software engineering.
ACM, 1999, pp. 285–294.
2015/12/15
[8] D. Lee and M. Yannakakis, “Principles and
methods of testing finite state machines-a survey,”
Proceedings of the IEEE, vol. 84, no. 8, pp. 1090–1123,
1996.
[9] B. S. Bosik and M. mit Uyar, “Finite state machine
based formal methods in protocol conformance
testing: from theory to implementation,” Computer
Networks and {ISDN} Systems, vol. 22, no. 1, pp. 7 –
33, 1991, ¡ce:title¿9th {IFIP} TC-6 International
Symposium on Protocol Specification, Testing and
Verification¡/ce:title¿. [Online]. Available:
http://www.sciencedirect.
com/science/article/pii/016975529190079R
[10] A. Petrenko, “Fault model-driven test derivation
from finite state models: Annotated bibliography,” in
Modeling and verification of parallel processes.
Springer, 2001, pp. 196–205.
[11] J. Tretmans, “Test generation with inputs,
outputs and repetitive quiescence,” Software—
Concepts and Tools, no. TR-CTIT-96-26, 1996.
後期英語論文ゼミ
30
15
2015/12/16
REFERENCES
•
[12] E. Brinksma and J. Tretmans, “Testing transition •
systems: An annotated bibliography,” in Modeling
and verification of parallel processes. Springer, 2001,
pp. 187–195.
•
[13] M. G. Merayo, M. Nu´nez, and I. Rodr ˜ ´ıguez,
“Formal testing from timed finite state machines,”
•
Computer networks, vol. 52, no. 2, pp. 432–460, 2008.
•
[14] I. Rodr´ıguez, M. G. Merayo, and M. Nu´nez,
“Hotl: Hypotheses and ob- ˜ servations testing logic,”
Journal of Logic and Algebraic Programming, vol. 74,
no. 2, pp. 57–93, 2008.
•
•
[15] D. Geman and B. Jedynak, “An active testing
model for tracking roads in satellite images,” Pattern
Analysis and Machine Intelligence, IEEE Transactions •
on, vol. 18, no. 1, pp. 1–14, 1996.
•
•
[16] P. Joshi, M. Naik, C.-S. Park, and K. Sen,
“Calfuzzer: An extensible active testing framework for
concurrent programs,” in Computer Aided Verification.•
Springer, 2009, pp. 675–681.
[17] A. R. Cavalli, E. M. D. Oca, W. Mallouli, and M.
Lallali, “Two complementary tools for the formal
testing of distributed systems with time constraints,”
in Proceedings of the 2008 12th IEEE/ACM
International Symposium on Distributed Simulation
and Real-Time Applications. IEEE Computer Society,
2008, pp. 315–318.
2015/12/15
[18] I. Hwang, A. R. Cavalli, M. Lallali, and D. Verchere,
“Applying formal methods to pcep: an industrial case
study from modeling to test generation,” Software
Testing, Verification and Reliability, vol. 22, no. 5, pp.
343–361, 2012.
[19] A. Cavalli, D. Lee, C. Rinderknecht, and F. Za¨ıdi,
“Hit-or-jump: An algorithm for embedded testing
with applications to in services,” in Formal Methods
for Protocol Engineering And Distributed Systems.
Springer, 1999, pp. 41–56.
[20] A. Simao, A. Petrenko, and J. Maldonado,
“Comparing finite state machine test coverage
criteria,” IET software, vol. 3, no. 2, pp. 91– 105, 2009.
[21] A. Petrenko and N. Yevtushenko, “Adaptive
testing of deterministic implementations specified by
nondeterministic fsms,” in Testing Software and
Systems. Springer, 2011, pp. 162–178.
[22] M. Gromov, K. El-Fakih, N. Shabaldina, and N.
Yevtushenko, “Distinguing non-deterministic timed
finite state machines,” in Formal Techniques for
Distributed Systems. Springer, 2009, pp. 137–151.
後期英語論文ゼミ
31
REFERENCES
•
[23] R. Dorofeeva, K. El-Fakih, S. Maag, A. R. Cavalli,
and N. Yevtushenko, “Fsm-based conformance testing
methods: A survey annotated with experimental
evaluation,” Inf. Softw. Technol., vol. 52, no. 12, pp.
•
1286– 1297, Dec. 2010.
•
[24] M. Bozga, S. Graf, I. Ober, I. Ober, and J. Sifakis,
“The if toolset,” in Formal Methods for the Design of
Real-Time Systems. Springer, 2004, pp. 237–267.
•
[25] M. Bozga, S. Graf, and L. Mounier, “If-2.0: A
validation environment for component-based realtime systems,” in Computer Aided Verification.
Springer, 2002, pp. 343–348.
•
[26] A. Huima, “Implementing conformiq qtronic,” in
Testing of Software and Communicating Systems.
•
Springer, 2007, pp. 1–12.
•
[27] M. Veanes, C. Campbell, W. Grieskamp, W.
Schulte, N. Tillmann, and L. Nachmanson, “Modelbased testing of object-oriented reactive systems
with spec explorer,” in Formal methods and testing.
Springer, 2008, pp. 39–76.
•
[28] C. Jard and T. Jeron, “Tgv: theory, principles and
algorithms,” ´ International Journal on Software Tools
for Technology Transfer, vol. 7, no. 4, pp. 297–315,
2005.
•
[29] A. Belinfante, “Jtorx: A tool for on-line model-
2015/12/15
•
driven test derivation and execution,” in Tools and
Algorithms for the Construction and Analysis of
Systems. Springer, 2010, pp. 266–270.
[30] M. Lallali, F. Zaidi, and A. Cavalli, “Transforming
bpel into intermediate format language for web
services composition testing,” in Next Generation
Web Services Practices, 2008. NWESP’08. 4th
International Conference on. IEEE, 2008, pp. 191–197.
[31] M. Lallali, F. Zaidi, A. Cavalli, and I. Hwang,
“Automatic timed test case generation for web
services composition,” in on Web Services, 2008.
ECOWS’08. IEEE Sixth European Conference. IEEE,
2008, pp. 53–62. 4849
[32] I. Hwang, M. Lallali, A. Cavalli, and D. Verchere,
“Modeling, validation, and verification of pcep using
the if language,” in Formal Techniques for Distributed
Systems. Springer, 2009, pp. 122–136.
後期英語論文ゼミ
32
16