💬 NLP

Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis

이 논문은 기존 방식들이 실패하는 공개 데이터셋에서 적응형 트리거에 대한 강건성과 완벽에 가까운 탐지율을 달성하며, 숨겨진 기능 블록 로직을 노출하고 트리거를 합성함으로써 IEC 61131-3 PLC 프로그램 내의 래더 로직 밤(Ladder Logic Bombs)을 탐지하도록 ESBMC-PLC+를 확장한 정형 검증 프레임워크인 ESBMC-LLB를 제시한다.

원저자: Pierre Dantas, Lucas Cordeiro, Waldir Junior

게시일 2026-07-10

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Pierre Dantas, Lucas Cordeiro, Waldir Junior

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

PLC(프로그래밍 가능 로직 컨트롤러)를 공장의 두뇌라고 상상해 보십시오. 이 두뇌는 센서를 관찰하고, 결정을 내리고, 기계를 움직인 다음, 다시 아주 짧은 순간 안에 이 과정을 반복하는 루프를 끊임없이 실행합니다. 이제, 이 두뇌 안에 몰래 숨어든 '로직 폭탄(logic bomb)'을 가진 교활한 해커를 상상해 보십시오. 이 폭탄은 마치 잠자는 용과 같습니다. 공장이 정상적으로 작동하는 동안에는 아무 일도 하지 않지만, 특정하고 숨겨진 조건(예: 카운터가 특정 숫자에 도인 경우)이 충족되는 순간 깨어나서 혼란을 야기합니다. 기계를 멈추게 하거나, 센서 수치를 속이거나, 닫혀 있어야 할 밸브를 열게 만드는 식입니다.

오랫동안 이 공장 두뇌를 점검하는 도구들은 사각지대를 가지고 있었습니다. 이 도구들은 메인 코드는 확인했지만, '함수 블록(function blocks)'—즉, 메인 코드 내부의 작은 서브루틴이나 미니 프로그램들—은 무시했습니다. 이 논문은 그 '잠자는 용(폭탄)'들이 바로 무시되었던 이 함수 블록 안에 숨어 있었다고 설명합니다. 기존 도구들이 이 블록들을 시야에서 놓쳤기 때문에, 악성 코드와 안전한 코드가 검사기에게는 완전히 동일하게 보였던 것입니다. 이는 마치 군중 속에서 스파이를 찾으려 할 때, 사람들의 얼굴만 보고, 정작 스파이가 숨어 있는 코트는 쳐다보지도 않는 것과 같았습니다.

거대한 해결책: 코트를 열다
저자들인 피에르 단타스(Pierre Dantas), 루카스 코르데이로(Lucas Cordeiro), 발디르 주니어(Waldir Junior)는 ESBMC-LLB라는 새로운 방법을 구축했습니다. 그들의 핵심 전략은 간단하지만 강력했습니다. 바로 검사기가 함수 블록 내부를 들여다보게 만든 것입니다. 그들은 숨겨진 코드 내부를 펼쳐서 검사기가 볼 수 있도록 만드는 '번역 레이어(translation layer)'를 추가했습니다.

코드가 눈에 보이게 되면, 그들은 두 가지 영리한 트릭으로 폭탄을 잡아냅니다:

스톱워치 (Scan-Watchdog): 만약 폭탄이 프로그램이 무한 루프에 빠지게 만들어 기계를 멈추려 한다면, 검사기는 스톱워치를 든 엄격한 심판 역할을 합니다. 검사기는 "이 작업을 완료하는 데 100단계의 여유를 주겠다. 만약 이를 초과하면 탈락이다!"라고 말합니다. 만약 폭탄이 영원히 루프를 돌려고 하면, 검사기는 즉시 이를 잡아냅니다.
배선 테스터 (Output Wiring): 만약 폭탄이 센서에 대해 거짓말을 하거나 기계를 강제로 움직이려 한다면, 검사기는 숨겨진 코드와 메인 시스템 사이의 전선을 연결합니다. 만약 숨겨진 코드가 '거짓'(예: 밸브가 열리면 안 되는데 열라고 명령하는 것)을 보내려 하면, 검사기는 이것이 안전 규칙을 위반하는 것을 포착합니다.

