<C3D6C1BEBAB8B0EDBCAD2E687770>

Transcription

1 최종연구보고서 KISA-WP 스마트카드 운영체제에 대한 EAL6 수준의 시험서 평가제출물 개발 Development of EAL6 Evaluation Deliverables: ATE Class for Smart Card Operating Systems 수탁기관: 고려대학교 발행년도

2 제 출 문 한국인터넷진흥원 원장 귀하 본 보고서를 스마트카드 운영체제에 대한 EAL6 수준의 시험서 평가제출물 개발 의 최종연구개발 결과보고서로 제출합니다 년 11월 30일 수탁 기관 : 고려대학교 연구책임자 : 교 수 최진영 (고려대학교 컴퓨터 통신공학부) 참여연구원 : 교 수 서동수 (성신여자대학교 컴퓨터정보학부) 교 수 강인혜 (서울시립대학교 기계정보공학과) 연 구 원 심재환 (고려대학교 컴퓨터 통신공학부) 연 구 원 황대연 (고려대학교 컴퓨터 통신공학부) 연 구 원 박준길 (고려대학교 컴퓨터 통신공학부) 연 구 원 정연오 (고려대학교 컴퓨터 통신공학부) 연 구 원 신지훈 (고려대학교 컴퓨터 통신공학부)

3 요 약 문 1. 제목 스마트카드 운영체제에 대한 EAL6 수준의 시험서 평가제출물 개발 2. 연구개발의 목적 및 중요성 현재까지 국제적으로 EAL5 이상의 고등급을 획득한 제품은 40여개 정 도가 된다. 국가별로 보면, 독일이 60%, 프랑스가 23% 정도를 차지하고 있 다. 그러나 국내에는 EAL5 이상의 고등급을 획득한 사례가 한 건도 없다. 이는 국내 개발 산업의 정형기법에 대한 인식과, 개발과정에서 정형기법을 사용하는 능력이 외국에 비해 많이 뒤떨어져있는 상황에 기인한다. 본 과 제에서는 KCOS라는 스마트카드 운영체제에 대한 EAL6 수준의 시험서 평 가제출물을 개발한다. 이 과제는 다음과 같은 이유에서 매우 필요하다. o (준)정형기법의 인식과 활용능력이 부족한 현재의 국내 현실에서, (준) 정형기법을 사용하여 EAL6 수준의 시험서 평가제출물 개발사례를 확보 가 중요 o 개발된 평가제출물은 국내 고등급 평가능력 함양을 위한 모의평가에

4 사용할 수 있음 o 스마트카드 운영체제에 대한 고등급 평가제출물을 확보하여, 증가하 는 내장형 시스템의 평가 수요에 대처할 평가능력을 국내에 갖추게 됨 o 국내에 고등급 평가능력을 갖추게 되면, 국산보안제품을 국제 평가 기 관을 통해 평가 받을 때 발생하는 고비용이 절감됨 o 국내 우수 기술이 국외로 유출 될 수 있는 가능성이 차단됨 o 국산 스마트카드 운영체제인 KCOS가 EAL6의 고등급을 획득하게 되 면 국산 보안제품이 국제 시장에서 매우 큰 경쟁력을 가지게 됨 또한 본 과제에서는 고등급 시험서 평가제출물 개발과 함께 준정형명세 와 정형도구을 기반으로 하는 테스팅 방법론을 제안한다. 이것은 EAL6의 ATE 클래스에 해당하는 시험문서 작성을 위한 기반 연구가 된다. 3. 연구개발의 내용 및 범위 본 과제는 다음과 같은 세부 연구내용을 중심으로 진행된다. o 스마트카드 운영체제(KCOS)에 대한 EAL6 수준의 시험서 평가제출물 개발 o 제품의 고 신뢰도 평가를 위한 정형도구를 사용한 테스트 방법론 제 안 4. 연구결과

5 본 연구에서는 K현금카드 내장형소프트웨어를 대상으로 CC v3.1의 ATE 클래스의 시험서를 작성하였다. EAL6 수준의 시험서를 작성하기 위 해 정적분석도구로는 Frama-C와 PolySpace를 사용했고, 소스기반 모델체 킹 도구로는 CBMC를 이용하였다. 또한 취약성 분석을 위해 Rats를 사용 하였다. 이러한 도구를 통해 KCOS를 시험한 결과, 잠재적으로 오류를 내 포한 모듈들을 발견할 수 있었다. 5. 기대효과 본 연구의 결과는 다음과 같은 기대효과를 갖는다. o 정형기법의 효과성을 이해하고 국내에 인식을 확산 o 고등급 평가제출물은 국내 고등급 평가능력을 갖추기 위한 기초자료 로 활용 o 연구 결과를 논문으로 작성함으로써 학문적인 기여 o KCOS가 EAL6 고등급을 획득하는데 사용될 수 있음

6 SUMMARY 1. Title Development of EAL6 Evaluation Deliverables : ATE Class for Smart Card Operating Systems 2. Purpose of the study Common Criteria has been widely used for evaluating security related information technology. There are forty or fewer products which are certified as high EAL in the world. 60% of them are from Germany and 23% of them are from France. However, there is no certified product as high EAL in Korea. Korea is behind the other countries in understanding and use of formal methods in industry. In this research project, we develop EAL6 test document evaluation deliverables for KCOS, a smartcard operating system. This research is very important for following reasons.

7 o It is important to provide EAL6 evaluation deliverable examples to industry in Korea where formal methods has not recognized well. o The deliverables can be used in mock evaluation for cutivating ability of evaluation as high EAL. o Evaluation ability can be cultivated so as to meet high-level evaluation demand which is increasing in embedded system area. o If we are able to evaluate a product as high EAL, we can reduce a great cost of the evaluation by international evaluator. o Leaking domestic technologies abroad is prevented. o Domestic security product can strengthen the competitive power in the world. In this project, we suggest a test methodology based on (semi)formal specification and tool with developing high-level test document evaluation deliverable. This is fundamental research for developing test document corresponding to EAL6 ATE class. 3. Contents and scope The detailed research contents of this project are based on followings. o developing EAL6 ATE class deliverables for smart-card operating system(kcos).

8 o suggesting test methodology using formal method tools for high EAL evaluation 4. Results of the study We used Frama-C and PolySpace as static analysis tool and also used CBMC as source code-based model checking tool for test documents of EAL6 ATE class. Also, We used Rats tool for vulnerability analysis. Though this analysis, we discovered modules which include some latent errors. 5. Expected effects and application Through this research, we expect effects: o spreading recognition of formal methods in domestic. o use of result of this project as source materiel for high level evaluation. o Academic contribution by writing papers based on the results. o KCOS can be used for certifying EAL6 high-level.

9 목 차 제 1 장 서론 1 제 1 절 연구 개발의 필요성 1 1. EAL6 수준의 시험서(ATE) 제출물 확보의 필요성 1 2. EAL6 평가를 위한 소스코드 레벨의 취약성 분석 방법론의 필요성 3 제 2 절 연구 개발의 목표 및 내용 5 1. 연구 개발 목표 5 2. 내용 및 범위 8 제 2 장 해외 공통평가기준 평가 사례 및 동향 분석 17 제 1 절 해외 평가 사례 및 통계 분석 전체 등급 상의 통계 고등급 인증의 통계 20 제 2 절 국가별 평가 사례 분석 미국 캐나다 영국 프랑스 독일 호주/뉴질랜드 일본 31

10 8. 네덜란드 노르웨이 스페인 스웨덴 32 제 3 절 해외 동향 분석 결과 33 제 3 장 정형 명세 언어의 소개 35 제 1 절 정적분석도구 Frama-C Frama-C 소개 값 해석(Value Analysis) 기법 튜토리얼 제약 사항 Parameterizing the analysis 입출력과 의존성 Annotations Primitives 116 제 2 절 정적 분석 도구 PolySpace PolySpace 소개 PolySpace for C 튜토리얼 124 제 3 절 모델체킹 도구 CBMC CProver 소개 사용 방법과 예 195 제 4 장 KCOS 시험 및 분석 결과 203

11 제 1 절 KCOS 시험 방법론 203 제 2 절 Frama-C 시험 결과 및 분석 isogetresponse 모듈 procreatesession 모듈 isoupdaterecord 모듈 isogetdata 모듈 isoputdata 모듈 isoselectfile 모듈 isogetchallenge 모듈 isextauth 모듈 problockfile 모듈 prounblockfile 모듈 proputkey 모듈 isoverify 모듈 prosetlifecycle 모듈 progetlifecycle 모듈 procreatefile 모듈 226 제 3 절 PolySpace 시험 결과 및 분석 isogetresponse 모듈 procreatesession 모듈 isoupdaterecord 모듈 isogetdata 모듈 isoputdata 모듈 isoselectfile 모듈 isogetchallenge 모듈 isextauth 모듈 problockfile 모듈 236

12 11. prounblockfile 모듈 proputkey 모듈 isoverify 모듈 prosetlifecycle 모듈 progetlifecycle 모듈 procreatefile 모듈 242 제 4 절 모델체킹 결과와 동적 테스팅 결과 EAL6의 시험서 평가 제출물 시험 환경의 제약 사항 모델체킹 및 동적 테스팅의 환경 구성 및 시험 248 제 5 절 TOE 분석결과 발견된 문제점들 type 오류 발견 잘못된 구조체 초기화 발견 재귀 함수 발견 코드의 미 완성적인 부분 발견 255 제 5 장 결론 258 부록 A. CC v3.1 EAL6 KCOS 평가 제출물 259

13 표 목차 [표 1-1] 공통평가기준 평가보증등급 1 [표 1-2] ATE 클래스 평가 제출물 6 [표 1-3] EAL6에서의 보증클래스와 보증 컴포넌트와의 관계 8 [표 1-4] ATE 클래스 컴포넌트 별 종속관계 9 [표 2-1] 연도별 등급별 인증 건수 (출처 : Common Criteria Portal) 17 [표 2-2] 제품군별 고등급 인증 현황 20 [표 2-3] 미국 고등급 인증 제품 (출처 : NIAP CCEVS) 21 [표 2-4] 미국 평가중인 고등급 제품(NIAP CCEVS) 22 [표 2-5] 영국 고등급 인증 제품 (출처 : CESG) 23 [표 2-6] 프랑스 고등급 인증 제품 (출처 : DCSSI) 23 [표 2-7] 독일 고등급 인증 제품 (출처 : BSI) 25 [표 2-8] 호주/뉴질랜드 ITSEC 고등급 인증 제품 (출처 : DSD) 30 [표 2-9] 호주/뉴질랜드 평가중인 고등급 제품(출처 : DSD) 31 [표 2-10] 노르웨이 고등급 인증 제품 (출처 : SERTIT) 32 [표 3-1] PolySpace 프로젝트 타입 125

14 그림 목차 (그림 1-1) 국가별 고등급 획득 비율 2 (그림 1-2) CEGAR 개략도 13 (그림 1-3) 테스트 방법론 15 (그림 2-1) 평가 등급별 점유율 18 (그림 2-2) 제품군별 인증 건수 및 백분율 (출처 Common Criteria Portal) 19 (그림 2-3) 국가별 공통평가기준 인증 현황 33 (그림 2-4) 국가별 등급별 고등급 CC 인증 현황 34 (그림 4-1) KCOS 시험 방법론 206 (그림 4-2) 등급별 평가 제출물 요구 사항 246 (그림 4-3) 평가보증등급 요약 247 (그림 4-4) 스마트 카드 환경의 PC 매핑 248

