정형 기법을 이용한 하드웨어 AES 모듈 백도어 탐색 연구Study of Hardware AES Module Backdoor Detection through Formal Method
- Other Titles
- Study of Hardware AES Module Backdoor Detection through Formal Method
- Authors
- 박재현; 김승주
- Issue Date
- 2019
- Publisher
- 한국정보보호학회
- Keywords
- hardware backdoor; formal method; model checker
- Citation
- 정보보호학회논문지, v.29, no.4, pp.739 - 751
- Indexed
- KCI
- Journal Title
- 정보보호학회논문지
- Volume
- 29
- Number
- 4
- Start Page
- 739
- End Page
- 751
- URI
- https://scholar.korea.ac.kr/handle/2021.sw.korea/70153
- DOI
- 10.13089/JKIISC.2019.29.4.739
- ISSN
- 1598-3986
- Abstract
- 임베디드 기기의 보안성이 주요한 문제로 부상하고 있다. 관련된 문제 중 특히 공급망 공격은 국가 간의 분쟁으로이어질 수 있어 심각한 문제로 대두되고 있다. 공급망 공격을 완화하기 위하여 하드웨어 구성요소, 특히 AES와 같은암호 모듈에 대한 CC(Common Criteria) EAL(Evaluation Assurance Level) 5 이상 고등급 보안성 인증 및평가가 필요하다. 고등급 보안성 인증 및 평가를 위하여 암호 모듈에 대한 은닉 채널, 즉 백도어를 탐지하는 것이 필요하다. 그러나 기존의 연구로는 암호 모듈 그 중 AES의 비밀 키를 복구시킬 수 있는 정보가 유출되는 백도어를 탐지하지 못하는 한계가 있다.
따라서 본 논문은 기존의 하드웨어 AES 모듈 백도어의 정의를 확장하여 개선시킨 새로운 정의를 제안하고자 한다. 또한, 이 정의를 이용하여 기존 연구가 탐지하지 못했던 백도어를 탐색하는 과정을 제시한다. 이 탐색 과정은Verilog HDL (Hardware Description Language)로 표현된 AES 모듈을 정형 기법 도구인 모델 체커(ModelChecker) NuSMV를 이용하여 검증하는 것으로 백도어를 탐색한다.
- Files in This Item
- There are no files associated with this item.
- Appears in
Collections - School of Cyber Security > Department of Information Security > 1. Journal Articles
Items in ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.