마법 같은 결과: "비밀 코드"를 찾아내다
여기 가장 멋진 부분이 있습니다. 검사기가 폭탄을 발견했을 때, 단순히 "에러!"라고만 말하는 것이 아닙니다. 검사기는 실제로 정확한 **트리거(trigger)**를 출력합니다. 이는 마치 검사기가 "용을 찾았습니다. 그리고 여기 그 용을 깨우는 비밀번호가 있습니다: '카운터가 12에 도달하면'"이라고 말하는 것과 같습니다. 이것을 "트리거 합성(trigger synthesis)"이라고 부릅니다.

얼마나 잘 작동했는가?
연구팀은 이 방법을 여러 데이터 세트에 테스트했으며, 결과는 인상적이었지만 몇 가지 중요한 한계도 있었습니다:

공개 테스트: 60개의 프로그램(안전한 프로그램 30개, 폭탄이 포함된 프로그램 30개)으로 구성된 유명한 데이터셋에서, 그들의 방법은 30개의 폭탄을 모두 찾아냈습니다. 모든 폭탄을 잡아냈고 각각의 비밀 트리거를 찾아냈습니다. 또한 29개의 안전한 프로그램이 정말로 안전하다는 것을 증명했습니다. 한 개의 안전한 프로그램은 너무 복잡하여 검사기가 100% 확신할 수 없었지만(안전하다고 하는 대신 "모름"이라고 답함), 해당 프로그램을 잘못 몰아세우지는 않았습니다.
"스마트한" 해커 테스트: 그들은 수학 퍼즐(단순한 숫자 대신 복잡한 계산을 사용하는 방식) 속에 트리거를 숨겨 시스템을 속이려 시도했습니다. 패턴만을 찾는 기존 도구들은 이러한 속임수를 놓쳤습니다. 그러나 ESBMC-LLB는 수학의 의미를 이해하여 이러한 까다로운 버전의 폭탄 5개를 모두 잡아냈습니다.
대규모 테스트: 속도를 테스트하기 위해 310개의 프로그램(안전 155개, 폭탄 155개)을 생성했습니다. 시스템은 평균 70밀리초(눈 깜빡임보다 빠른 속도!) 안에 폭탄의 **100%**를 잡아냈습니다.
실제 정수 처리장 테스트: 이들은 실제 정수 처리장 시뮬레이션(SWaT 코퍼스)에 이 방법을 테스트했습니다.
- 단순한 수학 트리거가 포함된 이전 버전의 데이터에서는, 오보(false alarm) 없이 150개 중 149개의 폭탄(99%)을 찾아냈습니다.
- 한계점: 매우 복잡한 비선형 수학(예: 숫자를 반복해서 제곱하는 방식)이 포함된 최신 버전을 테스트했을 때, 시스템은 막혔습니다. 수학이 너무 어려워 검사기가 제시간에 풀 수 없었고, 탐지율은 **49%**로 떨어졌습니다. 논문은 이 부분을 매우 명확하게 밝히고 있습니다. 그들의 방법은 표준적인 로직과 단순한 수학에는 훌륭하지만, 복잡한 비선형 수학의 벽에 부딪힙니다. 그런 특정 경우에는 다른 종류의 도구(CFG-triage 탐지기)가 여전히 더 낫습니다.