15 제 1 장 서론 제 1 절 연구 개발의 필요성 1. EAL6 수준의 시험서(ATE) 제출물 확보의 필요성 공통평가기준(Common Criteria for Information Technology Security Evaluation)은 보안관련 컴퓨팅 기술의 평가를 위한 국제 표준이다. ITSEC, TCSEC 등 유사 종류 의 표준을 범국가적으로 통합하고자 하는 목적으로 제정되었다. 공통평가기준은 보 증 수준에 따라 7단계의 평가보증등급(Evaluation Assurance Level)을 정의하고 있 다. 특히 EAL5에서 EAL7까지는 고 보증등급으로 불린다. 평가보증등급을 표로 나 타내면 다음과 같다. [표 1-1] 공통평가기준 평가보증등급 EAL7 EAL6 EAL5 EAL4 EAL3 EAL2 EAL1 정형화된 설계 검증 및 시험 준정형화된 설계 검증 및 시험 준정형화된 설계 및 시험 체계적인 설계, 시험 및 검토 체계적인 시험 및 검사 구조적인 시험 기능적인 시험 위의 표에서 보는 바와 같이 고 보증등급인 EAL5에서 EAL7의 경우에 준 정형기법 (Semiformal) 혹은 정형기법(Formal)을 이용하여 평가대상을 설계하고 검증하고, 테 스트하기를 요구하고 있다. 따라서 보안시스템의 개발주체는 고등급의 보증등급을 획득하기 위해서는 정형기법의 적용이 필수적이다. 국제적으로 정보보호의 중요성이 높아가면서 신뢰도가 높은 보안제품의 필요성 역 시 함께 증가하게 되었다. 이러한 이유로 CC 기반의 평가 인증 제도를 사용하고 있는 국가들에서는 고등급 평가에 관련된 연구가 2001년도부터 지속적으로 진행되 고 있다. 미국, 독일, 프랑스 등의 나라는 평가 및 인증 역사가 오래 되었고, 초기부 터 CCRA 가입국이 되었다. 우리나라는 2006년에 CCRA 가입국이 되었다. 현재까 - 1 -

16 지 국제적으로 EAL5 이상의 고등급을 획득한 제품은 40여개 정도가 된다. 국가별 로 보면, 독일이 60%, 프랑스가 23% 정도를 차지하고 있다. 아래의 그림은 이것을 도식화 한 것이다. (그림 1-1) 국가별 고등급 획득 비율 안타깝게도 국내에는 EAL5 이상의 고등급 평가하여 인증한 사례가 한 건도 없다. 국내 개발 산업의 정형기법에 대한 인식과, 개발과정에서 정형기법을 사용하는 능 력이 외국에 비해 많이 뒤떨어져있는 상황이다. 공통평가기준에서의 시험서(ATE)는 개발문서(ADV)와 관련이 깊다. 고등급에서 개발문서는 정형 또는 준정형으로 작성 되어야 한다. 따라서 공통평가기준의 고등급에서 시험서를 작성하기 위해서는 정형 기법에 대한 이해가 필요하다. 본 과제에서는 KCOS라는 스마트카드 운영체제에 대 한 EAL6 수준의 평가를 위한 시험서(ATE 클래스) 평가제출물을 개발할 것이다. 이 과제는 다음과 같은 이유에서 매우 필요하다. (준)정형기법의 인식과 활용능력이 부족한 현재의 국내 현실에서, (준)정형기법을 사용하여 EAL6 수준의 시험서 평가제출물 개발사례를 확보하는 것이 중요 개발된 평가제출물은 국내 고등급 평가능력 함양을 위한 모의평가에 사용될 수 있음 스마트카드 운영체제에 대한 고등급 평가제출물을 확보하여, 증가하는 내장형 시스템의 평가 수요에 대처할 평가능력을 국내에 갖추게 됨 국내에 고등급 평가능력을 갖추게 되면, 국산보안제품을 국제 평가 기관을 통해 평가 받을 때 발생하는 고비용이 절감됨 - 2 -

17 또한 국내 우수 기술이 국외로 유출 될 수 있는 가능성이 차단됨 국산 스마트카드 운영체제인 KCOS가 EAL6의 고등급을 획득하게 되면 국산 보 안제품이 국제 시장에서 매우 큰 경쟁력을 가질 수 있음 2. EAL6 평가를 위한 소스코드 레벨의 취약성 분석 방법론의 필요성 취약성이란 운영체계나 시스템 소프트웨어 또는 응용소프트웨어 컴포넌트가 지니고 있는 보안상의 문제점이나 허점을 말한다. 이러한 취약성을 가지고 있는 시스템이 나 네트웍은 외부의 침입에 대해 큰 손상을 입을 잠재 위험이 있다. 보안 전문 회 사들은 이를 위해 소프트웨어 버전 별로 취약성 데이터베이스를 유지하기도 한다. 공통평가기준의 고등급에서는 높은 보증을 제공하기위해 보안정책모델, 기능명세, TOE 디자인을 정형 또는 준정형명세하고 검증한다. 그리고 보안기능요구사항, 보안 정책모델, 기능명세 그리고 TOE 디자인 사이의 일치성을 확립한다. 하지만 검증된 디자인을 사용하여 소스코드를 구현을 했더라도, 코딩 과정에서의 실수 등 여러 가 지 이유로 소스코드에 취약성이 존재할 수 있다. 소스코드에 취약성이 있다면 시스 템이 동작할 때 이 그것이 발현될 위험이 존재하게 된다. 특별히, 이 과제에의 KCOS와 같은 스마트카드운영체제 경우에 소스코드의 취약성 은 커다란 문제를 야기할 수 있다. 스마트카드에는 개인정보를 비롯한 여러 비밀정 보를 담는 경우가 많다. 스마트카드 운영체제의 취약성으로 인해 이러한 개인정보 및 비밀정보가 그대로 외부에 노출될 수 있다. 이런 운영체제의 취약성은 프로그래 머의 실수로 인한 운영체제 소스코드 상의 결함으로 야기되는 경우가 많다. 소스코 드의 결함은 소스코드를 대상으로 직접 테스팅을 수행할 때만 찾아낼 수 있다. 제품의 정책모델, 기능명세, 디자인을 검증하는 것이 중요할 뿐 아니라, 제품의 소 스코드를 테스팅하는 것도 따라서 중요하다. 전통적인 의미에서 테스팅이란 소스코 드를 실행하여 어떤 입력을 넣었을 때 올바른 결과가 나오는지 확인하는 것을 말한 다. 테스팅은 소스코드의 결함이 있음을 보일 수 있어도 결함이 없다는 것을 보증 하지는 못한다. 이런 의미에서 테스팅은 항상 불충분하다고 말할 수 있다. 또한 KCOS 운영체제와 같은 반응형 시스템은 종료하지 않는 특성을 가지고 있는데, 이 - 3 -

18 런 시스템에 전통적인 테스팅 방법은 적용할 수 없다. 그리고 오늘날의 시스템은 실시간성과 동시성의 성질을 추가로 가지는 경우가 많은데, 이러한 시스템을 전통 적인 방법으로 테스팅하기는 거의 불가능하다고 말할 수 있다. 정형기법 분야에서는 이러한 시스템의 소스코드를 분석하기 위해 여러 가지 방법이 연구되어왔다. 정적분석, 동적분석, 시스템적인 테스팅, 소스코드 모델체킹들이 그 예들이다. 이 과제에서는 정형기법분야의 기존연구들을 바탕으로 스마트카드 운영 체제(KCOS)에 대한 EAL6 수준의 평가를 위한 소스코드 레벨의 취약성 분석 방법 론을 개발할 것이다. 이 과제는 다음과 같은 이유에서 필요하다. 불완전한 전통적인 테스팅의 한계를 정형기법을 사용하여 극복함 정형기법분야의 최신방법들을 이용하여 공통평가기준 관점으로 테스팅 방법론을 개발 공통평가기준의 테스팅 방법론으로 테스팅된 소스코드는 평가 및 인증할 때 추 가적인 보증을 가짐 정형기법 이론뿐 아니라 다수의 유용한 정형도구들을 공통평가기준 평가에서 실 제적으로 사용할 수 있게 됨 여러 도구를 이용하여 취약성을 분석한 KCOS는 더 높은 보안성을 갖게 됨 제 2 절 연구 개발의 목표 및 내용 1. 연구 개발 목표 본 과제의 최종 목표는 다음과 같다. KCOS를 대상으로 시험문서(ATE 클래스)에 대한 EAL6 수준의 평가제출물 개발 공통평가기준(CC)에 적합한 정형 도구를 사용한 테스트 및 취약성 분석 방법 개 발 - 4 -

19 KCOS에 대한 소스코드 수준의 테스트 및 취약성 분석에 개발된 방법론 적용 '08년 개발된 KCOS의 EAL6 수준 개발문서(ADV 클래스)에 대한 평가자 수정요 구사항 반영 해외(유럽, 미국, 일본) 최근 고등급 시험 취약성 평가기술, 평가방법론 및 적용 사례 조사 CC EAL6에서는 보다 구조화 된 테스트와 엄밀한 시험범위 분석을 요구하고 있다. 이러한 요구를 만족시킬 수 있는 체계화 된 테스트 방법의 적용과 이를 통해 산출 된 시험 문서를 개발하는 것이 본 과제의 첫 번째 목표이다. 본 과제에서 작성할 ATE 클래스 평가제출물은 다음의 표에 명시되어 있는 항목으로 평가 가능하게 시 험서를 작성한다. [표 1-2] ATE 클래스 평가 제출물 ATE_COV ATE_DPT ATE_FUN ATE_IND 범위 상세수준 기능 시험 독립적인 시험 이 중 독립 시험인 ATE_IND는 개발자가 아닌 평가자에 의해 수행 되어 진다. 본 과제의 두 번째 목표는 공통평가기준에 적합한 정형 도구를 사용한 테스트 및 취약성 분석 방법 개발이다. EAL6에서는 모든 매개 변수에 대한 시험을 요하고 있 고, 이에 대한 엄밀한 시험 범위 분석과 상세 수준 분석을 요구하고 있다. 이는 일 반적인 테스트 방법으로는 매우 높은 비용을 필요로 한다. 이 때문에 본 과제에서 는 높은 수준의 시험 사례 획득과 시험 범위 분석을 위한 테스트 방법론을 개발할 것이다. 본 과제에서 제안할 테스트 방법론은 다음과 같다. 정형언어를 통한 테스트 케이스 방법론 개발 소스코드 레벨에서의 모델체킹을 통한 테스트 방법론 개발 정적 분석을 통한 테스트 방법론 개발 본 과제의 세 번째 목표는 제안된 테스트 방법론을 실제 스마트카드 소프트웨어인 KCOS에 적용하여 그 타당성을 확인하는 작업이다. KCOS는 스마트카드의 동작을 위한 운영체제이다. 운영체제의 특성상 테스트 될 KCOS 소프트웨어는 하드웨어와 - 5 -

