증명이 곧 코드가 되는 언어 F*, 파이어폭스와 애저를 지탱하다

소프트웨어의 정확성을 테스트로만 보장하는 시대의 한계는 오래전부터 지적돼 왔다. 테스트는 존재하는 버그를 발견할 수는 있어도 버그가 없음을 증명하지는 못한다. 이 지점을 정면으로 겨냥한 언어가 마이크로소프트 리서치와 프랑스 국립연구소 Inria, 그리고 오픈소스 커뮤니티가 함께 개발하는 F(에프 스타)다. F는 스스로를 '증명 지향(proof-oriented) 범용 프로그래밍 언어'로 규정한다. 프로그램을 짜는 동시에 그 프로그램이 명세를 만족한다는 수학적 증명을 함께 작성하고, 컴파일러가 그 증명을 검증한 뒤에야 코드가 통과되는 구조다.

의존 타입과 SMT 자동화의 결합

F*의 기술적 핵심은 세 가지 요소의 조합이다. 첫째는 의존 타입(dependent type)으로, 타입 안에 값에 대한 조건을 직접 표현할 수 있어 '이 함수는 항상 양의 정수를 반환한다' 같은 성질을 타입 수준에서 명시한다. 둘째는 SMT 솔버에 기반한 증명 자동화로, 개발자가 일일이 증명 단계를 밟지 않아도 상당 부분을 자동으로 풀어준다. 셋째는 자동화가 실패하는 지점을 사람이 직접 다루는 택틱(tactic) 기반 대화형 정리 증명이다. 순수 함수형 코드뿐 아니라 부수효과(effect)를 갖는 코드까지 다룰 수 있다는 점에서, 학술적 증명 도구에 머물지 않고 실제 시스템 소프트웨어를 겨냥한 설계임을 알 수 있다.

F로 작성한 프로그램은 기본적으로 OCaml로 컴파일된다. 여기에 더해 특정 하위 집합은 F#으로, 또는 KaRaMeL이라는 도구를 통해 C나 WebAssembly로 추출할 수 있고, Vale 툴체인을 거치면 어셈블리까지 내려갈 수 있다. 특히 C로 컴파일되는 저수준 하위 집합인 Low는 별도 튜토리얼이 제공될 만큼 실무적 비중이 크다. 고수준에서 증명을 마친 코드를 성능이 중요한 저수준 언어로 안전하게 내려보낸다는 발상은, 검증과 실행 효율을 동시에 잡으려는 이 언어의 지향점을 잘 보여준다. F 자체도 F로 구현돼 있고 OCaml로 부트스트래핑된다.

이미 실제 제품 속에서 돌아가는 코드

F가 흥미로운 이유는 연구 단계에 머물지 않고 이미 널리 쓰이는 제품에 들어가 있다는 점이다. 그 중심에 있는 것이 고신뢰 보안 통신 소프트웨어를 개발하는 우산 프로젝트 Project Everest다. 여기서 파생된 HACL은 F*로 작성해 C로 추출한 고신뢰 암호 프리미티브 라이브러리이고, ValeCrypt은 검증된 어셈블리로 같은 암호 기능을 구현한다. 이 둘을 하나로 묶은 것이 EverCrypt다. 이렇게 형식 검증을 거친 암호 코드는 모질라 파이어폭스, 리눅스 커널, 파이썬, mbedTLS, 테조스 블록체인, 전자투표 SDK인 ElectionGuard, VPN 프로토콜 WireGuard 등 광범위한 제품에서 실제로 사용되고 있다.

또 다른 축은 바이너리 포맷 파서를 생성하는 EverParse다. 형식 증명을 마친 F* 코드에서 C 파서를 뽑아내는 이 도구는 윈도우 Hyper-V에 들어가 있는데, 애저 클라우드를 통과하는 모든 네트워크 패킷이 우선 EverParse가 생성한 코드로 파싱되고 검증된다. 파서는 신뢰할 수 없는 외부 입력을 가장 먼저 받아들이는 지점이라 전통적으로 보안 취약점의 온상이었다. 이 부분을 수작업 코드가 아니라 증명된 생성 코드로 대체했다는 것은, 형식 검증이 클라우드 인프라 규모에서 실전 방어선으로 기능하고 있음을 뜻한다.

실무자가 접근할 때 고려할 점

F는 아파치 2.0 라이선스로 GitHub에 공개돼 있으며, 윈도우·리눅스·macOS용 바이너리가 정기적으로 배포되고 OPAM, 도커, Nix, 소스 빌드 등 여러 경로로 설치할 수 있다. 학습 자료 측면에서는 온라인 서적 'Proof-oriented Programming in F'가 브라우저에서 예제와 연습문제를 직접 실행해가며 읽을 수 있는 형태로 지속 갱신되고 있고, 계절 학교 강의 자료와 저수준 Low* 튜토리얼도 함께 제공된다. 질문과 공지는 GitHub Discussions와 Zulip 공개 포럼으로 창구가 통합되는 중이며, 월 1회를 목표로 하는 부정기 PoP Up 세미나도 열린다.

다만 한국의 일반적인 개발 조직이 곧바로 도입하기에는 진입 장벽이 분명하다. 의존 타입과 정리 증명은 별도의 학습 곡선을 요구하고, 증명을 함께 작성해야 하는 개발 방식은 일반적인 애플리케이션 개발의 생산성 감각과 다르다. 따라서 F는 모든 코드를 대체하는 도구라기보다, 암호 구현이나 프로토콜 파서처럼 결함의 대가가 치명적이고 명세가 명확한 핵심 모듈에 선별적으로 투입할 때 가치가 극대화된다. 이미 검증을 마친 HACL이나 EverCrypt 같은 산출물을 라이브러리로 가져다 쓰는 방식이라면, 언어 자체를 익히지 않고도 형식 검증의 결실을 취하는 현실적인 접근이 될 수 있다. F*라는 이름의 시스템이 처음 논문으로 등장한 것이 2011년, 현재 형태로 다시 설계된 것이 2015년임을 감안하면, 이 언어는 10년 넘게 이론과 산업 적용을 오가며 다져진 성숙한 실험으로 볼 만하다.