그들이 주장하지 않는 것
저자들은 자신들의 도구가 할 수 없는 것에 대해 매우 솔직합니다. 만약 폭탄이 (무한 루프를 돌지 않고) 빠르게 임무를 완수하도록 설계되었고, 검사기가 찾아보라고 지시한 특정 안전 규칙을 위반하지 않는다면, 도구가 이를 놓칠 수도 있다고 명시적으로 밝히고 있습니다. 이것은 가능한 모든 나쁜 것을 찾아내는 마법 지팡이가 아닙니다. 시스템을 멈추거나 정의된 안전 규칙을 깨뜨리는 것을 찾아내는 도구입니다.

결론
이 논문은 함수 블록 내부를 들여다보기 위해 "코트를 열고", 코드의 의미를 이해하는 스마트한 검사기를 사용함으로써, 예전에는 눈앞에 두고도 놓쳤던 교활한 산업용 폭탄을 잡을 수 있음을 보여줍니다. 이 도구는 폭탄을 찾아내고, 그것을 어떻게 트리거하는지 정확히 알려주며(따라서 이를 차단할 수 있음), 수학이 너무 복잡해지지 않는 한 나머지 시스템이 안전하다는 것을 증명합니다. 저자들은 이 도구를 기존의 모든 것을 대체하는 것이 아니라, 기존 방식과 함께 작동하는 강력한 새로운 도구로서 제시하고 있습니다.

기술 요약: ESBMC-PLC+를 이용한 IEC 61131-3 PLC 프로그램 내 래더 로직 폭탄(Ladder Logic Bomb) 탐지

1. 문제 정의

프로그래머블 로직 컨트롤러(PLC)는 안전이 필수적인 산업 제어 시스템(ICS)의 중추 역할을 합니다. 특정 위협인 **래더 로직 폭：(Ladder Logic Bomb, LLB)**은 정상 작동 및 시운전 단계에서는 잠복해 있다가, 특정 트리거(trigger) 조건이 충족될 때 활성화되어 액추에이터를 조작하거나, 센서 판독값을 위조하거나, 운영자의 제어를 차단(예: 비종료 현상)하는 악성 제어 로직을 삽착하는 것을 의미합니다.

기존의 탐지 방법들은 두 가지 주요 한계점에 직면해 있습니다:

구조적 맹점(Structural Blindness): 많은 LLB는 함수 블록(Function Block, FB) 내부의 본체(body) 안에 숨겨집니다. 표준 래더 다이어그램(LD) 검증기들은 검증을 단순화하기 위해 FB 본체를 중간 표현(Intermediate Representation, IR)에서 누락시키는 경우가 많으며, 이로 인해 악성 로직이 검증기에게 보이지 않게 됩니다.
유계되지 않은 보증의 결여(Lack of Unbounded Guarantees): 시그니처 기반 또는 제어 흐름 그래프(CFG) 분류 탐지기는 구문적 패턴에 의존합니다. 이들은 적응형 트리거(예: 계산된 값, 모호한 산술 연산)에 의해 회피될 수 있으며, 모든 스캔 사이클에 걸쳐 폭탄의 부재를 공식적으로 증명할 수 없습니다.

2. 방법론: ESBMC-LLB

저자들은 기존의 ESBMC-PLC+(SMT 비트 벡터와 $k$ -유도법을 사용하는 IEC 61131-3 모델 체커) 검증기를 재목적화하여 LLB를 탐지하는 ESBMC-LLB 방식을 제시합니다. 이 접근 방식은 검증 백엔드를 수정하지 않고, 프런트엔드에 경량화된 모델링 레이어를 도입하여 숨겨진 로직을 노출하고 탐지를 공식적인 안전 속성 확인(safety property check)으로 재구성합니다.

핵심 구성 요소