20 매우 밀접한 연관을 가지고 있다. 이러한 경우 그 특성상 기존의 테스트 방법을 적 용하기에 어려움이 있다. 따라서, 운영체제와 같은 소프트웨어에 대한 테스트 방법 론을 개발하여 적용한 뒤 그 타당성을 확인할 것이다. 본 과제의 네 번째 목표는 '08년 개발된 KCOS 개발문서에 대해서 현재 KISA가 진 행 중인 평가에서 발견된 관찰사항에 대한 수정작업이다. 작년도 과제에서 개발된 개발문서는 KISA에서 개발한 평가방법론에 의해서 CC v3.1기반에 EAL6 평가가 진 행 중이며, 평가자에 제출물에 대한 수정 요구사항이 발생하거나, 시험서 개발 중에 개발문서와 시험서의 일관성 문제로 수정사항이 발생할 수 있으며, 전체 제출물의 일관성 및 정확도를 높이기 위해서 기 개발된 제출물에 대한 수정 작업이 필요할 것이다. 본 과제의 마지막 목표는 시험 취약성 평가 방법론 개발을 위한 해외 동향 조사 및 분석이다. 이 목표를 위해서 다음 분야에 대한 해외 동향을 조사할 것이다. - 정형기법을 적용하여 시험 취약성 분석을 수행한 해외 사례 조사 - CCRA 인증서 발행국에서 최근 수행한 고등급 평가 인증 사례 조사 - 고등급 평가 인증 적용된 시험 취약성 평가 방법론 및 사례 조사 2. 내용 및 범위 2.1 시험클래스 문서 제출물 개발 및 테스트 방법론 연구 시험 클래스(ATE)는 범위(ATE_COV), 상세수준(ATE_DPT), 독립적인 시험 (ATE_IND), 기능 시험 (ATE_FUN)의 4개의 패밀리를 포함한다. 시험은 TSF가 기능 명세, TOE의 설계, 구현의 표현에 서술된 대로 동작하는지를 보여주는 작업이다. 시험 문서가 EAL6을 만족하기 위해서는 EAL6에 해당하는 보증 컴포넌트와 이에 따르는 종속관계를 이해해야 한다. EAL6 등급에서 보증 클래스와 보증 컴포넌트와 의 관계는 아래의 표와 같다

21 [표 1-3] EAL6에서의 보증클래스와 보증 컴포넌트와의 관계 보증 클래스 COV 보증 컴포넌트 ATE_COV.3 시험 범위의 엄밀한 분석 DPT ATE_DPT.3 모듈 설계 시험 FUN ATE_FUN.2 순서화된 기능 시험 IND ATE_IND.2 독립적인 시험 : 표본 시험 각 컴포넌트 별 종속 관계는 아래의 표와 같다. [표 1-4] ATE 클래스 컴포넌트 별 종속관계 ATE_COV.3 ATE_DPT.3 ATE_FUN.2 ATE_IND.2 - ADV_FSP.2 보안-수행 기능명세 - ATE_FUN.1 기능 시험 - ADV_ARC.1 보안 구조 설명 - ADV_TDS.4 준정형화된 모듈화의 설계 - ATE_FUN.1 기능 시험 - ATE_COV.1 시험범위의 증거 - ADV_FSP.2 보안-수행 기능명세 - AGD_OPE.1 사용자 운영 설명서 - AGD_PRE.1 준비 절차 - ATE_COV.1 시험 범위의 증거 - ATE_FUN.1 기능 시험 위의 표에서와 같이 EAL6의 시험문서는 개발 문서를 참조하게 되어있고, 특히 ATE_DPT.3은 모듈의 시험을 위해 준정형화 된 설계 문서를 참조하게 되어있다. 따 라서 본 과제에서는 보다 효율적이고 높은 수준의 테스트 커버리지를 만족하는 테 스트 방법 제안하기 위해 소스코드 수행을 통한 통적 테스트를 기본으로 하여 다음 과 같은 추가적인 두 가지 방식의 테스트 방법을 연구한다. 정적분석기를 이용한 테스트 방법론 - 7 -

22 소스코드의 모델체킹 방법을 이용한 테스트 방법론 1) 정적분석기를 이용한 테스트 방법론 정적 프로그램 분석(Static Code Analysis)은 컴퓨터 소프트웨어를 분석하는 방법 가운데 하나로 그 소프트웨어로부터 만들어진 프로그램을 실제로 실행해보지 않고 분석하는 방법이다. 참고로 프로그램을 실행해보고 분석하는 방법은 동적 프로그램 분석이라고 한다. 대부분의 경우 원시 코드의 형태를 가지고 분석을 수행하지만 목 적 코드의 형태를 가지고 분석하는 경우도 있다. 정적 프로그램 분석은 일반적으로 사람이 어느 정도 프로그램에 대한 이해한 뒤 자동화된 도구를 이용한다. 분석의 복잡한 정도는 도구에 따라서 각각의 명령문과 선언문을 분석하는 것부터 프로그램의 원시코드 전체를 포함해 분석하는 것까지 다양하다. 분석된 정보를 이 용하는 것 또한 있음직한 코딩 에러를 표시해주는 것부터 프로그램이 어떤 속성을 만족하는지 수학적으로 증명하는 정형분석법까지 다양하다. 어느 학자는 소프트웨 어 계량과 역공학을 정적 프로그램 분석의 한 종류로 보는 견해를 가진다. 정적분석은 White-box 테스트의 한 종류로 보아진다. 그리고 정적분석의 한 종류로 실행의미 분석 기반의 정적분석이 있다. 실행의미 분석 기반의 정적 프로그램 분석 이란 프로그램이 실행 중에 가질 수 있는 성질을 실행 전에 엄밀하게 예측하는 기 술로서, 이를 통해 프로그램의 오류를 미리 자동으로 검증할 수 있다. 이 기술은 지 난 30년 동안 심도 있는 연구가 진행되어 왔으나, 이제 그 결실들이 실제 산업에서 프로그램 오류 검증 도구에 적용되기 시작했다. 프로그램 내에 있는 메모리 관련 오류를 정확하게 분석하기 위해서는 프로그램의 실행 단계를 따라가며, 각 단계에 서 변수들이 어떤 값을 가지는지, 할당된 메모리가 정상적으로 해지되고 있는지 등 을 세밀히 살펴보아야 한다. 실행의미 분석 기반의 정적 프로그램 분석 기술은 이 렇게 사람이 눈으로 분석하는 것과 동일한 방법으로 프로그램을 분석하는 기술이 다. 안전필수 시스템이나 보안필수 시스템에서 잠재적으로 취약한 코드를 찾아내기 위 해 정적 분석의 상업적 이용이 늘어나고 있다. 대표적인 정적분석기로는 Mathworks사의 Polyspace C Verifier와 파수닷컴사의 Sparrow가 있다. 이들은 실행 의미 분석 기반의 정적프로그램 분석을 수행한다. 이들은 실행의미 분석을 위해서 - 8 -

23 특별히 요약 해석 (Abstract Interpretation)이라는 기술을 사용하고 있는데, 이는 프 로그램의 실제 실행 과정을 요약해서 실행해 보는 것이다. 이를 위하여 먼저 프로 그램의 실제 실행흐름 및 상태를 Graph를 통해 구성한다. Graph의 각 정점은 프로 그램의 실행 상태를 나타내고, 간선은 실행 흐름을 나타낸다. 요약해석 방법을 통해 유한한 시간 내에 프로그램의 모든 실행결과를 포섭하는 분석을 수행할 수 있다. PolySpace C Verifier는 코드기반 검증을 제공하고 소스코드에 에러가 없음을 증명 하는 도구이다. 그리고 Polyspace는 코드를 실행시키거나, 코드를 읽고 조사하거나, 테스팅을 하지않고도 런타임 에러를 찾아냄으로 코드의 신뢰성을 높인다. Polyspace는 코드를 검증하는데 요약해석 기법을 사용한다. 이것을 통해 Polyspace 는 코드 내에 overflows, divisions by zero, buffer overflows, pointer issues 등의 문제가 없는지 자동으로 확인한다. Polyspace 파일레벨 또는 클래스레벨로 소프트 웨어 컴포넌트 검증이 가능하다. 그리고 Polyspace는 소스코드가 Misra C 2004나 JSF++과 같은 코딩 규칙을 부합하는지 체크해주는 기능을 가지고 있다. SPARROW는 프로그램의 실행 의미를 정교하게 분석하여, 검출이 어렵고 개발자가 지나칠 수 있는 치명적 오류를 자동으로 검출하는 정적분석기로서 우리나라 기술로 개발되었다. SPARROW는 소프트웨어 품질 향상을 위한 환경을 제공한다. SPARROW는 깊고 상세한 분석을 제공한다. 프로그램의 실제 실행 과정, 모든 상태 변화를 분석하여 복잡한 프로그램 속에 내재한 오류들도 정밀하게 분석한다. 특별 히 Deep call chain, Recursions, Complex heap structures, Pointer aliases, Infinite loops, Function pointer, Dynamic memory allocation, Libraries 들의 경우에도 분 석을 지원한다. SPARROW는 강력하고 안전한 타입 시스템을 제공하는 언어인 Ocaml 사용을 사용하여 구현되었다. 그리고 Web기반 통합관리/운용 툴인 NEST가 지원된다. Polyspace와 SPARROW와 같은 정적분석도구는 전통적인 테스팅을 보완하는데 사 용할 수 있다. 정적분석은 전통적인 테스팅보다 더 완전한 커버리지를 제공한다. 그 리고 공통평가기준의 시험 클래스에서 요구하는 것과 같이, 정적분석도구들은 TSF 가 설계 설명대로 동작하는지 테스트하는데도 사용될 수 있다. 정적분석기는 소스 코드를 여러 관점에서 자동으로 분석하고 도표 등을 이용하여 결과를 내준다. 이러 한 결과들은 시험클래스의 평가제출물들에 포함시키면 평가자가 평가하는데 도움을 줄 수 있고, 소스코드의 성질들을 한눈에 볼 수 있으므로 제품의 신뢰성을 높일 수 - 9 -

24 있게 된다. 2) 소스코드의 모델체킹 방법을 이용한 테스트 방법론 CC의 EAL6과 같은 고등급 평가를 위해서는 높은 수준의 시험범위(Test Coverage) 를 만족할 수 있는 테스트를 수행하여야 한다. 이를 위해 본 과제에서는 소스코드 에 대한 모델체킹 기법을 적용하고자 한다. 모델체킹은 그 특성상 프로그램이 도달 할 수 있는 모든 상태를 탐색하고 검증속성을위반하는 경우가 발생하면 반례를 통 해 그 경로를 알려주게 되므로, 이를 이용한다면 기존의 테스트 방식이 도달할 수 없었던 높은 수준의 커버리지를 만족할 수 있게 된다. 코드 레벨의 모델 체킹은 현 재 세계적으로 많은 프로젝트가 진행되고 이에 따른 결과물로 여러 종의 코드 레벨 모델체커가 존재한다. 이 중, 대표적인 것이 Microsoft의 SLAM, CMU의 MAGIC, CMBC, ETH의 SATABS 등이 있다. 특히, SATABS나 MAGIC과 같은 도구는 CEGAR(Counter Example Guided Abstraction Refinement) 패러다임을 이용하여 소스코드를 이용하여 위반된 검증 속성의 반례를 보여주는 방식을 가지고 있다. CEGAR은 최근 세계적으로 임베디드 시스템을 코드레벨에서 검증하는 데 많이 사 용되고 있다. 이 프로그램들은 보안의 분야에서 가장 취약점이 되는 다음과 같은 오류들을 발견해 줄 수 있다. Buffer Overflow Pointer Safety (null-pointer dereferences) Division by Zero User Property etc 아래의 그림은 CEGAR의 개략도를 보여주고 있다

