코드는 다양한 시점에 다양한 방식으로 실행되는 여러 함수가 복잡하게 얽힌 매듭이다. 따라서 함수형 프로그래밍의 몇 가지 중심 개념을 사용해 수학적으로 증명 가능한 코드를 생산하는 언어를 설계할 수 있다.
마이크로소프트 리서치와 프랑스 국립 연구 센터인 인리아(Inria)에서 진행 중인 프로젝트인 F*('F스타'라고 읽음)는 프로그램 검증 기법을 지원하는 함수형 프로그래밍 언어다. F*로 코드를 쓰고 검증한 다음 타겟 언어 및 환경으로 내보낸다. 이미 성숙도가 충분히 높아서 F* 자체를 개발하는 언어로 사용하고 있으며 OCaml에서 컴파일된다. 깃허브의 개발 커뮤니티도 활발하다.
F*는 프로젝트 에베레스트(Project Everest)에서 안전하고 검증된 HTTPS 버전을 개발하는 데 이미 쓰이고 있다. 이는 프로토콜의 중요한 부분으로, 애플리케이션과 HTTPS 내부 사이를 잇는 다리 역할을 한다. 프로젝트 에베레스트는 F*를 통해 레코드 레이어 자체가 안전함을 보장할 수 있었고, 그 결과로 얻은 miTLS 코드는 마이크로소프트의 QUIC HTTP 표준 구현의 일부를 구성한다.
F*은 HACL*(High Assurance Cryptographic Library) 및 베일크립트(ValeCrypt) 라이브러리의 일부로 일반적인 암호화 라이브러리의 검증된 버전을 생성해 코드를 C 및 어셈블리로 내보내는 데 사용한다. HACL* 및 베일크립트 위에 위치하는 에버크립트(EverCrypt) 암호화 공급자에도 사용돼 프로세서 및 실행 환경을 기준으로 알고리즘의 최적 구현을 선택한다. 애저 컨피덴셜 컨소시엄(Azure Confidential Consortium) 프레임워크와 리눅스 커널에 사용되는 와이어가드(WireGuard) VPN에도 사용된다.
그 외에 F* 구현의 혜택을 얻은 툴에는 시그널(Signal) 보안 메시징 프로토콜의 웹어셈블리(WebAssembly) 구현, 마이크로컨트롤러 펌웨어에서 실행되는 부팅 툴인 DICE(Device Identifier Composition Engine)의 검증된 버전이 있다. 깃허브에서 프로젝트 에베레스트의 작업 대부분을 찾을 수 있으며 소스 코드와 리눅스 도커 이미지는 매일 빌드된다.
F*는 비주얼 스튜디오 코드를 포함한 대부분의 주요 편집기를 위한 툴을 제공한다. F*로 코드를 쓰고 검증기를 통해 실행하고 사용할 준비가 되면 타겟 언어로 내보낸다. F*를 만든 이들은 이 언어를 함수적 정확함을 제공하고 보안 속성 및 리소스 사용을 관리하는 데 초점을 두는 “의존적 형식 지정(dependently typed)” 언어라고 설명한다. F* 위키는 시작할 때 도움이 되는 리소스를 제공하며 F* 프로그래밍을 위한 온라인 가이드도 있다.
[저작권자ⓒ CWN(CHANGE WITH NEWS). 무단전재-재배포 금지]
