⚡ electrical engineering

ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs

본 논문은 선언적 하드웨어 추상화 계층과 건전한 입력 범위 모델링을 통합하여 이상적인 정수 가정으로 인한 허위 경보를 제거하는 동시에, 자원이 제한된 마이크로컨트롤러에서 실행되는 IEC 61131-3 프로그램의 실제 너비 의존적 결함을 탐지함으로써 오픈 하드웨어 PLC의 배포 격차를 해소하는 하드웨어 충실도 기반 검증 프레임워크인 ESBMC-Arduino를 소개한다.

원저자: 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 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

당신이 수조를 관리하는 로봇을 만들고 있다고 상상해 보십시오. 당신은 IEC 61131-3이라는 특별한 언어로 명령어를 작성하는데, 이는 산업용 기계를 위한 일종의 범용 레시피 북과 같습니다. 수년 동안 엔지니어들은 이 레시피가 안전한지 확인하기 위해 "슈퍼 로봇" 시뮬레이터를 사용해 왔습니다. 이 시뮬레이터는 마치 무한한 숫자를 생각할 수 있는 마법사와 같아서, 로봇이 음의 무한대부터 양의 무한대까지 어떤 숫자든 머릿속에 담을 수 있고, 센서가 상상 가능한 모든 값을 보고할 수 있다고 가정합니다.

하지만 여기 반전이 있습니다. 당신이 실제로 만든 로봇은 마법사가 아닙니다. 그것은 실제 세상에 존재하는 아주 작고 저렴한 마이크로컨트롤러(아두이노 같은 것)입니다. 이 작은 칩은 매우 구체적이고 제한된 두뇌를 가지고 있습니다. 이 칩은 오직 32,767까지만 숫자를 담을 수 있습니다. 만약 계산값이 이보다 높아지면, 숫자는 단순히 커지는 것이 아니라, 부서지고 바닥으로 튕겨 나가 음수로 변해 버립니다. 이것은 마치 숫자가 999,999에서 000,000으로 되돌아가는 자동차 주행거리계와 같습니다.

거대한 괴리 (The Great Disconnect)
논문은 이를 "배포 간극(deployment gap)"이라고 부릅니다. 이것은 마법사의 꿈의 세계와 로봇의 좁디좁은 현실 사이의 차이입니다.

저자들은 엔지니어들이 코드를 점검하기 위해 기존의 "마법사" 시뮬레이터를 사용했을 때, 엄청난 양의 가짜 알람(false alarms)을 얻게 된다는 것을 발견했습니다. 테스트한 123개의 실제 프로그램 중, 기존 시뮬레이터는 54번이나(**44%**의 가짜 알람 발생률) "위험!"이라고 비명을 질렀습니다. 하지만 자세히 살펴보니, 이 "위험"들은 불가능한 것들이었습니다. 시뮬레이터는 -32,764와 같은 센서 값을 상상하고 있었습니다. 실제 세상에서 이 로봇에 연결된 센서는 0에서 1,023 사이의 숫자만 읽을 수 있습니다(10비트 센서이기 때문입니다). -32,764라는 값은 마치 온도계가 "영하 32,764도"라고 읽는 것과 같습니다. 그런 일은 일어날 수 없습니다.

저자들은 단순히 수학적 오류를 체크하는 것뿐만 아니라 센서가 실제로 무엇을 볼 수 있는지도 함께 체크해야 한다고 주장합니다. 그렇게 하지 않으면 검증이 실제 상황에서 "부적절(unsound, 신뢰할 수 없는)"하게 된다는 것을 보여줍니다.

마법 같은 해결책: HAL 디스크립터 (The Magic Fix: The HAL Descriptor)
이를 해결하기 위해 저자들은 ESBMC-Arduino라는 새로운 도구를 만들었습니다. 이 도구를 "현실 점검(Reality Check)" 필터라고 생각하십시오.

마법사 시뮬레이터가 코드를 보기 전에, 이 새로운 도구는 모든 센서에 아주 작은 자동 메모를 붙입니다. "이봐, 기억해, 이 센서는 0에서 1,023 사이의 숫자만 줄 수 있어"라고 말이죠. 또한 시뮬레이터에게 "그리고 로봇의 두뇌는 32,767까지만 숫자를 담을 수 있다는 걸 잊지 마"라고 상기시킵러줍니다.