25 (그림 1-2) CEGAR 개략도 CEGAR은 소스코드와 검증 속성을 입력하면 이를 모델 체킹을 위한 상태기반의 모 델로 바꿔준다. 그런 뒤 모델 체커 프로그램이 갖을 수 있는 모든 상태를 탐색하여 검증속성이 만족하는 지 여부를 알려주고, 만약 검증 속성이 위반 되었다면 검증 속성이 위반되는 프로그램의 경로를 보여준다. 만약 이 프로그램의 경로가 실제 프 로그램에서 나올 수 있는 경로라면 이를 반례로 보여주고 그렇지 않다면, 다시 모 델의 상태를 세분화(Refinement)하여 다시 검증을 하게 된다. 이렇게 얻어낸 반례는 프로그램의 모든 상태를 탐색한 뒤 얻어낸 프로그램 오류의 경로가 된다. 이 반례 는 경우에 따라 테스트 케이스로 사용 될 수 있다. 하지만, 이러한 프로그램은 개발 시스템의 컴파일러가 제공하는 바이너리 라이브러리는 검증할 수 없고, 하드웨어 모델을 제공하지 않아 본 과제에서 타겟으로 하고 있는 KCOS 운영체제에 대한 적 용이 간단하지 않다. 또한 어셈블리 코드에 대한 검증도 불가능하기 때문에 KCOS 운영체제에 대해 이 방법을 적용할 수 있는 방법을 연구하는 것이 본 과제에서의 핵심이 될 것이다. 2.2 KCOS에 대한 소스코드 수준의 테스트 및 취약성 분석에 개발된 방법론 적용 선행 연구된 테스트 방법론은 스마트 카드를 운영체제 및 응용프로그램인 KCOS에 적용되어, 그 타당성을 검토할 것이다. 하지만, 기존의 테스팅 도구, 정적분석 도구, 모델체킹 도구를 포함한 대부분의 자동화된 테스트 도구는 KCOS와 같은 운영체제 프로그램을 검증하기에는 어려움이 존재한다. 운영체제 프로그램을 검증하기 어려 운 요소는 다음과 같다

26 임베디드 프로세서가 제공하는 바이너리 라이브러리 하드웨어 종속적인 코드 어셈블리 코드 응용프로그램에 의해 동작한다는 운영체제의 특성 이러한 어려움을 해결하는 방법은 테스트 대상과 테스트 대상이 아닌 것을 잘 경계 지어 테스트 대상이 아닌 코드는 테스트 스터브(Test Stub)로 만들고, 운영체제 자 체를 구동시키기 위한 테스트 하니스(Test Harness)를 통하여 운영체제가 응용프로 그램의 요청 없이도 수행 될 수 있도록 환경을 구성하여 테스트 한다. (그림 1-3) 테스트 방법론 2.3 해외 시험 취약성 평가 사례 및 평가 방법론 조사 현재, 고등급 평가를 수행하고 있는 국가들은 영국, 프랑스, 독일과 같은 유럽 국 가, 미국과 최근 결과물을 내고 있는 일본 등이 있다. CCRA에서는 EAL4 등급까지 상호인정을 하고 있으며, EAL5 이상 등급의 세부 평가방법론은 평가 인증을 수행 하는 국가가 필요한 스킴을 수립하도록 권고하고 있다. 이런 이유로 고등급 평가를 진행하는 국가들은 자국에 적합한 평가 인증 스킴을 가지고 있으며, 이를 적용하 여 평가 인증을 진행하고 있다. 국내의 경우는 아직 공식 스킴이 수립되어 있지 않았기 때문에, 해외 고등급 평가 인증 사례를 조사하면서 다른 국가의 평가 스킴과 고등급 평가 정책을 어떻게 적

27 용하고 있는지를 확인하여 향후, 국내 스킴과 정책 수립에 참고자료를 제공할 수 있을 것으로 기대된다. 본 연구에서는 해외 사례를 다음과 같은 부분으로 나누어서 수행하고자 한다. - 정형기법을 적용하여 시험 취약성 분석을 수행한 해외 사례 조사 - CCRA 인증서 발행국에서 최근 수행한 고등급 평가 인증 사례 조사 - 고등급 평가 인증 적용된 시험 취약성 평가 방법론 및 사례 조사

28 제 2 장 해외 공통평가기준 평가 사례 및 동향 분석 이 장에서는 해외 평가 사례와 통계적 수치를 통해 국제적 평가 기술 수준과 평가 동향을 살펴 볼 것이다. 1절에서 전체적은 사례의 통계를 통해 국제적 수준과 동향을 살펴볼 것이고, 2절을 통해 국가별 수준과 평가 동향을 살펴볼 것이다. 그리고, 마지막 3절에서 해외 동향에 대한 결론을 도출할 것이다. 제 1 절 해외 평가 사례 및 통계 분석 1. 전체 등급 상의 통계 [표 2-1] 연도별 등급별 인증 건수 (출처 : Common Criteria Portal) EAL '97 '98 '99 '00 '01 '02 '03 '04 '05 '06 '07 '08 '09 Tot EAL EAL EAL EAL EAL EAL EAL EAL EAL EAL EAL EAL EAL Total

29 [표 2-1]에서 보는 바와 같이 2009년 현재 총 평가 인증 건수는 1037건이 공통평가기준 포털(Common Criteria Portal)에 등재 되어 있고, 2004년 을 기점으로 크게 증가 추세를 보이고 있다. 물론 아직 공통평가기준 포 털에 등록 되지 않은 건수가 존재 한다. 이 부분은 국가별 평가 사례에 서 분석할 것이다. 위의 자료를 토대로 평가 등급별 인증 건수를 살펴보 면 아래 그림 1과 같다. (그림 2-1) 평가 등급별 점유율 (그림 2-1)에서와 같이 전체 등급 중 EAL4+ 등급이 29.41% 가장 높은 점유율을 가지고 있다는 사실을 알 수 있다. 하지만, 고 등급에 속하는 EAL5~EAL7+등급은 전체 중 10%에 못 미치는 것을 알 수 있다. 그 중 에서도 EAL5+가 7.62%로 고 등급 평가의 대부분을 차지하며, EAL6 이 상의 등급은 전부 3건에 불과 하여 세계적으로 고 등급 제품의 개발 기 술 및 평가 기술이 아직은 미성숙 단계에 있다는 것을 확인 할 수 있다

30 (그림 2-2) 제품군별 인증 건수 및 백분율 (출처 Common Criteria Portal) 위의 (그림 2-2)에서 보는 바와 같이 가장 많은 평가 인증 건수를 가지고 있는 제품군은 25.14%로 IC와 스마트카드 하드웨어 제품군이다. 그 뒤를 네트워크 관련 장비와 운영체제가 잇고 있다. 이는 보안 관련 제품의 근 간이 되는 하드웨어와 하드웨어를 운영하기 위한 운영 소프트웨어 즉 운 영체제의 보안성이 확보 되어야만 전체적인 보안 제품의 보안성을 만족 시킬 수 있다는 국제적 요구에 의해 이루어졌다고 판단된다. 따라서, 본 연구과제의 대상 시스템인 스마트카드 운영체제의 평가 제출물 연구는 국제적 요구사항에 맞추어 볼 때, 매우 중요한 부분이며 국내 보안 제품 개발 및 평가 기술에 선도적인 역할을 할 수 있을 것이라고 판단된다

31 2. 고등급 인증의 통계 앞서 통계자료를 통해 다양한 측면에서 공통평가 인증 제품의 현황에 대해 살펴보았다. 이번 항목에서는 본 연구과제의 가장 큰 관심사인 고 등급에 관한 사항을 통계적 수치를 통해 살펴 볼 것이다. [표 2-2] 제품군별 고등급 인증 현황 EAL5 EAL5+ EAL6 EAL6+ EAL7 EAL7+ tot Access Control Boundary Protection Databases ICs & SmartCards Network related Devices Biometric Systems Data Protection Detection Devices Key Management Systems Operating systems Digital Signatures Other Devices, Systems tot 위의 [표 2-2]에서와 같이 접근제어(Access Control), 네트워크 장비, 전 자서명, 데이터베이스 등 대부분의 분야에서는 공통평가기준 시에 저등 급의 평가만을 받아왔고, IC와 스마트카드 관련 하드웨어 그리고, 운영 체제류의 제품이 대부분의 고등급 평가를 받은 제품군임을 알 수 있다. 이 중 대부분이 EAL5+ 등급에 속해 있는 스마트카드 관련 하드웨어 혹 은 플랫폼임을 확인 하였다. 이 중 국내 제품으로는 삼성전자의 스마트 카드 하드웨어가 2건 속해 있음을 알 수 있었다. 대부분의 스마트카드 관련 하드웨어가 EAL5+ 등급의 평가가 이루어 졌다는 것은 국제적으로 스마트카드 하드웨어의 보안 요구 수준을 예상가능하게 해준다. 또한 위

32 의 표에서 알 수 있는 또 다른 사실 하나는 EAL7 등급 이상을 획득한 제품은 Tenix의 Link Diode 뿐이며, Link Diode는 비교적 단순한 장치 이며, 이를 제외 한다면, 현재 가장 높은 수준의 등급을 획득한 제품은 Green Hill Software의 "INTEGRITY-178B separation kernel"이다. 이는 운영체제의 경우 하드웨어에 비해 보다 높은 보안 요구 사항을 만족해야 하고, 국제적으로 이러한 수준의 운영체제를 요구하고 있음을 예상할 수 있다. 또 다른 예로, 공통평가기준는 아니지만, 스마트카드에 탑재되는 Cos인 MULTOS의 경우 CC EAL7 등급과 같은 ITSEC E6 등급을 획득 한 바 있다. 공통평가기준 뿐만 아니라 여러 국제표준에서도 운영체제에 대해 높은 수준의 인증을 요구하고 있는 상황이다. 앞서 언급된 INTEGRITY-178B는 공통평가 뿐만이 아니라 항공분야 표준인 DO-178B 인증을 획득한 바 있다. 제 2 절 국가별 평가 사례 분석 본 절에서는 국가별 평가 사례 분석을 통해 1절에서 분석하지 못했던 자세한 부분에 대해 분석해 볼 것이다. 1. 미국 [표 2-3] 미국 고등급 인증 제품 (출처 : NIAP CCEVS) 제품명 평가등급 제품군 인증일 XTS-400/STOP6.4U4 EAL5+ OperatingSystem Tenix Interactive Link Version 5.1 EAL5+ MultipleDomainSolution XTS-400 / STOP 6.1.E EAL5+ OperatingSystem Tenix Interactive Link Data Diode Device Version 2.1 EAL7 MultipleDomainSolution Tenix Interactive Link Data Diode Device, Gigabit Variant EAL7+ MultipleDomainSolution INTEGRITY-178B kernel separation EAL6+ Operating System

