정형 기법을 이용한 하드웨어 AES 모듈 백도어 탐색 연구 (Study of Hardware AES Module Backdoor Detection through Formal Method)

서지정보

· 발행기관 : 한국정보보호학회
· 수록지 정보 : 정보보호학회논문지 / 29권 / 4호 / 739 ~ 751페이지
· 저자명 : 박재현, 김승주

초록

임베디드 기기의 보안성이 주요한 문제로 부상하고 있다. 관련된 문제 중 특히 공급망 공격은 국가 간의 분쟁으로이어질 수 있어 심각한 문제로 대두되고 있다. 공급망 공격을 완화하기 위하여 하드웨어 구성요소, 특히 AES와 같은암호 모듈에 대한 CC(Common Criteria) EAL(Evaluation Assurance Level) 5 이상 고등급 보안성 인증 및평가가 필요하다. 고등급 보안성 인증 및 평가를 위하여 암호 모듈에 대한 은닉 채널, 즉 백도어를 탐지하는 것이 필요하다. 그러나 기존의 연구로는 암호 모듈 그 중 AES의 비밀 키를 복구시킬 수 있는 정보가 유출되는 백도어를 탐지하지 못하는 한계가 있다.
따라서 본 논문은 기존의 하드웨어 AES 모듈 백도어의 정의를 확장하여 개선시킨 새로운 정의를 제안하고자 한다. 또한, 이 정의를 이용하여 기존 연구가 탐지하지 못했던 백도어를 탐색하는 과정을 제시한다. 이 탐색 과정은Verilog HDL (Hardware Description Language)로 표현된 AES 모듈을 정형 기법 도구인 모델 체커(ModelChecker) NuSMV를 이용하여 검증하는 것으로 백도어를 탐색한다.

영어초록

Security in embedded devices has become a significant issue. Threats on the sup-ply chain, like using counterfeitcomponents or inserting backdoors intentionally are one of the most significant issues in embedded devices security. Tomitigate these threats, high-level security evaluation and certification more than EAL (Evaluation Assurance Level) 5 on CC(Common Criteria) are necessary on hardware components, especially on the cryptographic module such as AES. High-levelsecurity evaluation and certification require detecting covert channel such as backdoors on the cryptographic module.
However, previous studies have a limitation that they cannot detect some kinds of backdoors which leak the in-formationrecovering a secret key on the cryptographic module.
In this paper, we present an expanded definition of backdoor on hardware AES module and show how to detect thebackdoor which is never detected in Verilog HDL using model checker NuSMV.

참고자료

· 없음