함수 블록 본체 번역(Function-Block-Body Translation):
- 저자들은 기존 LD 검증기들이 FB 본체를 버린다는 점에 주목했습니다. ESBMC-LLB는 사용자 정의 FB 본체를 파싱하여 이를 네이티브 GOTO 코드(할당, 루프, 비교)로 번역합니다.
- 이를 통해 FB 내부에 존재하는 악성 로직이 IR에 포함되도록 보장하며, 검증기가 해당 로직에 도달할 수 있도록 합니다.
탐지 메커니즘:
본 방식은 LLB 페이로드를 특정 안전 위반 사항에 매핑합니다:
- 스캔 와치독(Scan-Watchdog, 제어 거부/비종료 탐지용): 실제 PLC 와치독 타이머를 충실히 모사하여 모든 런(rung) 루프 내에 유계된 반복 카운터를 단언(assert)합니다. 만약 트리거에 의해 제어되는 페이로드가 비종료 루프에 진입하면, 이는 예산 제약을 위반하게 되어 도달 가능한 안전 위반 사항이 됩니다.
- 출력 배선(Output Wiring, 액추에이터/센서 위조 탐지용): FB 출력 핀을 해당 값을 소비하는 프로그램 변수에 연결합니다. 만약 페이로드가 값을 위조하면, 이 값이 프로그램 전체로 전파되어 공급된 안전 속성(예: 인터록된 액추에이터 간의 상호 배제)을 위반하게 됩니다.
검증 결과:
- $k$ -유도법( $k$ -Induction): 프로그램이 건전하다면, $k$ -유도법은 모든 스캔 사이클에 대해 안전 속성이 유지된다는 **유계되지 않은 증명(unbounded proof)**을 제공하여, 모델링된 클래스의 폭탄이 없음을 인증합니다.
- 유계 모델 체킹(Bounded Model Checking, BMC): 폭탄이 존재할 경우, BMC는 반례 추적(counterexample trace)을 반환합니다. 이 추적은 폭발 트리거(detonation trigger)(특정 입력 시퀀스와 스캔 사이클 횟수)를 구성하며, 이를 통해 자동 트리거 합성이 가능해집니다.

3. 주요 기여

본 논문은 다섯 가지 주요 기여를 설명합니다:

숨겨진 로직 노출: FB 본체를 검증기의 IR로 번역하는 모델링 레이어를 통해, 기존에 탐지 불가능했던 FB 상주형 폭탄을 도달 가능한 상태로 만듭니다.
트리거 합성을 포함한 이중 탐지: 비종료(와치독 활용)와 값 위조(출력 배선 활용)를 모두 탐지하는 메커니즘을 제공하며, BMC 반례를 통해 폭발 트리거를 자동으로 복구합니다.
적응형 적대자(Adaptive-Adversary)에 대한 강건성: 이 방식은 구문적 패턴이 아닌 프로그램 의미론(semantics)을 바탕으로 추론하기 때문에, CFG 기반 분류를 회피하도록 설계된 트리거(예: 계산된 상수, 다중 스캔 누적기)를 탐지할 수 있습니다.
포괄적인 평가:
- 제3자 검증: 공개된 Iacobelli 등의 데이터셋(악성 프로그램 30개)에서 100% 탐지율을 기록했습니다.
- 확장성: 310개의 프로그램으로 구성된 Boolean/Integer 분류 코퍼스에서 100% 재현율(recall)과 0% 오탐률(false positive)을 달려냈습니다(중앙값 실행 시간 70ms).
- 실제 벤치마크: 시맨틱 모델 체커를 사용하여 PLC-Defuser SWaT 아날로그 벤치마크를 평가한 첫 사례입니다.
시맨틱 vs. CFG 트레이드오프 특성화: 시맨틱 모델 체킹이 우위를 점하는 영역(Boolean/integer 로직, 선형 아날로그, 유계되지 않은 증명)과 CFG 분류가 우위를 점하는 영역(비선형 아날로그 비종료)을 명확히 구분하였습니다.

4. 실험 결과

Boolean 및 Integer 로직