33 미국의 경우 현재 290개의 제품이 평가 인증 되었다. 이 중 5개 제품 만이 EAL5 이상의 고등급 인증을 획득하였다. 그리고, 작은 네트워크 장 치인 Tenix의 Link Data Diode Device가 유일한 EAL7 이상 등급을 획 득하였으며, 이를 제외한 고등급 제품은 운영체제 제품군에 속하는 XTS 시리즈이다. XTS는 EAL5+ 등급을 획득하였다. 또한 현재, 70개의 제품과 보호 프로파일이 평가 중에 있으며, 이중 두 개의 제품이 고등급을 획득하기위해 평가를 받고 있다. [표 2-4] 미국 평가중인 고등급 제품(NIAP CCEVS) 제품명 평가등급 평가시작일 예상완료일 Boeing Secure Network Server EAL Wind River VxWorks MILS 2.0 EAL Boeing Secure Network Server는 현재 EAL7등급을 위한 평가가 진행 중이다. 이 제품은 이미 EAL7 등급을 획득한 Tenix의 장치를 이용한 제 품이다. VxWorks는 실시간 운영체제로서 안전필수 시스템의 필수 인증인 IEC 과 항공분야 필수 인증인 DO-178B의 인증을 받았다. 따라서 VxWorks 운영체제를 사용한 제품은 CC를 포함한 여러 분야의 인증을 받기에 용이해진다. 이 두 경우에서와 같이 최근에 작은 부분을 인증 받 고 이를 이용한 더 큰 제품의 인증을 받는 형태가 나타나고 있다. 이런 이유로 항공, 원자력, 철도와 같은 다른 대형 시스템의 인증을 위해 이에 탑재되는 운영체제를 고등급 평가하려는 시도가 나타나고 있다. 최근 2008년 이후 1건의 제품에 대해 고등급 평가 인증하였고, 현재 2건의 고 등급 평가를 진행중에 있다. 2. 캐나다 현재 76건의 평가 인증 되었지만, 단 한건의 고등급 평가도 이루어지지

34 않았다. 현재 평가 진행 중인 제품의 수는 22건이다. 하지만, 이 역시 고 등급의 평가는 시행되고 있지 않다. (출처 : CSEC) 3. 영국 [표 2-5] 영국 고등급 인증 제품 (출처 : CESG) 제품명 평가등급 제품군 인증일 Datacryptor 2000 Application Software Version 3.3 EAL5 Communications XTS-400 STOP Version 6.4 EAL5+ Operating Systems 영국의 경우 현재 74건의 제품이 평가 인증 되었다. 이 중 2개의 제품 만이 EAL5 등급 이상의 고등급 평가를 받았다. XTS-400의 경우는 동시 에 미국에서 같은 등급을 획득하였다. 그리고, 현재 9개 제품과 보호 프 로파일에 대한 평가 중에 있으며, 이 중 고등급의 평가는 1건도 진행되 고 있지 않다. 최근 2008년 이후 1건의 고등급 평가를 수행하였다. 4. 프랑스 [표 2-6] 프랑스 고등급 인증 제품 (출처 : DCSSI) 제품명 평가등급 제품군 인증일 Microcontrôleur sécurisé SA23YL18A incluant la bibliothèque cryptographique EAL5+ IC NesLib SA révision 1.0 Microcontrôleur sécurisé ST23YL18A EAL5+ IC Microcontrôleur sécurisé SA23YL80B incluant la bibliothèque cryptographique EAL5+ IC NesLib SA révision 1.0 Microcontrôleur sécurisé ST23YL80B EAL5+ IC Microcontrôleur sécurisé ATMEL EAL5+ IC

35 AT90SC12872RCFT / AT90SC12836RCFT rev. M Bibliothèque cryptographique ATMEL Toolbox pour la famille de EAL5+ IC microcontrôleur AT90SC Microcontrôleur sécurisé ST19NR66-A EAL5+ IC Microcontrôleur sécurisé ST19NA18C EAL5+ IC Microcontrôleur sécurisé ATMEL AT90SC12872RCFT EAL5+ IC / AT90SC12836RCFT rev. I et J Microcontrôleur sécurisé ATMEL AT90SC6404RT rev. B EAL5+ IC Microcontrôleur sécurisé ST19NR66B EAL5+ IC Microcontrôleur sécurisé ST19WR66I EAL5+ IC Microcontrôleur sécurisé ATMEL AT90SC12872RCFT rev. E EAL5+ IC Microcontrôleur sécurisé ATMEL AT90SC6404RT rev. I EAL5+ IC Microcontrôleur sécurisé ST19WR08C EAL5+ IC Micro-circuit ST19WP18E EAL5+ IC Micro-circuit ST19WL34A EAL5+ IC Micro-circuit ST19WR66D EAL5+ IC Micro-circuit ST22L128-A rev. L Carte à puce JCLX80jTOP20ID : Java Trusted Open Platform sur composant SLE66CLX800PE Carte COSMOS V1.1: composant P5CT072VOP masqué par la plate-forme COSMO 64 RSA D v5.4 et embarquant l'application EAL5+ IC EAL5+ Smart Card Platform EAL5+ Smart Card

36 IDOne IAS v1.01 (configuration SSCD) 프랑스의 경우 현재 163건의 제품이 평가 인증 되었다. 이 중 21개의 제품과 보호 프로파일이 EAL5 등급 이상의 고등급 평가를 받았다. 특 히 프랑스의 경우 모든 고등급의 인증 제품들이 IC 혹은 스마트카드 플 랫폼 관련 제품임을 알 수 있다. 최근 2008년 이후 7건의 고등급 평가를 수행하였다. 5. 독일 독일의 경우 현재 266건의 제품이 평가 인증 되었다. 이 중 56개의 제 품이 EAL5 등급 이상의 고등급 평가를 받았다. 특히 독일의 경우 모든 고등급의 인증 제품들이 IC 혹은 스마트카드 플랫폼 관련 제품임을 알 수 있다. 가장 많은 수의 고등급 평가를 건수를 가지고 활발히 보안 평 가 활동을 하고 있지만, 많은 수가 Infineon, Philips 등의 특정 기업의 유사 제품에 대한 평가가 이루어 졌음을 알 수 있다. 최근 2008년 이후 20건의 고등급 평가를 수행하였다. [표 2-7] 독일 고등급 인증 제품 (출처 : BSI) 제품명 평가등 급 제품군 인증일 Processor Resource/System Manager (PR/SM) for the IBM eserver zseries 900 EAL Processor Resource/System Manager (PR/SM) for the IBM eserver zseries 800 and 900 GA3 EAL Processor Resource/System Manager (PR/SM) for the IBM eserver zseries 990 EAL PR/SM LPAR for the IBM eserver zseries z890 and z990 EAL PR/SM LPAR for the IBM System z9 109 EAL PR/SM LPAR for the IBM System z9 Enterprise Class and the IBM System z9 Business Class EAL Processor Resource / Systems Manager (PR/SM)for the IBM System z10 EC GA1 EAL Philips Smart Card Controller P8WE6017 V1I EAL5+ smart cartd GemXplore'Xpresso V3 - Java Card Platform 내장 Software V3 (Core) EAL5+ smart cartd

37 Philips Smart Card Controller P8WE6004 V0D EAL5+ smart cartd Smart Card IC (Security Controller) SLE66CX322P with RSA 2048/m1484a23 EAL5+ smart cartd GemXpresso Pro E64 PK - Java Card Platform 내장 Software V3 (Core) EAL5+ smart cartd Philips Smart Card Controller P8WE5033V0G EAL5+ smart cartd Philips Smart Card Controller P8WE5033V0F EAL5+ smart cartd Philips Smart Card Controller P8WE6017V1J EAL5+ smart cartd Philips Smart Card Controller P16WX064V0C EAL5+ smart cartd Infineon Smart Card IC (Security Controller) SLE66CX322P with RSA 2048/m1484a24, m1484a27 and m1484b14 EAL5+ smart cartd Infineon Smart Card IC (Security Controller) SLE88CX720P / m1491b13 with PSL V L EAL5+ smart cartd Philips P5CC009V0M Secure Smart Card Controller EAL5+ smart cartd Philips P5CC036V0M Secure Smart Card Controller EAL5+ smart cartd Infineon Smart Card IC (Security Controller) SLE66CX322P with RSA 2048 m1484b14 and m1484f18 Philips P5CT072V0M and P5CC072V0M Secure Smart Card Controller Philips P5CC036V1C and P5CC009V1C Secure Smart Card Controller Infineon Smart Card IC (Security Controller) SLE66C82P/m1474a15 and SLE66C42P/m1495a15 Infineon Smart Card IC (Security Controller) SLE66CX322P / m1484b14 and m1484f18 EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd Infineon Smart Card IC (Security Controller) SLE66CX642P/m1485b16 with RSA 2048 V1.30 and specific EAL5+ smart cartd IC Dedicated Software Philips P5CC036V1D and P5CC009V1D with specific IC Dedicated Software Secure Smart Card Controller Philips P5CC036V1C and P5CC009V1C with specific IC Dedicated Software Secure Smart Card Controller Infineon Smart Card IC (Security Controller) SLE66CX680PE/m1534a13 and SLE66CX360PE/m1536a13 both with RSA 2048 V1.4 and specific IC Dedicated EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd Software Infineon Smart Card IC (Security Controller) SLE66C168PE/m1530-a25, SLE66C84PE/m1538-a25, SLE66C44PE/m1539-a25 and SLE66C24PE/m1563-a25 with specific IC Dedicated Software Philips Secure Smart Card Controller P5CT072V0N including OM9500/1 and OM9501/2, P5CD072V0N and P5CD036V0N EAL5+ smart cartd EAL5+ smart cartd with specific IC Dedicated Software Infineon Smart Card IC (Security Controller) SLE66CLX640P/m1523-a11 and SLE66CLX641P/m1522-a11 EAL5+ smart cartd

38 both with RSA2048 V1.3 and specific IC Dedicated Software Infineon Smart Card IC (Security Controller) SLE66CX162PE/m1531-a24 and SLE66CX80PE/m1533-a24 both with RSA 2048 V1.4 and specific IC Dedicated Software Infineon Smart Card IC (Security Controller) SLE66CLX320PS / m1554b21 and SLE66CLX160PS / m1525b21 both with RSA2048 V1.3 and specific IC Dedicated Software Infineon Smart Card IC (Security Controller) SLE66CLX320P/m1559b19 and SLE66CLX321P/m1359b19 both with RSA2048 V1.3 and specific IC Dedicated Software Infineon Smart Card IC (Security Controller) SLE88CFX4000P/m8830b17, SLE88CFX4002P/m8834b17, SLE88CFX3520P/m8847b17 and SLE88CFX2920P/m8849b17 each with PSL V and specific IC Dedicated Software Philips Secure Smart Card Controller P5CT072V0Q, P5CD072V0Q, P5CD036V0Q, including specific Inlay Packages OM95xx, each with specific IC Dedicated Software Philips Secure Smart Card Controller P5CT072V0P, P5CC072V0P, P5CD072V0P and P5CD036V0P each with specific IC Dedicated Software Infineon Smart Card IC (Security Controller) SLE66CL80P/m1457-a14 and SLE66CL81P/m1436-a14 with specific IC Dedicated Software Infineon Smart Card IC (Security Controller) SLE66C166PE/m1532-a24 with specific IC Dedicated Software Philips Secure Smart Card Controller P5CD009V2A and P5CC009V2A each with specific IC Dedicated Software Philips Secure Smart Card Controller P5CD009V2B with specific IC Dedicated Software Infineon Smart Card IC (Security Controller) SLE88CFX4000P/m8830b17, SLE88CFX4002P/m8834b17, SLE88CFX3520P/m8847b17, SLE88CFX2920P/m8849b17, SLE88CF4000P/m8845b17, SLE88CF4002P/m8846b17, SLE88CF3520P/m8848b17, SLE88CF2920P/m8850b17 each with PSL V _E107 or PSL V _E110 and specific IC Dedicated Software Infineon Smart Card IC (Security Controller) SLE66CL80P / m1457a14 and SLE66CL81P / m1436a14 with specific IC Dedicated Software Infineon Smart Card IC (Security Controller) SLE66CLX800PE / m1581-e12, SLE66CLX800PEM / m1580-e12, SLE66CLX800PES / m1582-e12, SLE66CLX360PE m1587-e12, SLE66CLX360PES / m1589-e12 with specific IC Dedicated Software EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd

