[논문]정형 기법을 이용한 하드웨어 AES 모듈 백도어 탐색 연구

박재현; 김승주

doi:10.13089/jkiisc.2019.29.4.739

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

情報保護學會論文誌 = Journal of the Korea Institute of Information Security and Cryptology, v.29 no.4, 2019년, pp.739 - 751

박재현 (고려대학교 정보보호대학원) , 김승주 (고려대학교 정보보호대학원)

초록
AI-Helper

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

Abstract ▼ AI-Helper

Security in embedded devices has become a significant issue. Threats on the sup-ply chain, like using counterfeit components or inserting backdoors intentionally are one of the most significant issues in embedded devices security. To mitigate 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-level security 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-formation recovering 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 the backdoor which is never detected in Verilog HDL using model checker NuSMV.

주제어

표/그림 (13)

그림 Fig. 1. The Top 10 IoT Segments in 2018
그림 Fig. 2. Structure of Hardware Backdoor
표 Table 1. Definitions of Hardware Backdoor
표 Table 2. Hardware Backdoor Definition in [24]
표 Table 3. Informations of AES
그림 Fig. 3. AES Module Backdoor Detection Process
표 Table 4. Comparison the definitions of Existing Studies with the definitions of this paper
그림 Fig. 4. Part of AES Module Verilog HDL Code
그림 Fig. 5. Part of AES Module SMV Format
그림 Fig. 6. Result of Verification through Fig 5. Code
표 Table 5. Specification in SMV Format for Definitions to detect backdoor
표 Table 6. Result of Detecting Backdoor
그림 Fig. 7. Result of Verification to check module variables

AI 본문요약
AI-Helper

* AI 자동 식별 결과로 적합하지 않은 문장이 있을 수 있으니, 이용에 유의하시기 바랍니다.

문제 정의

는 기존에 하드웨어 AES 모듈 백도어에 대한 정의와 본 논문에서 정의하는 백도어에 대한 비교표이다. 기존의 연구는 AES 비밀 키 유출에 대 해서만 백도어 탐색을 하였으나 본 논문은 유출 대상 정보의 범위를 확대하고 정형 기법을 활용하기 위해 정의하였다. 본 논문에서 탐색하고자 하는 백도어는 AES 비밀 키의 보안강도를 저하시켜 공격자가 비밀 키를 복구 가능하도록 유도하는 정보를 유출시킨다.
기존의 AES 모듈의 백도어는 비밀 키의 유출만을 백도어로 취급하였으나, AES에 대한 알고리즘 취약점, 부채널 공격 등으로 Round를 연산한 결과를 통해서 비밀 키 추출 및 AES에 영향을 줄 수 있다. 따라서 본 논문에서는 비밀 키 외의 다른 정보에 대한 백도어를 정의하고 해당 특성을 모델 체커에서 활용하기 위한 Property로 명세하였다. 이를 통해 기존의 AES 백도어 연구에서 확인하지 못한 백도어를 모델 체커를 통한 정형 기법으로 탐색 가능하다.
따라서 본 논문은 백도어를 탐지하기 위하여 제시 된 기존의 하드웨어 AES 모듈 백도어의 확장된 정 의를 제안한다. 이 확장된 정의를 이용하여 AES 비밀 키 외에 암호화 과정에서 생성되는 중간 결과 값이 유출되는 백도어를 탐색하는 과정을 제시한다.
해당 정보가 유출되는 경우, 비밀 키를 복구하거나 암호화에 영향을 끼칠 수 있으나 기존 연구는 키 이외의 값의 유출은 검증하지 않았다. 따라서 본 논문은 비밀 키 외에 AES 암호화 과정에 영향을 끼칠 수 있는 정보를 식별 및 정의하여 해당 정보가 유출되는 백도어를 탐색하는 연구를 진행하고자 한다.
하드웨어 AES 모듈의 백도어를 통하여 유출될 수 있는 내부 정보를 비밀 키 외에도 존재한다. 본 논문에서 하드웨어 AES 백도어의 탐색을 위해 유출 되는 정보의 특성을 고려한다. 기존의 백도어 탐색 연구는 Payload가 비밀 키의 일부 혹은 전체 값이 유출되는 경우로 한정하였다.
본 논문은 하드웨어 AES 모듈에 대해 정형검증을 통하여 백도어의 유무를 탐색하는 연구를 진행하였다.
본 연구는 이러한 정의들을 통하여 하드웨어 AES 모듈의 백도어를 모델 체커로 탐색하는 연구를 진행하였다.
상기 검증 과정의 확장으로 NuSMV의 기능을 이용하여 백도어가 발생하였을 시 AES 모듈의 구동을 확인할 수 있다. 원리는 NuSMV가 수식을 검증하는 과정에 서 반례가 존재하는 경우, 반례에 대한 변수 값들을 도출해주는 기능을 응용하는 것이다.
[24]의 연구는 최종적으로 AES의 비밀 키가 1-bit 이상 유출되는 경우와 AES의 비밀 키의 역 이 1-bit 이상 유출되는 경우에 대하여 백도어로 판단하였다. 이 정의를 모델 체커에 입력하는 것으로 AES 비밀 키가 유출되는 백도어를 탐색하는 연구를 진행하였다.

