스마트카드운영체제에대한 EAL6 수준의시험서평가제출물개발 2010. 01. 08 고려대학교 심재환
목차 연구개요 연구내용 해외동향조사 시험도구및방법론 연구결과 2
연구개요
과제명 연구개요 스마트카드운영체제에대한 EAL6 수준의시험서평가제출물개발 목표 KCOS 를대상으로시험문서 (ATE 클래스 ) 에대한 EAL6 수준의평가제출물개발 공통평가기준에적합한정형도구를사용한테스트및취약성분석방법개발 KCOS 에대한소스코드수준의테스트및취약성분석에개발된방법론적용 해외 ( 유럽, 미국, 일본 ) 최근고등급사례조사 4
Common Criteria, EALs EAL 7 EAL 6 EAL 5 EAL 4 EAL 3 EAL 2 EAL 1 Formally verified design and tested Semiformally verified design and tested Semiformally designed and tested Methodically designed, tested and checked Methodically tested and checked Structurally tested Functionally tested 5
EAL6 보증컴포넌트 EAL 6 의평가제출물 ATE_COV.3 ATE_DPT.3 ATE_FUN.2 ATE_IND.2 6
시험서평가제출물특징 기능명세내의모든 TSFI 가완전히시험되었음을입증해야함. 모든 TSF 서브시스템이시험되었음을입증해야함. 모든 TSF 모듈이시험되었음을입증해야함. 7
연구내용 해외동향조사 시험도구및방법
해외동향조사
해외평가사례통계분석 2009 년 4 월
제품군별고등급평가통계 IC, 스마트카드등높은점유율을보임.
운영체제분야의인증사례 INTEGRITY-178B Seperation Kernel(EAL6+) 의경우항공분야표준인 DO-178B 획득. MULTOS (ITSEC E6) 는 CC EAL7 에해당하는인증획득. VxWorks RTOS, EAL6+ 평가진행중, VxWork 는이미 IEC61508 과 DO-178B 인증획득. 운영체제제품군은주로고등급평가와다수의인증목표로함. 고등급의운영체제를사용한시스템은인증에유리함. 현재 IEC61508 및 DO-178B 경우고등급인증을위해정적분석기법과정형기법을권고하고있음.
시험방법론 1 단계 : 정적분석 (Frama-C, PolySpace, Rats) - 모듈별로소스코드자체에대한분석 2 단계 : 소스코드기반모델체킹 - TSFI 에해당하는결과를 Assert 를이용해서검증하거나반례를찾아냄. - 반례는테스트케이스로사용될수있음. 3 단계 : 소스코드동적테스팅 - 2 단계의결과를이용해반례가나왔을경우테스트케이스로사용하고, - 검증이성공했을경우, TSFI 에명시된입출력을테스트한다.
시험도구및방법 정적분석 : PolySpace, Frama-C 코드기반모델검증 : CBMC 동적테스팅 취약성분석 : Rats
Frama-C Frama-C C 로작성된소프트웨어의소스코드를분석하기위한도구 C 언어를위한모듈정적분석프레임워크 Frama-C 플러그인을통해분석된 C 코드가실제로무엇을하는지알수있음 Run-Time 시발생할수있는오류들을알려줌 Divide by 0 Array out of bound Invalid pointer access
Frama-C Frama-C 를통해할수있는행위 매실행지점에서프로그램의변수들에대한가능한값들의집합을관측 큰프로그램을간단한모듈로나눌수있음 Frama-C 의특징 Graphical user interface 분석을유용하게하기위한다양한옵션을제공 Annotation을위한 ACSL언어를제공 Annotation을통해원하는속성을검증할수있음
Frama-C : KCOS 사례 기본적으로 syntax 오류가있는코드는 Frama-C 에삽입을할수없음 syntax 오류가있는경우, Frama-C 가어느부분에오류가있다는것을알려줌 검증한코드의결과에오류가있는경우, 메시지를통해오류를알려줌 검증할 KCOS 모듈 : isoupdaterecord.c 검증방법 1. main.c 에있는 isoupdaterecord 모듈에대한 isoupdaterecord.c 파일을만든다. 2. isoupdaterecord 모듈에서사용하고있는함수및전역변수를코드에추가한다. 3. main 함수를만들어 isoupdaterecord 모듈을호출하도록만든다. 4. 위의작업후에 Frama-C 를이용해검증작업을수행한다.
Frama-C 로검증할프로젝트 : KCOS 2/2 검증결과 Type 오류발생 코드에오류가있기때문에위와같은결과를얻음 오류메시지내용 : Symbol Fatal error
PolySpace 의미분석 (Semantics Analysis) 기법사용 컴파일시 Run-time error 검출 별도스크립트작성없음 검출결과를 4 가지색상 (Green, Red, Yellow, Gray) 으로표시 복잡해지고고기능화된임베디드소프트웨어분야에주로사용
PolySpace 특징 런타임에러를컴파일타임에발견 Out-of-Bounds Array Access Read Access ot Non-Initialized Data Illegal pointer access Invalid Arithmetic Operations: Division by Zero, Square Root of a Negative Number Illegal Type Conversion Overflow/Underflow on Integers and Floating Point Number Access Conflict on Shared Data (Multi-Task Application) Unreachable (dead) Code 코딩룰검사 MISRA-C
CBMC 소개 CBMC : ANSI-C Bounded Model Checker ANSI-C 프로그램을검증하기위한도구 Edmund Clarke, Daniel Kroening, and Flavio Lerda : 2004 검증가능속성 array bounds (buffer overflows) pointer safety exceptions user-specified assertions consistency with other languages, such as Verilog 검증결과가성공일경우, 테스트는 100% Coverage 를만족한다. 검증결과가실패일경우는반례를찾아준다.
Requirements Overview of CBMC Formal Requirement Properties in C (ex. assert( x< a[i]); ) C Program (Model) Satisfied Translation to SAT formula CBMC SAT Solver Not Satisfied Okay Counter Example
CBMC 의수행결과 실패의경우 ( 반례 ) 입력변수오버플로우 성공의경우 (100% 커버리지 )
동적테스팅 개발플랫폼을대신해 pc 플랫폼으로소프트웨어포팅 레지스터, EEPROM 등을 pc 의메인메모리영역으로옮기고동작시킴 터미널과스마트카드와의통신은 pc 의표준입출력 ( 키보드, 모니터로대치 ) Visual Studio 의디버거를사용할수있는시험시간은단축
동적테스팅 모니터를통한입출력과디버거를통해 TSFI 의입출력을테스트 출력 : atrstr, Sw1, Sw2
정적분석도구 - RATS RATS (Rough Auditing Tool for Security) Open Source Static Analysis Tool 시큐어소프트웨어社보안엔지니어들에의해개발 분석언어 C, C++, Perl, PHP, Python 언어별소스코드취약성목록내장 (XML Format) 찾아내는오류들의예 특징 Buffer Overflow Format String Attack TOCTOU (Time Of Check, Time Of Use) race condition 경량도구 (300KB 미만 ) 수동코드분석에대한소요시간단축
RATS on KCOS RATS results Severity: Low Issue: memcpy Double check that your buffer is as big as you specify. When using functions that accept a number n of bytes to copy, such as strncpy, be aware that if the dest buffer size = n it may not NULL-terminate the string. File: kcos/application/test.c Lines: 46 50 54 58 75 82 88 96 File: kcos/dedicated_sw/des_acc.c Lines: 16 17 21 22 23 24 25 26 30 31 32 33 34 35 44 45 83 84 File: kcos/dedicated_sw/eeprom.c Lines: 21 File: kcos/operating_system/carddata.c Lines: 31 36 41 46 51 56 61 66 71 76 File: kcos/operating_system/create_file.c Lines: 28 29 30 39 44 50 51 57 129 130 File: kcos/operating_system/create_session.c Lines: 46 59 78 File: kcos/operating_system/des.c Lines: 40 51 73 89 92 File: kcos/operating_system/ext_auth.c Lines: 30 71 84 File: kcos/operating_system/file.c Lines: 73 79 File: kcos/operating_system/getlifecycle.c Lines: 8 File: kcos/operating_system/main.c Lines: 267 File: kcos/operating_system/readrecord.c Lines: 49 File: kcos/operating_system/securemessaging.c Lines: 17 26 31 46 54 File: kcos/operating_system/trm.c Lines: 99 101 106 113 121 122 144 164 Inputs detected at the following points Total lines analyzed: 2428 Total time 0.000000 seconds -2147483648 lines per second
Validation of Findings 분석결과 함수 : memcpy 구조 : void *memcpy(void *dest, const void *src, size_t n); 잠재적위험 : dest 의버퍼사이즈에대한고려가필요 KCOS 내에서사용된 memcpy 들은 dest 의버퍼사이즈를고려하여사용되어모두안전하게사용됨 #define EEPROM_PAGE_SIZE 0x80... static u1 backupram[eeprom_page_size];...... memcpy(backupram,pdstpage,eeprom _PAGE_SIZE);... typedef unsigned char u1;... #define LEN_KEY 16... typedef struct KeyTag{ u1 key[16]; u4 chksum; }Key; Key key;... memcpy(key.key,data,len_key);...
연구결과 TOE 의발견된문제점 MISRA-C 분석결과 시험서결과
TOE 의발견된문제점들 (1) Type 오류 bool isallowed(accesscondition ac) 함수 32 비트구조체 PolySpace, Frama-C 등정적도구 에서에러출력 하지만, 잘컴파일되어동작 16bit 정수
잘못된구조체초기화 TOE 의발견된문제점들 (2) 구조체를정수초기화하듯초기화 정적도구에서는에러표시 하지만, 잘컴파일되어동작
TOE 의발견된문제점들 (3) 재귀함수 무한루프에빠짐 다행히호출되지않음 안쓰는함수는지워야함 명령어클래스 현재 0x00과 0x90만존재 If문에서참이되는명령어는존재하지않음 구현이완료되지않은것같음
MISRA-C 분석결과 모듈이름 Warning 수 isogetresponse 33 isoreadrecord 105 isoupdaterecord 223 isogetdata 38 isoputdata 144 isoselectfile 18 isogetchallenge 25 isoextauth 320 problockfile 177 prounblockfile 194 proputkey 231 isoverify 226 prosetlifecycle 192 progetlifecycle 32 procreatefile 364 procreatesession 394 총합 2716
시험서결과 모듈별로정적분석한결과 시험항목별로소스검증과동적시험결과