39 Infineon Smart Card IC (Security Controller) SLE88CFX4001P/m8835b18, SLE88CFX4003P/m8837b18, SLE88CFX3521P/m8857b18, SLE88CFX2921P/m8859b18 each EAL5+ smart cartd with PSL V and specific IC Dedicated Software NXP Secure Smart Card Controller P5CT072V0N, P5CD072V0N, P5CD036V0N, including specific Inlay EAL5+ smart cartd Packages OM95xx, each with specific IC Dedicated Software NXP Secure Smart Card Controller P5CD144V0B, P5CN144V0B and P5CC144V0B each with specific IC EAL5+ smart cartd Dedicated Software NXP Secure Smart Card Controller P5CD080V0B, P5CN080V0B and P5CC080V0B each with specific IC EAL5+ smart cartd Dedicated Software NXP Secure Smart Card Controller P5CD040V0B, P5CC040V0B, P5CD020V0B and P5CC021V0B each with EAL5+ smart cartd specific IC Dedicated Software Infineon Smart Card IC (Security Controller) SLE66CL180PE / m1585-e12, SLE66CL180PEM / m1584-e12, SLE66CL180PES / m1586-e12, SLE66CL81PE / m1594-e12, SLE66CL81PEM / m1595-e12, SLE66CL80PE / m1591-e12, EAL5+ smart cartd SLE66CL80PEM / m1592-e12, SLE66CL80PES / m1593-e12, SLE66CL41PE / m1583-e12 with specific IC Dedicated Software Infineon Smart Card IC (Security Controller), SLE66CLX800PE / m1581-e12, SLE66CLX800PEM / m1580-e12, SLE66CLX800PES / m1582-e12, EAL5+ smart cartd SLE66CLX360PE / 1587 e12, SLE66CLX360PEM / m1588-e12, Infineon Smart Card IC (Security Controller)SLE66CLX800PE / m1581-e13/a14, SLE66CLX800PEM / m1580-e13/a14, SLE66CLX800PES / m1582-e13/a14, SLE66CX800PE / EAL5+ smart cartd m1599-e13/a14, SLE66CLX360PE Infineon Smart Card IC (Security Controller), SLE66CX680PE / m1534-a14, SLE66CX360PE / m1536-a14, SLE66CX482PE / m1577-a14, SLE66CX480PE / 1565-a14, SLE66CX182PE / EAL5+ smart cartd m1564-a14, all optional with RSA 2048 V1.5 and all with specific IC dedicated software NXP Smart Card Controller P5CC024V0A, P5CC020V0A, P5SC020V0a and P5CC012V0A each with IC Dedicated EAL5+ smart cartd Software: Secured Crypto Library Release 2.0 to CC EAL5+ NXP Smart Card Controller P5CD080V0B with Dedicated software: Secured Crypto Library Release 2.0 EAL5+ smart cartd NXP Smart Card Controller P5CC037V0A with specific IC Dedicated Software EAL5+ smart cartd NXP Smart Card Controller P5CC052V0A with specific IC Dedicated Software EAL5+ smart cartd NXP Smart Card Controller P5CD040V0B with IC dedicated EAL5+ smart cartd

40 software: Secured Crypto Library Release 2.0 to EAL5+ S3CC9LC 16-bit RISC Microcontroller for Smart Card, Revision 2 NXP Smart Card Controller P5CD144V0B with IC Dedicated Software, Secured Crypto Library Release 2.0 Infineon Smart Card IC (Security Controller) SLE66CX162PE /m1531-a24 and SLE66CX80PE / m1533-a24 both optional with RSA2048 V1.5 and ECC V1.1 and both with specific IC dedicated software Infineon Smart Card IC (Security Controller) SLE66CL180PE / m1585-a14, SLE66CL180PEM / m1584-a14, SLE66CL180PES / m1586-a14,sle66cl81pe / m1594-a14, SLE66CL81PEM / m1595-a14, Infineon Smart Card IC (Security Controller) SLE66CLX1600PEM / m1590-a12, SLE66CLX1600PE / m1596-a12, SLE66CLX1600PES / m1597-a12, SLE66CX1600PE / m1598-a12, SLE66CLX1440PEM / Infineon Smart Card IC (Security Controller) SLE66CL187PEM / m2984-a11, SLE66CL187PE / m2985-a11, SLE66CL187PES / m2986-a11, SLE66CL88PEM / m2995-a11, SLE66CL88PE / m2994-a11, NXP Smart Card Controller P5CC024V0A, P5CC020V0A, P5SC020V0A, P5CC012V0Aall with IC dedicated software:secured Crypto Library Release 2.0 NXP Smart Card Controller P5CC037V0Awith IC dedicated software:secured Crypto Library Release 2.0 NXP Smart Card Controller P5CC052V0Awith IC dedicated software:secured Crypto Library Release 2.0 Atmel Smartcard ICs AT90SC28872RCU / AT90SC28848RCU with Atmel Cryptographic Toolbox Version or NXP J3A080 v2.4.1 Secure Smart Card Controller (JCOP v2.4.1) EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd EAL5+ smart cartd 호주/뉴질랜드 호주/뉴질랜드의 경우 현재 30건의 제품이 평가 인증 되었다. 이 중에 서 공통평가기준을 통해 고등급의 인증을 받은 제품은 단 한건도 존재하 지 않는다. 하지만, ITSEC을 통한 다수의 인증 사례와 함께 ITSEC 고등 급 인증 사례가 존재한다. EAL5~EAL7에 해당하는 E4~E6 등급으로 인 증된 제품이 10건 존재 한다. 특히 공통평가 기준의 EAL7에 해당하는

41 등급을 받은 제품은 7개 제품이나 된다. 따라서 호주/뉴질랜드는 고등급 평가를 위한 기술력을 갖추었다고 판단된다. 그리고, 이중 3건이 스마트 카드 운영체제와 관련이 있고, 나머지 7건은 네트워크 보안 관련 제품인 것이 특징적이다. 고등급 평가에 있어, 다른 지역이 주로 IC와 스마트카 드 하드웨어 관련 제품의 평가가 이루진 반면 호주/뉴질랜드 지역은 네 트워크 보안 관련 제품과 운영체제의 평가 인증 건수가 두드러진다. [표 2-8] 호주/뉴질랜드 ITSEC 고등급 인증 제품 (출처 : DSD) 제품명 평가등급 제품군 인증일 BAE Systems Mobile Trusted Filter E5 Network Security Products 2007 BAE Systems Trusted Filter V1 E5 Network Security Products 2001 Serial Data Regulator V1 E6 Network Security Products 2003 Interactive Link Multiple Computer Switch V2.0 E6 Network Security Products 2000 Interactive Link Data Diode Device V1.2 E6 Network Security Products 1999 CSX-100 V1 E6 Network Security Products - Interactive Link V3 E6 Network Security Products 2000 MULTOS V1Q E6 Smart Card Products (Operating System) 2003 MULTOS V1N E6 Smart Card Products (Operating System) 2003 STARCOS SPK 2.3 E4 Smart Card Products (Operating System)

42 현재 호주/뉴질랜드 지역은 8건의 평가가 진행되고 있다. 이 중 2009년 까지 1건의 EAL7 등급의 평가가 완료 될 예정이다. 평가 완료 예정인 제품은 아래와 같다. [표 2-9] 호주/뉴질랜드 평가중인 고등급 제품(출처 : DSD) 제품명 평가등급 평가시작일 예상완료일 Secure Optical Switch EAL 일본 일본의 경우 현재 213건이 평가 인증 되었지만, 단 한건의 고등급 평가 도 이루어지지 않았다. 현재 평가 진행 중인 제품의 수는 12건이다. 하지 만, 이 역시 고등급의 평가는 시행되고 있지 않다. (출처 : IPA) 8. 네덜란드 네덜란드의 경우 현재 총 7건의 제품이 평가 인증 되었지만, 단 한건의 고등급 평가도 수행되지 않았다. 또한 현재 평가 진행 중인 사례는 찾지 못했다. (출처 : TNO-Ceritification BV) 9. 노르웨이 노르웨이의 경우 현재까지 4건의 제품이 평가 인증 되었다. 이중 EAL5 이상의 고등급에 해당하는 제품은 2건이 있다. 인증 건수 자체는 매우 적지만, 높은 비율로 고등급의 평가가 이루어지고 있다고 판단된다

43 [표 2-10] 노르웨이 고등급 인증 제품 (출처 : SERTIT) 제품명 평가등급 제품군 인증일 Trusted Security Filter EAL5 Data Filtering Mechanism Thales Operator Terminal Other Devices and EAL5 Adapter Systems 현재 평가 중에 있는 제품은 4건이지만, 이중 고등급 평가는 수행되고 있지 않다. 10. 스페인 스페인의 경우 현재 14건이 평가 인증 되었지만, 단 한건의 고등급 평 가도 이루어지지 않았다. 현재 평가 진행 중인 제품의 수는 9건이다. 하 지만, 이 역시 고등급의 평가는 시행되고 있지 않다. (출처 : CCN) 11. 스웨덴 스웨덴의 경우 현재 총 2건의 제품이 평가 인증 되었지만, 단 한건의 고등급 평가도 수행되지 않았다. 또한 현재 평가 진행 중인 사례는 찾지 못했다. (출처 : FMV CSEC)

44 제 3 절 해외 동향 분석 결과 (그림 2-3) 국가별 공통평가기준 인증 현황 그림 3에서와 같이 미국, 독일, 일본, 프랑스 순으로 제품에 대한 CC 인증 건수가 많다. 이상의 순서대로 평가 인증 활동이 활발함을 알 수 있다. 하지만, 그림 4에서와 같이 고등급일 경우에는 상황이 달라진다. 독일의 인증 건수가 전체에 60%, 프랑스가 전체의 23%에 달할 정도로 많은 제품의 인증 건수를 보여 준다. 반면에 일본과 미국 등은 상대적으 로 낮은 수의 고등급 인증 건수를 보여준다. 또한 독일, 프랑스, 미국 등 을 제외한 대부분의 국가들이 고등급 평가의 경험을 가지고 있지 않다. 이는 소수의 국가만이 고등급 평가 기술을 가지고 있고, 많은 국가의 제 조사들이 고등급 인증을 받기 위해서는 독일, 프랑스, 미국 등의 소수국 가에서 평가를 받아야 하는 상황이 발생하게 된다. 이럴 경우, 비용적으 로 외화낭비가 발생할 수 있을 뿐만 아니라, 국내 기술의 유출도 걱정해 야할 문제이다