가설 설정

하드웨어 AES 모듈의 백도어 탐색을 위한 초기의 연구는 백도어를 활성화시키는 Trigger를 식별 하는 것으로 백도어를 탐색하였다[17], [18], [19]. 해당 연구는 백도어는 전체 입력 값 중 드물게 발생하는 Rare Condition일 때 활성화된다고 가정하고, 이를 탐지하는 연구를 하였다. 하지만 백도어가 아닌 회로에 대한 False Positive가 많이 발생하고, Trigger가 항시 활성화되는 백도어를 탐색하지 못하였다.

제안 방법

본 논문에서는 구현된 AES 모듈 및 백도어를 SMV 포맷으로 변경하고, 백도어의 특징을 검출하기 위한 Property를 수식형태로 명세한다. AES 모듈의 SMV 포맷 파일에 대하여 백도어 Property를 NuSMV로 검증하는 것으로 백도어의 존재 유무를 판단한다.
이 확장된 정의를 이용하여 AES 비밀 키 외에 암호화 과정에서 생성되는 중간 결과 값이 유출되는 백도어를 탐색하는 과정을 제시한다. Verilog HDL로 구현되어 있는 AES 모듈과 확장 된 백도어 정의를 SMV 포맷으로 정형 명세하고 NuSMV에 입력하여 하드웨어 AES 모듈의 백도어를 탐색한다.
의 정보가 유출되는 경우, 백도어를 탐색할 수 있어야 한다. 그러므로 이를 위하여 AES 모듈이 운용 되는 Path 상에서 특정 조건이 만족하는지 여부를 확인할 수 있는 LTL(Linear Tempoal Logic)을 사용하여 백도어의 유무를 탐색한다.
NuSMV를 이용해 AES 모듈의 모델을 생성하는 과정에서 유의할 사항으로 State Explosion이 있다. 모델 체커는 내부 변수의 변경에 따라 발생하는 State가 전환되는 Path나 Computation Tree 형태로 모델을 자동으로 생성하고 특정 Property를 검증한다. 이 과정에서 내부 변수의 경우의 수나 변수의 개수가 많을 경우, State의 수가 증가하여 모델 생성이 불가능할 수 있다.
기존의 연구는 AES 비밀 키 유출에 대 해서만 백도어 탐색을 하였으나 본 논문은 유출 대상 정보의 범위를 확대하고 정형 기법을 활용하기 위해 정의하였다. 본 논문에서 탐색하고자 하는 백도어는 AES 비밀 키의 보안강도를 저하시켜 공격자가 비밀 키를 복구 가능하도록 유도하는 정보를 유출시킨다. 이 보안강도의 기준은 NIST의 112-bit 이하로, 유출되는 데이터의 양은 16-bit 이상으로 정의된다.
따라서 NuSMV는 State가 전환되는 Transition 횟수를 제한한 BMC(Bounded Model Check) 기능을 지원하여 State Explosion을 해결한다. 본 논문에서는 Bound 범위를 5회 이하로 제한하여 검증을 실시하였다.
본 논문에서는 구현된 AES 모듈 및 백도어를 SMV 포맷으로 변경하고, 백도어의 특징을 검출하기 위한 Property를 수식형태로 명세한다. AES 모듈의 SMV 포맷 파일에 대하여 백도어 Property를 NuSMV로 검증하는 것으로 백도어의 존재 유무를 판단한다.
Table 3. 수식의 부정형을 입력하여 검증을 실시한다. 이는 해당 모듈은 백도어가 절대로 발생하지 않는다는 의미로 검증을 실시하는 것으로, 반례가 발생하는 것은 백도어가 존재한다는 의미와 같다.
따라서 본 논문은 백도어를 탐지하기 위하여 제시 된 기존의 하드웨어 AES 모듈 백도어의 확장된 정 의를 제안한다. 이 확장된 정의를 이용하여 AES 비밀 키 외에 암호화 과정에서 생성되는 중간 결과 값이 유출되는 백도어를 탐색하는 과정을 제시한다. Verilog HDL로 구현되어 있는 AES 모듈과 확장 된 백도어 정의를 SMV 포맷으로 정형 명세하고 NuSMV에 입력하여 하드웨어 AES 모듈의 백도어를 탐색한다.
정리하자면 본 논문에서 ‘백도어를 통한 정보 유출’로 간주할 수 있는 속성은 비밀 키의 보안강도를 NIST 권고인 112-bit 이하로 저하시킬 수 있는 정보의 유출과 유출 대상 정보를 역연산한 결과가 일부 유출되어도 ‘백도어를 통한 정보 유출’로 간주하였다.
He Li 외 2명이 2016년에 발표한 논문에서 하드웨어 백도어는 특정 입력 값을 받았을 때 활성화되는 매커니즘 부분을 Trigger로, Trigger로 인하여 구동되거나 출력되는 결과를 Payload라고 명명하였다. 제안한 구조를 통하여 하드웨어 백도어를 탐지하고 방지하는 방법에 대하여 자체적인 프로세스를 제안하였다[14].
Mohammad Tehranipoor 외 1명이 2011년 발표한 논문에서는 하드웨어 백도어를 물리적 특성, 활성화 방법에 대한 특성, 백도어의 기능에 대한 특성의 세 가지 기준으로 분류하였다[13]. 탐색 방법에 대하여 부채널 분석이나 Fuzzer와 같이 무작위 입력 값을 통해 백도어를 활성화시키는 방법에 대하여 서술하였다.
2018년 Sam Thomas 외 1명은 백도어에 관련하여 정의, 부정 가능성(Deniability)과 탐지에 대해 조사한 논문을 발표하였다[12]. 해당 논문에서는 기존에 백도어와 관련된 연구를 종합하면서 구성요소와 특성을 반영하여 백도어의 정의를 내렸다.
해당 논문은 백도어를 컴퓨터 시스템에 인가되지 않은 접근을 실시하기 위하여 시스템 내부에 몰래(“surreptitiously”) 삽입된 매커니즘으로 정의하였다.
하드웨어 AES 모듈 백도어를 정형 기법으로 탐색하기 위한 대표적인 연구로 Jeyavijayan Rajendran 외 3명은 공급망 공격에 대응하기 위해 SoC(System-on-Chip)의 설계를 정형 기법 도구를 이용하여 검증하고 하드웨어 백도어를 탐색하는 연구를 실시하였다[24]. 해당 연구는 백도어 탐색을 위해 모델 체커를 사용하였고, 이를 활용하기 위하여 백도어에 대한 정의를 재실시하였다.
[27], [28], [29]는 AES에 대한 공격 기법인 Square 공격, Impossible Differentials, Meet-in-the-Middle 공격을 통하여 비밀 키를 복구하는 연구를 실시하였다. 해당 연구들의 공통점은 특정 라운드 이하의 중간 연산 과정에서 각 라운드의 중간 입력 값, 중간 출력 값 그리고 라운드 키를 이용하여 비밀 키를 복구하는 공격을 실시하였다. [27]의 연구는 5라운드 이하의 값이 필요했으나, [29]의 연구에서는 8라운드의 중간 값을 통하여도 비밀 키를 복구한 결과를 제시하였다.
해당 공격은 AES 암호화 연산, 특히 SubByte 연산과 MixColumn 연산 간에 발생하는 전력 소모량을 측정하고, 측정값들을 AES 논리식에 대입하여 비밀 키를 도출하는 방법이다. 해당 연구에서는 각 연산의 중간 결과 값을 부채널 공격을 통하여 획득하였다. 하지만 중간 결과 값을 출력하는 백도어가 있는 경우, [25], [26]의 공격을 통하여 AES 비밀 키를 복구하는 것이 가능하다.

