Ada와 SPARK로 Cortex-M 정복하기: 임베디드 환경의 형식 검증과 그 한계

임베디드 시스템에서 C나 C++로 코드를 작성하다 보면, 어느 순간 알 수 없는 HardFault와 싸우고 있는 자신을 발견하게 된다. 15년 넘게 이 바닥에서 수많은 메모리 오염과 Undefined Behavior를 디버깅해왔지만, 솔직히 이 짓을 언제까지 해야 하나 싶을 때가 있다. 그래서 오늘은 조금 다른 접근법, 바로 Ada와 SPARK를 활용한 형식 검증(Formal Verification) 에 대해 이야기해보려 한다.

C/C++의 늪에서 벗어나기

대부분의 임베디드 엔지니어에게 Ada는 항공우주나 국방 분야에서나 쓰는 고인물 언어로 취급받는다. 하지만 SPARK와 결합하면 이야기가 완전히 달라진다. SPARK는 Ada의 서브셋으로, 코드가 특정 속성(예: 런타임 에러 없음, 데이터 흐름의 무결성)을 만족함을 수학적으로 증명할 수 있게 해준다.

최근 Inspirel에 올라온 ‘Ada and Spark on ARM Cortex-M’ 튜토리얼을 보면서, 이를 Arduino나 Nucleo 보드 같은 친숙한 타겟에 올리는 과정을 다시금 흥미롭게 살펴봤다.

Cortex-M에 Ada와 SPARK 올리기

튜토리얼 자체는 매우 실용적이고 훌륭하다. GNAT 툴체인을 셋업하고, 레지스터 맵을 매핑해서 LED를 깜빡이는 기초적인 과정부터 꼼꼼하게 다룬다.

개인적으로 가장 마음에 드는 부분은 하드웨어 레지스터를 다루는 방식이다. C언어에서 흔히 보는 volatile 포인터 캐스팅 범벅인 헤더 파일 대신, Ada의 엄격한 타입 시스템과 Representation Clause를 사용해 레지스터를 매핑한다. 이 방식은 초기 셋업에 시간이 조금 더 걸릴지 몰라도, 한번 작성해두면 컴파일러가 비트 필드 수준의 오류를 런타임 이전에 잡아낸다는 점에서 압도적인 안정성을 제공한다. 2018년쯤에 의료기기 펌웨어를 개발할 때 C++ 템플릿 메타프로그래밍으로 비슷한 타입 안정성을 확보하려고 발버둥 쳤던 기억이 나는데, Ada는 언어 차원에서 이를 우아하게 지원한다.

형식 검증의 한계: ARM은 왜 Cortex-M ASL을 공개하지 않는가?

소프트웨어 레벨에서 SPARK로 아무리 수학적 무결성을 증명해봤자, 하드웨어 스펙과 맞물리지 않으면 반쪽짜리 증명에 불과하다. 이번 Hacker News 스레드에서 한 유저(anon)가 남긴 댓글이 내 뼈를 강하게 때렸다.

“ARM이 최근 A 시리즈 아키텍처에 대해서는 ASL(Architecture Specification Language)로 기계 판독 가능한 스펙을 공개해서 정말 멋지다고 생각했는데, M 시리즈에 대해서는 그렇게 하지 않아 극도로 짜증난다.”

이게 왜 치명적일까? 진정한 의미의 Full-stack Formal Verification을 달성하려면 우리가 작성한 코드가 컴파일된 어셈블리가 실제 CPU 파이프라인과 메모리 모델 위에서 어떻게 동작하는지 기계적으로 증명할 수 있어야 한다. Cortex-A는 ASL이 공개되어 있어 이를 형식 검증 스택에 통합하기 수월해졌다.

하지만 정작 안전 필수(Safety-Critical) RTOS나 베어메탈 펌웨어가 가장 많이 돌아가는 Cortex-M은 기계 판독 가능한 공식 스펙 이 없다. 결국 검증 툴을 만드는 사람들이 PDF 매뉴얼을 보고 수동으로 모델링을 해야 한다는 뜻인데, 이는 휴먼 에러의 여지를 남긴다. 생태계 확장을 가로막는 ARM의 이런 폐쇄적인(혹은 게으른) 행보는 솔직히 이해하기 어렵다.

결론 (Verdict)

그렇다면 Cortex-M 환경에서 Ada와 SPARK를 도입하는 것은 단순한 장난감 수준일까? 절대 아니다.

미션 크리티컬한 환경이나 높은 신뢰성이 요구되는 시스템이라면, C/C++의 디버깅 늪에 빠지는 것보다 초기 학습 곡선을 감수하더라도 Ada와 SPARK를 실전 도입할 가치가 충분하다. Inspirel의 튜토리얼은 그 훌륭한 출발점이다.

하지만 완벽한 시스템 수준의 형식 검증을 꿈꾸는 엔지니어들에게 하드웨어 벤더(특히 ARM)의 미온적인 지원은 여전히 큰 아쉬움이자 넘어야 할 산으로 남아있다.

References