이 규칙들을 가지고 시뮬레이터를 실행하면 마법 같은 일이 일어납니다:

54개의 가짜 알람이 즉시 사라집니다. -32,764라는 유령은 이제 그 숫자가 불가능하다는 것을 알기에 사라졌습니다.
이미 안전하다고 증명된 32개의 프로그램은 그대로 안전하게 유지됩니다.
가장 중요한 것은, 이 도구가 실제 버그를 놓치지 않았다는 점입니다. 도구는 기존 시뮬레이터들이 특정 종류의 진짜 위험을 숨기고 있었다는 것을 찾아냈습니다: 바로 센서 값이 큰 숫자(예를 들어, 원시 센서 값을 백분율로 변-환하는 과정)와 곱해질 때, 계산이 16비트 로봇의 두뇌 용량을 초과하는 경우입니다.

진짜 위험 (그리고 그것이 얼마나 드문지)
논문은 기존의 "유령 알람"은 흔했지만, 이 간극으로 인해 발생하는 진짜 버그는 테스트한 공개 코드에서 의외로 드물었다는 점을 발견했습니다. 그들은 16비트 보드에서 센서 값이 큰 상수(예: 100)와 곱해지는 특정 시나리오에서만 실제 결함을 발견했습니다.

예를 들어, 센서가 898(정상적인 실제 값)을 읽고 코드가 여기에 100을 곱한다면, 결과는 89,800이 됩니다. 이는 16비트 로봇의 두뇌(최대 32,767)에는 너무 큽니다. 숫자는 되돌아가 버려 음수가 되고, 로봇은 수조가 가득 차 있음에도 불구하고 비어 있다고 착각하게 됩니다. 새로운 도구는 정확히 이 시나리오를 잡아냈으며, 엔지니어들에게 크래시를 일으킬 수 있는 실제 센서 값을 물리적인 예시와 함께 제공했습니다.

이 논문이 주장하지 않는 것
저자들은 자신들이 하지 않은 일에 대해서도 매우 정직합니다. 그들은 모든 프로그램이 이제 안전하다고 증명한 것이 아닙니다. 123개의 프로그램 중 91개는 "알 수 없음(unknown)"이라는 판정을 받았습니다. 이는 도구가 고장 났기 때문이 아니라, 현재의 엔진으로는 해당 프로그램들의 안전을 증명하기 위한 수학적 난도가 너무 높기 때문입니다. 도구는 노이즈(가짜 알람)를 성공적으로 제거하고 신호(실제 증명)를 유지했지만, 아직 가장 어려운 퍼즐들을 모두 풀지는 못했습니다. 또한, 이들은 부동 소수점 숫자(3.14와 같은 소수)나 복잡한 물리 시뮬레이션을 테스트하지 않았습니다. 그들은 엄격하게 정수(integers)와 불리언 로직(on/off 스위치)에 집중했습니다.

결론 (The Bottom Line)
이 논문은 오픈 하드웨어 PLC(학교나 작은 공장에서 사용되는 것들)를 검증하려면, 단순히 수학만 체크해서는 안 되며 하드웨어의 한계를 반드시 체크해야 한다는 것을 보여줍니다. 센서가 실제로 무엇을 할 수 있는지 알려주는 "현실 점검"을 자동으로 추가함으로써, 그들은 소음이 심하고 신뢰할 수 없던 도구를 믿을 수 있는 도구로 바꾸어 놓았습니다. 그들이 수백만 개의 새로운 버그를 찾아낸 것은 아니지만, 도구가 계속해서 헛소리를 하는 것을 막아줌으로써 엔지니어들이 다시 안전 점검 결과를 신뢰할 수 있게 만들었습니다.

기술 요약: ESBMC-ARDUINO