대상 데이터

하드웨어 암호 모듈 검증 연구 중 하드웨어 AES 모듈에 대한 백도어 탐색 연구는 현재까지 지속적으로 진행되었다. 기존 하드웨어 AES 모듈 백도어 탐색의 연구는 AES 비밀 키 유출에 한정되어 실시되었다. 그러나 AES 비밀 키 외에 암호화 과정에서 발생하는 중간 값을 통하여 공격자가 비밀 키를 복구 할 수 있다[27],[28].
본 논문에서 지정한 유출 대상 정보들은 다양한 공격 기법을 통하여 비밀 키를 복구할 수 있는 정보이다. 예를 들어 유출 대상 정보가 16-bit 이상 노출되는 경우, AES 비밀 키를 16-bit 이상 복구할 수 있다.
분석 대상인 백도어가 포함된 AES 모듈은 Verilog HDL로 구현되었으며, 3.1장에서 식별한 탐색 대상 정보를 유출시키는 백도어는 Trust Hub[31]와 같은 저명한 단체에서 제공하는 벤치마 크가 존재하지 않아 별도로 구현하였다.

이론/모형

검증을 위한 모델 체커는 NuSMV[32]를 사용하였다. NuSMV는 카네기 멜론 대학을 포함한 4개 대학 및 기업에서 개발한 오픈 소스 모델 체커이다.
국제공통평가기준은 개발 환경에서 해당 제품이 안전하게 개발되었는가를 평가하고 인증하기 위하여 활용되는 국제표준이다. 평가대상(Target Of Evaluation, TOE)의 신뢰도를 인증하기 위하여 평가자는 국제공통평가기준의 평가보증등급(Evaluation Assurance Level, EAL)을 활용하여 수준별 보안성을 보증한다[7].