Iacobelli 데이터셋: 30개의 악성 프로그램을 모두 탐지(재현율 100%)하였으며, 오탐은 발생하지 않았습니다. "UNKNOWN"으로 보고된 단 하나의 건전한 프로그램은 오탐이 아니라 정수 상태에 대한 유도 단계의 한계였습니다.
적응형 트리거: 트리거가 계산된 값, 제곱, 인수 분해 또는 시간적 누적을 통해 숨겨진 5가지 변종 폭탄을 모두 성공적으로 탐지했습니다. 반면, CFG 기반 대리 지표(proxy)는 나이브한 베이스라인(1/5)만을 탐지했습니다.
확장성: 생성된 310개의 프로그램 코퍼스(Boolean/integer)에서 100% 재현율과 0% 오탐률을 달성했으며, 중앙값 탐지 시간은 70ms였습니다.

아날로그 제어 (SWaT 벤치마크)

저자들은 비-Boolean(REAL/INT) 로직을 포함하는 PLC-Defuser SWaT(보안 수처리 플랜트) 코퍼스에 대해 방법을 평가했습니다.

파싱 기능 활성화: 아날로그 모델링 확장(REAL 타입 및 비-Boolean 코일 지원)을 통해 이 코퍼스를 시맨틱 모델 체커로 처음 파싱할 수 있었습니다.
선형 트리거 (v1.0.0): 선형 트리거 비종료 폭탄이 포함된 아카이브 릴리스에서, ESBMC-LLB는 150개 중 149개(99%)의 악성 프로그램을 탐지했으며, 오탐은 **0%**였습니다.
비선형 트리거 (Dev Snapshot): 비선형 산술 비종료 폭탄(예: $i := i*i$ )을 포함하는 후기 버전에서는 탐지율이 **49%**로 떨어졌습니다. SMT 백엔드가 루프 언롤링 과정에서 비선형 산술을 추론해야 할 때 타임아웃이 발생했기 때문입니다.
비교: 저자들은 비선형 아날로그 비종료 상황에서는 CFG 기반 분류 탐지기(예: PLC-Defuser)가 우위를 유지하는 반면, Boolean/integer 로직 및 선형 아날로그 제어에서는 시맨틱 모델 체킹이 앞선다고 명시했습니다.

5. 의의 및 주장

본 논문은 ESBMC-LLB를 모든 기존 탐지기를 대체하는 도구가 아니라, 보안 검증 지형의 특정 공백을 채우는 보완적 접근 방식으로 포지셔닝합니다:

유계되지 않은 보증: 시그니처 스캐너나 유계 모델 체킹과 달리, ESBC-LLB는 특정 클래스의 폭탄이 모든 스캔 사이클에 걸쳐 존재하지 않음을 공식적으로 증명할 수 있습니다.
자동 트리거 합성: 단순히 프로그램을 악성으로 표시하는 데 그치지 않고, 폭발을 일으키는 데 필요한 정확한 입력 시퀀스를 생성하여 포렌식 분석을 돕습니다.
난독화에 대한 강건성: CFG 기반 분류를 무력화하는 구문적 난독화 기법에 영향을 받지 않습니다.
제한 사항 인정: 저자들은 이 방식이 특정 페이로드 유형에 대해 **건전하지만 완전하지는 않다(sound but not complete)**는 점을 명시적으로 인정합니다. 즉, 종료 실패 또는 특정 안전 속성 위반을 유발하는 페이로드로 제한됩니다. 또한, 비선형 산술이 포함된 아날로그 맥락에서는 현재 CFG 분류 방식보다 성능이 뒤처집니다.

결론적으로, 본 연구는 시맨틱 모델 체킹과 CFG 분류가 상호 보완적임을 강조합니다. 시맨틱 모델 체킹은 Boolean/integer 및 선형 아날로그 로직에 대한 유계되지 않은 증명과 강건성을 제공하며, CFG 분류는 비선형 아날로그 비종료 처리에 있어 여전히 우위에 있습니다. 이러한 두 접근 방식을 결합하는 것(예: 루프 요약 또는 하이브리드 CFG 가이드 체크)이 향-후 연구의 유망한 방향으로 제시되었습니다.