문제점: 오픈 하드웨어 PLC의 배포 격차(Deployment Gap)
Arduino OPTA, CONTROLLINO, Industrial Shields M-Duino 등에서 실행되는 OpenPLC와 같은 오픈 하드웨어 프로그래머블 로직 컨트롤러(PLC)는 저가형 마이크로컨트롤러급 장치에 대해 IEC 61131-3 프로그래밍을 대중화했습니다. 이러한 플랫폼은 교육, 소규모 자동화, 그리고 산업 제어 시스템(ICS) 보안 연구를 위한 런타임 기질로서 점점 더 많이 사용되고 있습니다. 그러나 기존의 오픈 소스 검증기(예: ESBC-PLC, PLCverif)에서 사용하는 추상 모델과 실제 하드웨어 실행 환경 사이에는 결정적인 "배포 격차"가 존재합니다.

현재의 검증기들은 이상적이고 무제한적인 정수와 제약 없는 입력을 가정하는 추상적인 스캔 사이클 모델 위에서 작동합니다. 반면, 실제로 배포된 아티팩트들은 특정 머신 워드 너비(예: 8비트 AVR 보드에서의 16비트 int)와 유한한 해상도의 아날로그-디지털 변환기(ADC, 일반적으로 10비트이며 $[0, 1023]$ 범위를 가짐)를 가진 자원 제한적인 마이크로컨트롤러 유닛(MCU)에서 실행됩니다. 이러한 불일치는 두 가지 실패 모드로 이어집니다:

결함 미검출(Missed Defects): 프로그램이 추상 모델에서는 안전하다고 증명되었으나, 좁은 워드 너비로 인한 정수 오버플로(예: 16비트 보드에서 스케일링 계산이 래핑되는 현상)로 인해 실제 장치에서는 안전하지 않을 수 있습니다.
팬텀 알람(Phantom Alarms, 허위 양성): 더 심각하게도, 워드 너비는 고려하지만 하드웨어 입력 범위를 무시하는 단순한 너비 인식 검증은 물리적 ADC가 생성할 수 없는 센서 값(예: 음수 또는 1023을 초과하는 값)을 탐색합니다. 이는 허위 오버플로 보고를 초래합니다. 123개의 실제 제3자 프로그램을 대상으로 한 평가 결과, 단순한 16비트 오버플로 체크는 **44%의 허위 알람율(123개 중 54개)**을 보이는 반면, 실제 결함은 단 하나도 발견하지 못했습니다.

방법론: 하드웨어 충실도 기반 검증(Hardware-Faithful Verification)
본 논문은 대상 하드웨어를 충실하게 표현하는 "배포 모델"( $M_{dev}$ )을 구축함으로써 이 격차를 해소하는 방법을 제안합니다. 이 접근 방식의 핵심은 하드웨어 추상화 계층(HAL) 디스크립터와 건전한 로워링(Sound Lowering) 프로세스입니다.

HAL 디스크립터 ( $H$ ): 다음을 포착하는 선언적 튜플 $H = \langle w, b_{adc}, b_{pwm}, \mu \rangle$ $H = ⟨ w, b_{a d c}, b_{pw m}, μ ⟩$ 입니다.
- $w$ : 머신 워드 너비 (예: AVR의 16비트, ARM의 32비트).
- $b_{adc}$ 및 $b_{pwm}$ : 아날로그-디지털 변환기 및 펄스 폭 변조 출력의 해상도.
- $\mu$ : IEC 61131-3 직접 주소 지정 체계로부터 자동으로 도출된 I/O 바인딩 맵 (예: %IW 주소는 특정 ADC 범위를 가진 아날로그 입력에 매핑됨).
충실한 로워링(Faithful Lowering): 이 방법은 PLC 프로그램( $P$ $P$ )을 대상 하드웨어를 충실히 표현하는 배포 모델( $M_{dev}(P, H)$ $M_{d e v} (P, H)$ )로 변환합니다.
- 대상 워드 너비 $w$ 에서 산술 연산을 해석합니다 (2의 보수 래핑을 정확히 재현).
- 입력 샘플링 직후에 assume 제약 조건을 삽로하여 변수를 하드웨어적으로 구현 가능한 범위로 제한합니다 (예: $0 \leq adc \leq 1023$ ).
- 비선형 함수 블록(예: PID)을 트랙터빌리티(tractability) 유지를 위해 비결정론적 출력으로 과대 근사(over-approximation)합니다.
검증 엔진: 수정 없이 ESBMC 백엔드(SMT 기반 유계 모델 체킹 및 $k$ -유도)를 재사용합니다. 로워링은 래더 다이어그램(LD) 프론트엔드에서 발생하며, 입력 범위를 강제하고 아키텍처 워드 너비를 설정하는 경량 훅(약 40줄)을 추가합니다.