성능/효과

본 논문은 하드웨어 AES 모듈에 대해 정형검증을 통하여 백도어의 유무를 탐색하는 연구를 진행하였다. 기존의 AES 모듈의 백도어는 비밀 키의 유출만을 백도어로 취급하였으나, AES에 대한 알고리즘 취약점, 부채널 공격 등으로 Round를 연산한 결과를 통해서 비밀 키 추출 및 AES에 영향을 줄 수 있다. 따라서 본 논문에서는 비밀 키 외의 다른 정보에 대한 백도어를 정의하고 해당 특성을 모델 체커에서 활용하기 위한 Property로 명세하였다.
유출 대상 정보가 일부 유출되는 경우, 해당 과정을 반복하여 AES 비밀 키를 도출하거나 AES 보안강도를 저하시켜 전수조사 등으로 비밀 키를 도출할 수 있도록 유도하는 것이 가능하다. 따라서 본 논문에서는 유출 대상 정보의 전체가 유출되는 경우 외에 일부, 16-bit 이상이 유출되는 경우도 포함하여 백도어로 유출 가능하다고 판단하였다.
따라서 본 논문에서는 비밀 키 외의 다른 정보에 대한 백도어를 정의하고 해당 특성을 모델 체커에서 활용하기 위한 Property로 명세하였다. 이를 통해 기존의 AES 백도어 연구에서 확인하지 못한 백도어를 모델 체커를 통한 정형 기법으로 탐색 가능하다.

