정형 기법을 이용한 하드웨어 AES 모듈 백도어 탐색 연구
Study of Hardware AES Module Backdoor Detection through Formal Method
0
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
임베디드 기기의 보안성이 주요한 문제로 부상하고 있다. 관련된 문제 중 특히 공급망 공격은 국가 간의 분쟁으로이어질 수 있어 심각한 문제로 대두되고 있다. 공급망 공격을 완화하기 위하여 하드웨어 구성요소, 특히 AES와 같은암호 모듈에 대한 CC(Common Criteria) EAL(Evaluation Assurance Level) 5 이상 고등급 보안성 인증 및평가가 필요하다. 고등급 보안성 인증 및 평가를 위하여 암호 모듈에 대한 은닉 채널, 즉 백도어를 탐지하는 것이 필요하다. 그러나 기존의 연구로는 암호 모듈 그 중 AES의 비밀 키를 복구시킬 수 있는 정보가 유출되는 백도어를 탐지하지 못하는 한계가 있다. 따라서 본 논문은 기존의 하드웨어 AES 모듈 백도어의 정의를 확장하여 개선시킨 새로운 정의를 제안하고자 한다. 또한, 이 정의를 이용하여 기존 연구가 탐지하지 못했던 백도어를 탐색하는 과정을 제시한다. 이 탐색 과정은Verilog HDL (Hardware Description Language)로 표현된 AES 모듈을 정형 기법 도구인 모델 체커(ModelChecker) NuSMV를 이용하여 검증하는 것으로 백도어를 탐색한다.
Abstract
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.
참고문헌 (34)
- "The Top 10 IoT Segments in 2018 – based on 1,600 real IoT projects" (2018)[URL]
- Iris Heckmannm, "A Critical review on supply chain risk – Definition, measure and modeling", Omega, 52 (2015)
- "Se rect Back Door in Some U.S. Phones Sent Data to China, Analyst Say" (2016)[URL]
- "Huawei cyber security evaluation centre oversight board: annual report 2019" (2019)[URL]
- "The Big Hack: How China Used a Tiny Chip to Infiltrate U.S. Companies" (2018)[URL]
- "Internet Security Threat R eport (ISTR) 2019" (2019)[URL]
- Common Criteria, "Common Criteria for Information Technology Security Evaluation Part 3 : Security assurance components Version 3.1 Revision 5", ~ (2017)
- Yin Zhang, "Detecting Backdoor", USENIX Security Symposium (2000)
- Felix Schuster, "Towards Reducing the Attack Surface of Software Backdoors", 2013 ACM SIGSAC conference on Computer &communications security, pp.851~862 (2013)
- Yan Shoshitaishvili, "Firmalice -Automatic Detection of Authentication Bypass Vulnerabilities in Binary Firmware", NDSS (2015)
- Ryan Williams, "Backdoor to typical case complexity", IJCAI(International Joint Conference on Artificial Intelligence), 3, pp.1173~1178 (2003)
- Sam Thomas, "Backdoors: Definition, Deniability and Detection", International Symposium on Research in Attacks, Intrusions and Defenses, pp.92~103 (2018), Springer
- Mohammad Tehranipoor, "A Survey of Hardware Trojan Taxonomy and Detection", IEEE Design & Test of Computers, 27, pp.10~25 (2010), IEEE
- He Li, "A survey of hardware Trojan threat and defense", Integration the VLSI journal, 55, pp.426~437 (2016), ELSEVIER
- Nisha Jacob, "Hardware Trojans : current challenges and approaches", IET Computers & Digital Techniques, 8, pp.264~273 (2014), IET
- Julien Francq, "Introduction to hardware Trojan detection methods", 2015 Design, Automation & Test in Europe Conference & Exhibition(DATE), pp.770~775 (2015), EDA Consortium
- Adam Waksman, "FANCI:Identification of Stealthy Malicious Logic Using Boolean Functional Analysis", 2013 ACM SISGSAC conference on Computer &communications security, pp.697~708 (2013)
- Jie Zhang, "VeriTrust : Verification for Hardware Trust", IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems, 34, pp.1148~1161 (2015), IEEE
- Xuehui Zhang, "Case Study: Detecting Hardware Trojans in Third-Party Digital IP Cores", 2011 IEEE International Symposium on Hardware-Oriented Security and Trust(HOST), pp.67~70 (2011), IEEE
- Michael Rathmair, "Applied Formal Methods for Hardware Trojan Detection", 2014 IEEE International Symposium on Circuits and Systems(ISCAS), pp.169~172 (2014), IEEE
- Adib Nahiyan, "Hardware Trojan Detection through Information Flow Security Verification", 2017IEEE Internatioanl Test Conference (ITC), pp.1~10 (2017), IEEE
- Mainak Banga, "Trusted RTL: Trojan Detection Methodology in Pre-Silicon Designs", 2010 IEEE International Symposium on Hardware-Oriented Security and Trust(HOST), pp.56~59 (2010), IEEE
- Xiaolong Guo, "Automatic RTL-to-formal code converter for IP security formal verification", 201617th International Workshop on Microprocessor and SOC Test and Verification (MTV), pp.35~38 (2016), IEEE
- Jeyavijayan Rajendran, "Formal Security Verification of Third Party Intellectual Property Cores for Information Leakage", 2016 29th International Conference on VLSI Design and 2016 15th International Conference on Embedded Systems (VLSID), pp.547~552 (2016), IEEE
- Mathieu Renauld, "Algebraic Side-Attacks on the AES:Why Time alse Matter in DPA", International Workshop on Cryptographic Hardware and Embedded Systems, pp.97~111 (2009), Springer
- Mohamed Saied Emam Mohamed, "Improved Algebraic Side Channel Attack on AES", 2012 IEEE International Symposium on Hardware-Oriented Security and Trust(HOST), pp.146~151 (2012), IEEE
- Niels Ferguson, "Improved Cryptanalysis of Rijindael", International Conference on Information Security and Cryptology, pp.39~49 (2001), Springer
- Eli Biham, "Cryptoanalysis of Reduced Variants of Rijndael", 3rd AES Conference, 230 (2000)
- Huseyin Demirci, "A Meet-in-the-Middle Attack on 8-Round AES", International Workshop on Fast Software Encryption, pp.116~126 (2008), Springer
- Elaine Barker, "Recommendation for key management part 1: General (revision 3)", NIST special publication, 800(57), pp.1~147 (2016)
- "Trojan Benchmarks" (2018)[URL]
- Roberto Cavada, "NuSMV 2.6 User Manual", CMU and ITC-irst, ~ (2015)
- Ahmed Irfan, "Verilog2SMV: a tool for word-level verification", Proceedings of the 2016 Conference on Design, Automation & Test in Europe, pp.1156~1159 (2016), EDA Consortium
- Xiaolong Guo, "Scalable SoC trust verification using integrated theorem proving and model checking", 2016 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp.124~129 (2016), IEEE