From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware

기술 요약: Rocq에서 Metal까지

문제 정의
대규모 언어 모델(LLM)의 확산은 코드 생성 비용을 획기적으로 낮추었으나, 이는 생성된 펌웨어의 양을 코드 리뷰가 따라잡을 수 없는 안전 필수 임베디드 시스템에서 심각한 병목 현상을 야기했습니다. 형식 검증(Formal Verification)은 수학적으로 불변량(invariants)을 증명함으로써 해결책을 제시하지만, Rocq와 같은 정리 증명기(Theorem Prover)에서 추출된 표준 추출 파이프라인은 하드웨어 제약으로 인해 임베디드 타겟으로의 이행에 실패합니다. Lean 4, OCaml 또는 표준 Scheme과 같은 언어의 기존 런타임은 너무 크거나, 제한된 RAM(예: ST33J2M0의 50 KB)과 호환되지 않는 가비지 컬렉션 메커니즘에 의존하거나, 마이크로컨트롤러에는 존재하지 않는 호스트 환경(OS 지원, libc)을 요구합니다. 결과적으로 개발자들은 엄밀함과 합성성(composability)을 희생하면서 수동 번역이나 호스트 언어 확장 방식에 의존하게 됩니다.

방법론
저자들은 자원이 제한된 마이크로컨트롤러(특히 Cortex-M35P)에서 형식적으로 검증된 로직을 직접 실행하도록 설계된 완전한 엔드 투 엔드 파이프라인인 **Encore!**를 제안합니다. 이 방법론은 세 가지 기둥에 기초합니다:

1. 아키텍처 모델: 펌웨어는 순수 상태 전이 함수로 구조화됩니다: step : State × Event → State × (list Effect).

   • **State(상태)**는 애플리케이션 로직을 나타냅니다.
   • **Event(이벤트)**는 입력(예: USB 패킷, 버튼 누름)을 나타냅니다.
   • **Effect(효과)**는 호스트에 의해 해석될 부수 효과(예: I/O, 디스플레이)를 기술합니다.
   • 이러한 분리는 핵심 비즈니스 로직이 Rocq에서 증명 가능한 순수 함수임을 보장하며, 검증되지 않은 신뢰 컴퓨팅 기반(TCB)—이벤트 폴러(event poller)와 효과 해석기(effect interpreter)로 구성됨—의 크기를 애플리케이션 복잡도와 관계없이 일정하게 유지합니다.

2. 추출 타겟 선택: 저자들은 여러 추출 경로(Lean 4, OCaml, CertiRocq, Scheme)를 평가했습니다. 그들은 Scheme이 유일하게 실행 가능한 타겟이라고 판단했는데, 이는 Scheme이 강제적인 가비지 컬렉션 요구 사항이 없고 컴팩트한 의미론을 가지고 있기 때문입니다. 그러나 표준 Scheme 구현체(Chibi 또는 Ribbit 등)는 플래시 예산을 초과하거나 Rocq 추출에서 생성된 특정 매크로(예: quasiquote)를 지원하지 못하는 것으로 나타났습니다.

3. Encore! VM 및 컴파일러:

   • **Encore!**는 CPS(Continuation Passing Style) 바이트코드를 실행하는 베어메탈, no_std Rust 가상 머신입니다.
   • 이는 256개의 레지스터를 가진 레지스터 기반 아키텍처를 사용하며 콜 스택(call stack)이 없어, 숨겨진 제어 흐름을 제거하고 가비지 컬렉션(GC)을 단순화합니다.
   • GC는 모든 활성 레지스터를 루트(root)로 취급하는 마크-컴팩트(mark-compact) 알고리즘을 사용하여 무제한적인 스택 스캐닝을 방지합니다.
   • 컴파일 파이프라인은 Rocq에서 추출된 Scheme을 Direct-Style IR로 변환하고, 적용(application)을 언커리(uncurry)하며, De Bruijn 인덱스를 사용하여 CPS로 변환하고, 최적화한 후 바이트코드로 컴파일합니다.
   • 호스트 인터페이스는 절차적 매크로를 사용하여 Rust 호스트 타입과 VM 생성자 태그 간의 타입 안전한 바인딩을 생성함으로써 검증된 브리지를 보장합니다.

주요 기여