후속연구

두 번째로 모델 체커의 근본적인 한계로 인해 복잡한 수식이나 함수에 대해서는 검증이 제한된다. 또한, 하드웨어가 구현된 Verilog HDL 코드를 SMV 포맷으로 변경할 때, 지원하는 도구[33]의 미비함으로 일치성 검증의 문제가 발생할 수 있다.
본 연구의 한계로 첫째 탐지하고자 하는 백도어의 다양성이 부족한 것이다. 서술하였듯이 해당 유형의 백도어는 현재 저명한 단체에서 제공하고 있지 않아서 적절한 벤치마크로서 실험여부를 명백히 증명하기가 제한된다.
본 연구의 한계로 첫째 탐지하고자 하는 백도어의 다양성이 부족한 것이다. 서술하였듯이 해당 유형의 백도어는 현재 저명한 단체에서 제공하고 있지 않아서 적절한 벤치마크로서 실험여부를 명백히 증명하기가 제한된다. 차후 연구로 해당 유형의 백도어를 다양한 방법으로 구현하고 이를 검증하는 과정이 추가적으로 필요하다.
[34]는 Theorem Prover와 모델 체커를 병행하여 사용하는 프로세스를 제안하여 상호 도구 간의 문제를 개선하고자 하였다. 이와 같이 향후 연구는 모델 체커와 Theorem Prover를 결합하는 것으로 하드웨어 모듈에 대한 정형 검증 방법론을 개선하는 것과 실제 Verilog HDL 구현체와 SMV 포맷 간의 일치성 검증에 대한 연구가 남아있다.
서술하였듯이 해당 유형의 백도어는 현재 저명한 단체에서 제공하고 있지 않아서 적절한 벤치마크로서 실험여부를 명백히 증명하기가 제한된다. 차후 연구로 해당 유형의 백도어를 다양한 방법으로 구현하고 이를 검증하는 과정이 추가적으로 필요하다.

LOADING...

표제어: PCR

동의어: Packet Collision Rate

용어 설명 출처 목록 (6)

용어 설명: PCR은 세균 특이성이 있는 primer를 이용하여 적은 수의 세균이 있을지라도 쉽게 검출할 수 있는 유용한 방법이며, 이를 이용하여 구강 내 치면세균막이나 타액에서 직접 세균을 검출할 수 있게 되었다[8].

내보내기 구분	파일저장 인쇄 메일전송
구성항목	기본정보 상세정보 관리번호, 논문명, 저널/프로시딩명, 저자 , 발행년, 권, 호, 시작페이지, 끝페이지, 발행기관 관리번호, 논문명, 대등논문명, 저자 , 저널/프로시딩명, 발행기관, 발행년, 발행언어, 권, 호, 시작페이지, 끝페이지, ISBN, ISSN, 주제분야, 키워드, 초록(한글), 초록(영문), 저자(소속기관)
저장형식	Text(ASCII format) Excel format RefWorks Direct Export RIS format (for Reference Manager, ProCite, EndNote), Scholar's Aids, Mendeley
메일정보	받는사람 (필수) @ 보내는사람 (선택) @ 제목 내용 KISTI 검색결과 이메일 서비스
안내	총 건의 자료가 검색되었습니다. 다운받으실 자료의 인덱스를 입력하세요. (1-10,000) 검색결과의 순서대로 최대 10,000건 까지 다운로드가 가능합니다. 데이타가 많을 경우 속도가 느려질 수 있습니다.(최대 2~3분 소요) 다운로드 파일은 UTF-8 형태로 저장됩니다. 파일의 내용이 제대로 보이지 않을실 때는 웹브라우저 상단의 보기 -> 인코딩 -> 자동선택 여부를 확인하십시오. ~ Text(ASCII format) Excel format

연합인증