암호모듈 검증을 위한 UML 2.0 상태도 기반의 유한상태모델 명세 및 분석

국문 초록 (Abstract)

암호알고리즘 및 암호함수를 하드웨어적 또는 소프트웨어적으로 구현한 암호모듈을 암호모듈검증체계(Cryptographic Module Validation Program, CMVP) 내에서 시험(또는 인증, 검증)을 받기 위해서는 암호모듈에 대한 유한상태모델(Finite State Model, FSM)이 개발되고 제공되어야한다. 그러나 FSM을 체계적으로 모델링하고 분석하는 지침은 개발자와 시험자의 경험이므로 잘 알려져 있지 않다. 본 연구에서는 CMVP내에서 암호모듈의 검증을 위해 요구되는 FSM의 모델링, 분석지침, 천이시험경로 생성알고리즘을 제시하고 모델링도구인 CM-Statecharter를 개발하였다. FSM은 UML 2.0의 상태도를 이용해 모델링한다. 상태도는 FSM의 부족한 점을 보완하고 암호모듈의 FSM을 정형적이고 쉽게 명세할 수 있는 모델이다.

다국어 초록 (Multilingual Abstract)

A cryptographic module (CM) is an implementation of various cryptographic algorithms and functions by means of hardware or software. When a CM is validated or certified under the CM validation program(CMVP), a finite state model(FSM) of the CM should be developed and provided. However, guides or methods of modeling and analysis of a FSM is not well-known, because the guide is occasionally regarded as a proprietary know-how by developers as well as verifiers of the CM. In this paper, we propose a set of guides on modeling and analysis of a FSM, which is needed for validation of a CM under CMVP, and a transition test path generation algorithm, as well as implement a simple modeling tool (CM-Statecharter). A FSM of a CM is modeled by using the Statechart of UML 2.0. Statechart, overcoming weakness of a FSM, is a formal and easy specification model for finite state modeling of a CM.

목차 (Table of Contents)

• 요약
• ABSTRACT
• Ⅰ. 서론
• Ⅱ. 관련연구
• Ⅲ. 상태도의 정의 및 특성
• Ⅳ. 상태도 검증방법
• Ⅴ. 상태도 작성도구 CM-statecharter의 구현
• Ⅵ. 분석 및 결론
• 참고문헌
• 〈著者紹介〉

참고문헌 (Reference)

1 기술표준원, "암호시험기준, KS X ISO/IEC 24759"

2 IT보안인증사무국, "암호검증제출물 작성법 소개"

3 기술표준원, "암호검증기준, KS X ISO/IEC 19790: 2007"

4 "국가정보원 IT 보안 인증 사무국"

5 D. Harel, "“Synthesis revisited: generating statechart model from scenario-based requirements,” Formal Methods in Software and Systems Modeling" 309-324, 2005

6 장연세, "UML기반 시스템 분석 설계" 이한출판사 2008

7 D. Latella, "Towards a formal operational semantics of UML statechart diagrams" 331-347, 1999

8 IPA Security Policy, "Toshiba Solutions Cryptographic Library V.1.0.1" Toshiba Solutions Corporation 2007

9 J. Rumbaugh, "The Unified Modeling Language Reference Manual, 2th Ed." Addison-Wesley 2004

10 T. Maier, "The Fujaba statechart synthesis approach" 2003

11 M. Glinz, "Systematically combining specifications of internal and external system behavioral using statecharts" 14-20, 2004

12 B. Ludemann, "Synthesis of human- readable statecharts from sequence diagrams in ROOM environment" Christian Albrechts Universität zu KielAug 2005

13 S. Uchitel, "Synthesis of behavioral model from scenarios" 29 (29): 99-115, 2003

14 D. Harel, "Statecharts: A visual formalism for complex systems" 8 (8): 231-274, 1986

15 R. Eshuis, "Statecharting petri nets" Eindhoven University of Technology 2005

16 "StarUML 프로젝트"

17 H. Behrens, "Requirements analysis using statecharts and generated scenarios" 2002

18 R. Eshuis, "Reconciling statechart semantics" 74 (74): 65-99, 2009

19 S. Marquess, "OpenSSL FIPS 140-2 Security policy V.1.1.1b" Open Source Software Institute 2007

20 D. Drusinsky, "Modeling and verification using UML Statecharts" Newnes Pub. 2006

21 A. Jantsch, "Modeling Embedded Systems and SOC’s-concurrency and time in models of computation" Morgan Kaufmann Pub. 2003

22 Z. Pap, "Methods of checking general safety criteria in UML statechart specification" 87 (87): 89-107, 2005

23 "Japan Cryptographic Module Validation Program"

24 "ISO/IEC 24759:2008, Test Requirements for Cryptographic Modules"

25 "ISO/IEC 19790: 2006(E), Security Requirements for Cryptographic Modules"

26 J. Whittle, "Generating statechart designs from scenarios" 314-323, 2000

27 I. Kruger, "From MSCS to Statecharts" 61-71, 1999

28 "FIPS PUB 140-3(DRAFT), Security Requirements for Cryptographic Modules"

29 "FIPS PUB 140-2, Security Requirements for Cryptographic Modules"

30 "Derived Test Requirements(DTR) for FIPS PUB 140-2, Security Requirements for Cryptographic Modules"

31 A. Karatkevich, "Deadlock analysis in statecharts" 414-424, 2003

32 "Cryptographic Module Validation Program"

33 Z. Pap, "Completeness and consistency analysis of UML statechart specifications" 83-90, 2001

34 N. Mansurov, "Automatic synthesis of SDL models in use case methodology" 225-240, 1999