1. 실행의 입증: 본 논문은 Scheme을 추출 타겟으로 선택하고 목적에 맞게 제작된 베어메탈 런타임을 구축함으로써, Rocq에서 추출된 코드가 Cortex-M 마이크로컨트롤러에서 성공적으로 실행될 수 있음을 입증합니다.
2. Encore! 구현: 저자들은 ST33 클래스 하드웨어(구체적으로 ST33J2M0의 50 KB RAM 제약)의 리소스 예산 내에 들어오는 no_std CPS 바이트코드 VM인 Encore!를 제시하며, 이를 통해 Rocq에서 추출된 Scheme을 엔드 투 엔드로 실행합니다.
3. 검증된 아키텍처: 펌웨어를 순수 상태 전이 함수로 구조화하는 아키텍처를 도입합니다. 이를 통해 핵심 로직은 Rocq에서 완전히 증명할 수 있는 동시에, 검증되지 않은 경계(unverified boundary)의 크기를 고정하여 하드웨어 복잡도와 상관없이 검증 노력을 분리할 수 있습니다.

실험 결과
저자들은 Ledger Flex 트랜잭션 서명 애플리케이션을 통해 접근 방식을 검증하였으며, QEMU 및 실제 하드웨어 상에서 7가지 벤치마크(산술, FSM, Red-Black tree)를 통해 Encore!를 CertiRocq와 비교하였습니다.

• 실행 가능성: 모든 추출 경로 중에서 Encore!와 CertiRocq만이 실행 가능한 후보였습니다. 그러나 CertiRocq는 베어메탈에서 작동하기 위해 런타임에 대한 정밀한 수정이 필요했으며, 동적 할당 워크로드에서 실패했습니다.
• 리소스 사용량:
  • 플래시(Flash): CertiRocq는 직접 어셈블리 컴파일을 수행하기 때문에 단순 산술 작업에서는 더 작은 바이너리(56배 작음)를 생성하지만, 리스트 생성을 인라인화하기 때문에 규모가 커질수록 성능이 저하됩니다(rbtree-100의 경우 146 KB). 반면 Encore!는 생성이 런타임에서 처리되므로 일정한 풋프린트(18 KB)를 유지합니다.
  • 힙(Heap): Encore!는 메모리 사용량 측면에서 CertiRocq를 크게 앞섭니다. CertiRocq는 산술을 위해 Peano 자연수를 사용하여 엄청난 힙 팽창을 일으키며(예: rbtree-100에 대해 약 63 KB가 필요하여 50 KB RAM 제한을 초과), 반면 Encore!의 마크-컴팩트 GC는 낮은 요구 사항(예: 3.7 KB)을 유지합니다.
  • 빌드 시간: Encore!는 단순한 경우 1.3~2.6배 빠르게 빌드되며, 복잡한 경우(rbtree-100)에는 CertiRocq에 필요한 무거운 C 코드 생성 및 최적화 단계를 피함으로써 최대 665배 더 빠르게 빌드됩니다.
• 실제 검증: 약 400줄의 검증된 Gallina 로직과 약 575줄의 검증되지 않은 Rust 호스트 코드로 구성된 트랜잭션 서명 앱이 실제 Ledger Flex 하드웨어에 성공적으로 배포되었습니다. 이 앱은 데이터를 올바르게 파싱, 표시 및 서명하며, "파싱 중 바이트 누락 없음" 및 "ASCII 유효성"과 같은 속성들이 머신 체크되었습니다.

의의
본 논문은 명세 언어의 엄밀함을 희생하지 않고도 베어메탈에서 형식적으로 검증된 펌웨어를 구현하는 것이 오늘날 가능하다고 주장합니다. 펌웨어를 순수 상태 전이 함수로 구조화함으로써, 이 접근 방식은 검증된 코어가 애플리케이션 복잡도에 따라 확장될 수 있도록 하는 동시에 검증되지 않은 경계는 고정된 상태로 유지할 수 있게 합니다. 이러한 아키텍처는 특히 LLM 시대에 중요합니다. 이는 AI가 생성한 코드를 정리 증명을 통해 자동으로 검증할 수 있는 워크플로우를 가능하게 하여, 수동 코드 리뷰를 머신 체크가 가능한 증명 리뷰로 대체할 수 있게 합니다. 저자들은 컴파일러 패스와 VM 자체를 검증하는 등의 엔지니어링 작업이 남아있지만, 제한된 임베디드 타겟에서 증명된 로직을 실행하는 데 있어 근본적인 장벽이 극복되었다고 결론짓습니다.