45 (그림 2-4) 국가별 등급별 고등급 CC 인증 현황 전체적으로 볼 때, 고등급 인증의 건수로는 독일과 프랑스가 우위에 있 지만, 두 국가 모두 IC와 스마트카드에 편중되어 있는 면이 있다. IC 혹 은 스마트카드의 컨트롤러 등은 국제적인 추세가 EAL5+ 등급을 요구하 고 있는 상황이다. 이에 따라 독일과 프랑스가 많은 수의 고등급(EAL5+) 등급을 보유하고 있지만, 미국의 경우는 EAL6+ 등급과, EAL7, EAL7+ 등급을 평가한 경험을 가지고 있다. 현재 EAL7 등급의 Boeing Secure Network Server 와 EAL6+의 Wind River VxWorks MILS 2.0 을 평가 하고 있어, 고등급 평가를 위한 높은 수준의 기술력을 가지고 있음을 확 인할 수 있었다. 호주/뉴질랜드의 경우도 공통평가기준(CC)의 고등급 평 가 능력을 가지고 있지는 않지만, 이에 상응하는 ITSEC의 고등급 평가 경험을 가지고 있다. 현재 EAL7 등급의 Secure Optical Switch 을 평가 하고 있어, 미국과 마찬가지로 고등급 평가를 위한 높은 수준의 기술력 을 가지고 있음을 확인할 수 있다

46 제 3 장 정형 명세 언어의 소개 이번 장에서는 본 연구의 내용이해를 돕기 위한 기술들을 설명한다. 제 1 절 정적분석도구 Frama-C 1. Frama-C 소개 Frama-C는 C언어를 위한 모듈정적분석 프레임워크이다. 이 매뉴얼은 Frama-C의 수치분석(value analysis) 플러그인에 대한 문서이다. 수치분 석 플러그인은 프로그램의 변수들에 대하여 가능한 값들의 집합을 자동 적으로 계산한다. 각 분석된 함수에 관한 종합의 정보(synthetic information)는 수치분석에 의해 제공되는 값들로부터 자동적으로 계산 될 수 있다. 프레임워크, 수치분석 플러그인 등은 모두 Open Source 소 프트웨어로서, 다운받을 수 있다. (1) 기본 기능 Frama-C는 두 종류의 인터페이스로 구성 되어있다. 일괄실행(Batch)과 상호작용(Interactive)이다. Frama-C의 상호작용 그래픽 인터페이스는 분 석된 소스코드의 표준화된 버전을 보여준다. 이 인터페이스에서, 수치분 석 플러그인은 사용자가 코드에 있는 표현식을 선택하는 것을 허용하고 실행시간에 이 표현식이 취할 수 있는 값들의 집합의 over-approximation을 관찰한다. 다음은 C 예제이다. 1 int y, z=1;

47 2 int f(int x) { 3 y = x + 1; 4 return y; 5 } 6 7 void main(void) { 8 for (y = 0; y < 2+2; y++) { 9 z = f(y); 10 } 11 } 만약 Frama-C가 옵션 -val introduction.c와 함께 실행되면, 수치분석 플 러그인은 함수 f의 return 명령문을 통해 각 passage에서 전역변수 y와 z가 각 1 또는 3을 포함하는 것을 보장할 수 있다. 함수 main의 마지막 에서, y는 반드시 4를 포함하고 z의 값은 다시 1 또는 3임을 지적한다. 플러그인이 y의 값이 함수 f의 마지막에서 1 또는 3이라는 것을 가리킬 때, 이것은 전체 실행 프로그램 지점을 통하여 각 passage에서 y에 저장 될 수 있는 모든 변수들의 union을 절대적으로 계산한다. 이런 결정론적 인 프로그램의 실제 실행에서, 함수 main의 마지막일지라도 오직 하나의 passage가 있고, 그러므로 이 지점에서 오직 z를 위한 값이 하나 있다. 수치분석에 의해 주어진 대답은 대략적이고 정확하다.(실제 값 3은 제안 된 값들 중에 있다) 수치분석에 대한 이론적인 프레임워크는 요약해석(Abstract Interpretation)이라고 불린다. (2) 실행시간 오류 다음 프로그램의 경우처럼 분석된 어플리케이션은 실행시간 오류(0으로

48 나누는 것, 유효하지 않은 포인터 접근 등)들을 포함할 수 있다. 1 int i, t[10]; 2 void main(void) { 3 4 for(i = 0; i <= 8+2; i++) 5 t[i] = i; 6 } 명령에 frama-c -val rte.c와 함께 인스턴스에 대하여 실행할 때, 수치해 석은 5번째 라인에서 out-of-bound 접근에 대한 경고를 말해준다. rte.c:5: Warning : accessing out of bound index assert((0 <= i) && (i < 10)); 실제로 프로그램에서 이 라인에 out-of-bound 접근이 있다. 근사치 (approximation)들은 그것의 전체 계산들을 만들기 때문에 Frama-C는 어떤 실행시간 오류들을 야기하지 않는 구조들에 대해 경고라고 말해주 는 경우도 있다. 이런 것을 false alarm 이라고 한다. 이와 반면에 수치 분석은 정확한 계산을 한다는 것과, 가능한 값들의 over-approximated 집합은 실행시간오류를 포함하고 있는 프로그램에 조용하게 남는 것을 예방한다는 사실에 주목하자. 2. 값 해석(Value Analysis) 기법 (1) 값 수치분석 플러그인은 주어진 프로그램 지점에서 변수 x의 값에 관련하 여 질의를 처리할 수 있다. 이것은 모든 가능한 실행에 대하여 지정된

49 지점에서 x에 의해 가능하게 취해질 수 있는 값들의 집합의 over-approximation을 지니고 있는 질의와 같은 것에 대답한다. - Interactive and programmatic interfaces 사용자(GUI을 통한) 또는 고객 플러그인(모듈러 Db.Value에 등록된 함 수들 호출을 통하여)은 명시된 명령문, l-value, 또는 임의의 표현식에 평 가(evaluation)를 요청할 수 있다. 그러므로 이런 l-value 또는 표현식이 실제의 실행에서 선택된 명령문이 도달되기 바로 전에 어떤 지점을 가지 고 있는 모든 값들을 포함하는 variation 도매인을 얻는다. 함수!Db.Value.access는 사용자 플러그인으로 제공되는 함수들 중에 하 나이다. 이것은 프로그램 지점(of type Cil_types.kinstr)을 취하고, l-value(of type Cil_types.lval)의 대표 값(representation)과 프로그램 지 점에서 l-value에 대해 가능한 값들의 대표 값(representation)을 반환한 다. 또 다른 함수!Db.Value.lval_to_loc는 l-value의 대표 값(representation) 을 메모리에 공간을 위한 분석기의 abstract representation인 기억장소 (of type Locations.location)로 해석한다. 이 함수에 의해 반환된 기억장 소는 산술적이거나 메모리 접근의 해제(free of memory)이다. 제공된 프 로그램 지점은 l-value 내부에 있는 표현식 안에 나타나는 변수들의 값 을 instantiating하는데 사용된다. 사용자 플러그인은 추상 기억장소 (abstract location)에 대하여 완전하게 이론(reason)이 될 것이고, 포인터 들의 문제와 aliasing을 다루는 것을 완전하게 피한다. 사용자 플러그인을 작성하는 것에 대한 많은 정보는 Frama-C Plug-in Development Guide에서 찾아볼 수 있다

50 - Variation domain 변수 또는 표현식의 variation 도메인은 다음에 설명되는 형태들 중에 하 나를 취할 수 있다. A set of integers 변수의 variation 도메인은 정수들의 집합이 되기 위한 분석에 의해 결정 될 것이다. 이것은 보통 정수 타입의 변수들에 대하여 발생하고, 만약 어 플리케이션이 unions 또는 cast를 포함한다면 다른 변수들을 대해 일어 날 것이다. 그러한 정수들의 집합은 다음과 같이 나타낼 수 있다. an enumeration, {v1;... vn ;}, an interval, [m.. l], m과 l 사이를 구성하는 모든 정수를 나 타낸다. 만약 -- 이 낮은 바운드(bound) l으로써 나타나면, 이것은 낮은 바운드 - 를 의미한다.(높은 바운드는 + ), 주기성 정보와 함께 interval은, [l.. u], r%m, m에 의해 Euclidean division에서 나머지가 r과 동일한 l과 u 사이의 구성된 값들 의 집합을 나타낸다. 예를 들어, [2..42],2%10은 2, 12, 22, 32 그리고 42를 포함하는 집합을 나타낸다. A floating-point value or interval 메모리(전형적인 floating-point 변수)에 있는 기억장소는 floating-point 숫자 또는 floating-point 숫자들의 interval을 포함할 것이다

51 0이 아닌 floating-point 숫자 f (floating-point 숫자 +0.0은 정 수 0으로써 같은 대표 값을 갖고 그것과 같이 동일시된다)를 위한 f. fm으로부터 fm까지의 간격을 위한 [fm.. fm]를 포함. A set of address Variation 도메인(예를 들면 포인터 변수들을 위한)은 주소들의 집합이 될 것이고, {{a1;... an; }}으로 표시된다. 각 ai의 형태는 다음과 같다. &x+d, &x는 변수 x와 일치하는 기본 주소이고, D는 정수 값 들의 도메인에 있고 기본 주소 &x에 대한 바이트로 표현된 가능한 offset들을 나타낸다. NULL+D, 정수들 D의 집합을 위한 또 다른 표시법이다(기본 주소 NULL에 대한 offsets). An imprecise mix of addresses 만약 어플리케이션이 주소를 넘어 다른 수학적 오퍼레이션을 포함하면, variation 도메인들의 많은 것들은 형태 garbled mix of &{ x1;... xn;}의 집합들이 부정확하게 되는 분석에 의해 제공된다. 이런 표현은 변수 x1... xn의 주소들로의 그리고 정수들로의 arithmetic operation을 적용하는 것으로부터 만들어진 알지 못하는 값을 나타낸다. Absolutely anything 실제로 이것을 관찰해서는 안 된다. 가끔 분석자는 변수의 variation 도 메인에 대해 ANYTHING을 나타내는 경우 모든 변수의 값 위에 어떤 정보를 추론하지 못할 것이다

52 - Interpreting the variation domains 현대의 C 언어를 위한 컴파일레이션 플랫폼들은 정수 값과 절대주소들 을 통합한다. 정수 256의 인코딩과 주소 (char*)0x 사이의 차이점 은 없다. 그러므로 수치분석은 이런 두 값들 사이를 구별하지 않는다. floating-point 계산에서, 수치분석은 NaN, +, 또는 - 를 얻는 것은 원 하지 않는 오류라는 것을 고려한다. 분석에 의해 제공된 floating-point intervals는 항상 유한한 floating-point 값들의 intervals이다. Example of variation domains [ ]은 1과 256사이의 구성되는 정수의 집합을 나타내 고, 각각은 0x1 그리고 0x100 사이의 절대주소로써 해석될 수 있다. [ ], 0%2는 0부터 256사이의 짝수정수의 집합을 나타낸 다. 이런 집합은 메모리에서 정렬된 16-bit word들의 첫 번째 129의 주 소들의 집합이다. 낸다. [ ]. 1%2는 1과 255사이의 구성된 홀수 정수들을 나타 [ ]는 모든 정수들의 집합(가능하면 음수도)을 나타낸다. 3. floating-point 숫자 3.0을 나타낸다. [ ]는 -3.0부터 9.0사이의 구성된 floating-point 값들의 간격을 나타낸다