주요 기여

하드웨어 충실도 검증 방법: 안전 필수 임베디드 C(Frama-C 및 Astrée와 같은 도구에 의해 확립된)의 타겟-모델 규율을 PLC 영역으로 전이하는 공식적인 접근 방식을 제안합니다. 이러한 도구들과 달리, 본 방법은 자동으로 입력 범위를 도출합니다(IEC 61131-3 주소 지정 체계 및 보드 디스크립터로부터).
ESBMC-Arduino 인스턴스화: 공식 Arduino 코어로부터 HAL 파라미터를 가져오는 Arduino 클래스 타겟을 위한 구체적인 구현체입니다. 이는 16비트(AVR) 및 32비트(ARM) 타겟을 모두 지원합니다.
경험적 평가: 123개의 실제 프로그램과 20개의 패턴으로 구성된 통제된 코퍼스에 대한 엄격한 평가를 수행했습니다.

결과

허위 알람 제거: 123개 프로그램 코퍼스에서 HAL 어노테이터를 활성화함으로써 모든 54개의 허위 알람을 제거하였고(불안전 개수를 54개에서 0개로 감소), 모든 견고성 증명(32개 프로그램이 여전히 안전한 것으로 판명됨)을 유지했습니다.
실제 결함 탐지: 통제된 코퍼스는 본 방법이 물리적으로 실현 가능한 증거(witness)와 함께 실제 너비 의존적 결함(예: 16비트 보드에서의 ADC-to-percentage 스케일링 오버플로)을 탐지함을 보여주었습니다.
교차 도구 검증: 로직의 C 미러에 대해 독립적인 도구(CBMC 및 Frama-C/EVA)를 사용하여 "팬텀 알람" 현상을 재현하였으며, 이는 문제가 ESBMC에 국한된 것이 아니라 입력 모델링이 없는 나이브한 너비 인식 검증의 고유한 문제임을 확인시켜 줍니다.
성능: HAL 어노테이터의 오버헤드는 무시할 수 있는 수준입니다. 검증 시간은 프로그램당 1초 미만으로 유지됩니다.
한 한계점: 허위 알람은 제거되었으나, 91개의 프로그램이 내부 상태를 가진 함수 블록에서의 $k$ -유도 불완전성으로 인해 "알 수 없음(unknown)" 판정을 받았습니다. 이는 프로버의 유도 단계를 닫는 능력에 대한 한계이지, 입력 모델의 문제는 아닙니다.

의의
본 논문의 주요 가치는 발견된 버그의 개수(조사된 특정 공개 코퍼스에서는 불리언 및 타이머 로직이 지배적이어서 버그가 드묾)가 아니라, 건전성(soundness)의 회복에 있다고 주장합니다. 저자들은 나이브한 너비 인식 검증이 44%의 허위 알람율로 인해 검증 결과를 신뢰할 수 없게 만들며, 이로 인해 실제 결함을 찾아내는 능력을 저해한다는 점을 입증했습니다. 하드웨어적으로 실현 가능한 입력 범위를 자동으로 도출함으로써, 본 방법은 신뢰할 수 없는 도구를 실현 가능한 보고만을 발행하는 도구로 변환하여 엔지니어가 오픈 하드웨어 PLC에 대해 검증 결과를 신뢰할 수 있게 합니다. 이 접근 방식은 새로운 제안을 하는 대신, 성숙한 검증 인프라와 통합되는 현실적이고 저비용의 채택 전략(4개 필드의 디스크립터와 40줄의 훅)으로 제시됩니다.

유사한 논문