53 {{&x + { 0; } ; }}는 변수 x의 주소를 나타낸다. {{ &x + { 0; 1; } ; }}는 변수 x의 첫 번째 두 바이트들 중의 하나의 주소를 나타낸다(x는 적어도 2바이트 이상이라고 가정). 만약 그 렇지 않다면, 이런 표기는 유효하지 않은 주소들과 x의 주소를 포함하고 있는 집합을 나타낸다. {{ &x + { 0; } ; &y + { 0; } ; }}는 x와 y의 주소를 나타낸다. {{ &t + [ ], 0%4; }}, 어플리케이션에서 t는 32-bit 정수 의 배열로써 선언되고, 위치 t[0], t[1],..., t[64]의 주소를 나타낸다. {{ &t + [ ] ; }}는 변수 i가 0과 256사이의 정수 값으로 구성되었을 때 표현식 (char*)t+i로써 같은 값들을 나타낸다. {{ &t + [--..--] ; }}는 misaligned 그리고 유효하지 않은 것을 포함하여 t를 시프팅(shifting)함으로써 얻어지는 모든 주소들을 나타낸 다. - Origins of approximations heavy approximation들로부터의 결과인 값들은 이런 approximations의 origin에 대한 정보를 포함한다. 값이 V (origin :...) 으로써 나타나는 경우이다. 텍스트는 기억장소와 이런 approximation들의 몇몇의 원인 (cause)을 나타내는 origin : 후에 제공한다. origin은 다음 것들 중에 하나가 될 수 있다. - Misaligned read

54 origin Misaligned L은 정확하게 되는 계산을 방해하는 misaligned read 들이 있는 어플리케이션에서 라인들의 집합 L을 나타낸다. Misaligned read는 bits read가 전체 bit들의 집합이 정확하게 변경된 single write로 써 이전에 쓰이지 않은 memory read-access이다. misaligned read를 이 끌어 내는 프로그램의 예제는 다음과 같다. 1 int x, y; 2 int *t[2] = { &x, &y }; 3 4 int main(void) 5 { 6 return 1 + (int) * (int*) (( int ) t+2); 7 } 함수 main에 의해 반환되는 값은 {{ garbled mix of &{ x; y; } (origin : Misaligned { misa.c:6; }) }} 이다 분석기는 32-비트 아키텍처에 대해 디폴트에 구성되었다는 것을 기억하 고, 결과적으로 read memory access는 out-of-bound access가 아니다. 만약 이것이 그렇다면, 이것은 경고의 원인이 되고 경고할 것이다. 디폴트 타겟 플랫폼과 함께, read access는 배열 t의 바운드 안에 남고, 두 바이트들의 offset이기 때문에, 32-bit word read는 t[1]으로부터 처음 두 번째 그리고 t[0]으로부터 마지막 두 바이트들로 구성된다. - Call to an unknown function origin Library function L은 재귀적인 함수들 또는 값을 정확하게 알지 못하는 함수 포인터들로의 호출의 결과를 위해 사용된다

55 - Fusion of values with different alignments 표기법 Merge L은 모순된 alignments가 함께 fuse된 것과 함께 메모리 상태들 위치의 분석된 코드 안의 라인들의 집합 L을 나타낸다. 아래에 있는 예제에서 then 분기와 else 분기로부터 메모리 상태들은 배열 t 안 에 몇몇의 32-bit 주소들을 모순된 alignments와 함께 포함한다. 1 int x, y; 2 char t[8]; 3 4 int main(int c) 5 { 6 if(c) 7 * (int **) t = &x; 8 else 9 * (int **) (t+2) = &y; 10 x = t[2]; 11 return x; 12 } 함수 main에 의해 반환되는 값은 {{ garbled mix of & { x; y; } (origin : Merge { merge.c:9; }) }} 이다. - Arithmetic operation origin Arithmetic L은 분석기가 정확하게 결과를 나타낼 수 있는 것 없 이 arithmetic operation이 발생하는 라인들의 집합 L을 나타낸다

56 1 int x, y; 2 int f (void) 3 { 4 return (int) &x + (int) &y; 5 } 이 예제에서 함수 f는 다음을 반환한다. {{ garbled mix of & { x; y; } (origin : Arithmetic { ari.c:4}) }} - Well value 몇몇의 상황들에서, 분석기는 정보에 대해 오직 그것의 타입과 함께 변 수에 대한 가능한 값들의 집합을 생성해야 한다. 몇몇의 재귀 또는 깊이 연결된(chained) 타입들은 애매함을 포함하는 변수들에 대해 생성된 콘 텐츠들을 집행할 것이다. absorbing 값들은 well value들이라고 불린다. 계산들은 애매하고 Well value이기 때문에 origin: Well 로써 표시된다. (2) 값 해석에 대한 로그 메시지 이 부분은 분석기(frama-c)의 batch 버전에서 수치분석에 의해 나타나는 메시지들을 분류한다. Graphical interface(frama-c gui)를 사용할 때, 메 시지들은 쉬운 접근법인 다른 패널(panel)들로 수신되고 지시된다. - Results Frama-C의 batch 버전과 함께, 계산들의 결과들은 표준출력(standard output) 위에 나타난다. 몇몇의 계산들에 대하여 정보는 계산되고, human-readable way에서 쉽게 나타나게 될 수 없다. 이런 경우, 이것은

57 보이지 않고, GUI 또는 프로그램적이게 통해 오직 접근될 수 있다. 다른 경우에는 절충안은 도달되어야 한다. 예를 들어, 변수들에 대한 variation 도메인들일지라도 분석된 어플리케이션의 실행에서 어떤 지점, 오직 batch 버전만 나타나고, 각 함수들에 대하여, 함수들의 끝에 도달할 때마 다 잡고 있는 값들에 대하여 이용가능하다. - Proof obligations 수치분석에 의해 제공되는 결과들의 정확성은 오직 사용자가 분석하는 동안에 생성되는 모든 proof obligation들을 검증하여 보장된다. Frama-C 의 현재 버전에서 이런 proof obligation들은 Warning:... 그리고 alarm 또는 assert를 포함하는 것과 함께 시작되는 메시지로써 나타난다. Frama-C는 모든 플러그인에 대한 일반적인 명세 언어인 ACSL로 구성되 어 있다. Proof obligation들의 대부분은 ACSL에서 표현되는 수치분석에 의해 발생한다. 각 proof obligation 메시지는 nature 그리고 obligation의 origin을 포함한다. Annotate된 proof obligation들과 함께 분석된 소스코드의 버전을 획득하 는 것이 가능하다. 아직 ACSL에 표현되지 않은 proof obligation들은 출 력 소스코드로부터 missing이다. ACSL assertion들로써 표현된 이런 경 고들에 대하여, ACSL의 syntax가 사용되고, ACSL에 대해 수치분석의 지원은 오류의 부재를 보증하는 ACSL 상태에서 그것들을 정확하게 표 현하기 위한 이런 공식으로부터 몇 몇의 명백한 coercion operation들은 missing될 것이고 여전히 일부분이다. 이 버그는 이후의 버전에서 고쳐 질 것이다. Division by zero 분석은 non-null이 되는 것을 보장하지 않는 표현식에 의해 나누기를 할

58 때, proof obligation은 발생한다. 이 obligation은 코드의 이 지점에서 나 눗수가 0과 다르다는 것을 나타낸다. 나눗수에 대하여 0이 오직 가능한 값이 되는 실제의 경우에 대하여, 분 석은 이 분기에 대하여 멈춘다. 만약 나눗수가 non-zero 값이 될 수 있 을 것처럼 보이면, 분석기는 분석을 계속하고 이 지점 후에 나눗수가 0 과 다르다는 속성들을 고려하여 허용한다. 속성은 경고에 의해 표현되고, 이것이 쉽게 되지 않는다는 것을 고려하지 않을 것이다. 1 int A, B; 2 void main ( int x, int y) 3 { 4 A = 100 / (x * y); 5 B = 333 % x; 6 } div.c :4: Warning : division by zero : assert (x*y!= 0);... div.c :5: Warning : division by zero : assert (x!= 0); 위의 예제에서, x*y가 null이 아니라는 것을 분석기에게 보장할 방법이 없다. 그래서 경고를 발생한다. 이론에서, 발생을 피하기 위해서는 alarm x!= 0을 라인 5번째에 쓴다. 이 속성은 라인 4에서 경고로써 방출되는 속성의 결과이기 때문이다. 이런 경우보다 더 간단한 경우일지라도 쓸모 없는 경고들이 발생한다. 그런 것에 대해서는 놀라지 말자. Unspecified logical shift 또 다른 Arithmetic 경고는 두 번째 인자가 타겟 타입의 크기보다 커지 게 되는 논리적인 정수에 대하여 shift operation에 대해 발생하는 경고

59 이다. 그러한 operation은 ISO/IEC 9899:1999 표준에 의해 명시되지 않 고 남게 된다. 프로세스들은 그런 operation이 보통 기대될 수 있는 0 또 는 -1 결과를 생성하지 않는 방법으로 만들어져 있다. 여기서 이런 문제 에 대한 예제가 있고 경고의 결과는 다음과 같다. 1 void main (int c){ 2 int x; 3 c = c? 1 : 8 * sizeof (int); 4 x = 1 << c; 5 } shift.c :4: Warning : invalid s h i f t : assert ((c >= 0) && (c < 32)); Floating-point alarms floating-point operation이 무한한 값 또는 NaN의 결과가 될 수 있을 때, 분석기는 이런 가능성들을 제외하고, 만약 이런 가능성들이 제외된다 면 얻어지는 결과를 나타내는 interval 과함께 분석을 진행하는 경고를 발생한다. 다른 어떤 결과처럼 이런 interval은 over-approximated일 것 이다. 어플리케이션이 floating-point 숫자로써 floating-point 숫자를 나타내지 않는 값으로 사용할 때 경고는 발생한다. 이런 상황은 만약 int 필드와 float 필드가 모두 사용되는 union type 또는 int*로부터 float*로의 변환 의 경우에 발생할 수 있다. 발생한 경고는 NaN, 무한, 또는 주소를 나타 내는 floating-point 숫자로써 사용되는 bit sequence의 가능성을 제외한 다. Uninitialized variables and dangling pointers

60 만약 어플리케이션이 아직 초기화되지 않은 지역변수의 값을 읽는 것처 럼 보이거나 만약 변수의 scope의 밖으로 지역변수의 주소가 조작되는 것처럼 보인다면 경고는 발생할 것이다. 두 문제들은 다음 예제에 등장 한다. 수치분석은 5번째(변수 r이 초기화되지 않았음)와 11번째(dangling pointer로 지역변수 t는 사용되었음) 라인에 대하여 경고를 발생한다. 현 재 버전으로써, 메시지들은 ACSL속성들로써 아직 표현되지 않는다. 1 int *f( i n t c) 2 { 3 int r, t; 4 if (c) r = 2; 5 t = r + 3; 6 return &t; 7 } 8 9 int main (int c) 10 { 11 return *(f(c)); 12 } Invalid memory accesses 수치분석이 dereferenced pointer가 유효하다는 것을 만들지 못할 때마 다, 이것은 이 지점에서 pointer가 유효해져야할 필요가 있다는 것을 표 현하는 경고를 발생한다. 1 int i, t [10]; 2 void main ()