"보안을 수학적으로 입증"… F*로 안전한 코드 만들기

프로그래밍의 많은 부분이 추상화, 산업화됐다고 해도 그 내부는 여전히 수학이다. 소프트웨어의 기반 수학은 프로그래밍 언어와 알고리즘을 움직이게 하고 코드를 빌드하는 데 사용하는 툴과 개념을 제공한다.
 
코드는 다양한 시점에 다양한 방식으로 실행되는 여러 함수가 복잡하게 얽힌 매듭이다. 코드가 제대로 동작한다고 짐작할 수도 있고 눈으로 볼 수도 있지만 이를 증명하는 작업은 어떨까. 함수형 프로그래밍의 몇 가지 중심 개념을 사용해 수학적으로 증명 가능한 코드를 생산하는 언어를 설계할 수 있다. 그러면 정적 분석 기법을 사용해 다양한 시작 조건 하에서 코드가 어떻게 동작할지 파악할 수 있다.
 
안전한 코드를 원한다면 증명 가능한 코드가 중요하다. 코드가 형식 안전을 위반하는 부분이 어디인지, 계획되지 않은 중단이나 메모리 오버런이 발생할 위험이 있는 부분은 어디인지를 볼 수 있어야 한다. 코드 실패는 애플리케이션의 보안에 영향을 미치므로 코드가 보안 모델을 깨뜨리는 상태가 되지 않는다는 것을 증명해야 한다.

컴퓨터 과학의 최첨단에서는 이러한 기법을 구현하고자 하는 실험적인 툴과 언어에서 수학과 코드의 교차점을 볼 수 있다. 예를 들어 마이크로소프트 리서치와 프랑스 국립 연구 센터인 인리아(Inria)에서 진행 중인 프로젝트가 있다.
 

F* 소개

F*('F스타'라고 읽음)는 프로그램 검증 기법을 지원하는 함수형 프로그래밍 언어다. F*로 코드를 쓰고 검증한 다음 타겟 언어 및 환경으로 내보낸다. 이미 성숙도가 충분히 높아서 F* 자체를 개발하는 언어로 사용하고 있으며 OCaml에서 컴파일된다. 깃허브의 개발 커뮤니티도 활발하다.
 
F*는 프로젝트 에베레스트(Project Everest)에서 안전하고 검증된 HTTPS 버전을 개발하는 데 이미 쓰이고 있다. 이 흥미로운 학계 프로젝트를 활용하면 현대의 전자상거래 환경 대부분을 뒷받침하는 주요 보안 기술을 공식적으로 증명할 수 있다.

프로젝트 에베레스트는 TLS-1.3 레코드 레이어를 포함해 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*로 코드를 쓰고 검증기를 통해 실행하고 사용할 준비가 되면 타겟 언어로 내보낸다. F*를 만든 이들은 이 언어를 함수적 정확함을 제공하고 보안 속성 및 리소스 사용을 관리하는 데 초점을 두는 “의존적 형식 지정(dependently typed)” 언어라고 설명한다. F* 위키는 시작할 때 도움이 되는 리소스를 제공하며 F* 프로그래밍을 위한 온라인 가이드도 있다.

F*로 못하는 일은 거의 없다. 함수형 프로그래밍 방법에 많은 부분을 의지하지만 다른 프로그래밍 언어처럼 사용할 수도 있다. 저수준 시스템 프로그래밍 언어로 사용할 수도, 퍼블릭 클라우드에서 다른 마이크로서비스 툴과 함께 사용 가능한 메시지 기반 분산 애플리케이션을 빌드하기 위한 툴로 사용할 수도 있다. 

언어로서 F*는 각각 특정 사용 사례에 초점을 둔 다양한 언어의 생태계로 보는 것이 더 타당하다. 이러한 영역별 내부 언어는 F* 프로그래밍에 접근하는 최선의 방법이다. 자신의 경험과 애플리케이션, 두 가지에 가장 근접한 하나를 선택하면 된다.
 
유용한 옵션 중 하나는 로우*(Low*)다. 보안이 중요한 저수준 시스템 애플리케이션을 위해 일반적으로 C를 사용할 만한 상황에서 사용한다. C 기반 프로젝트에서 익숙한 C와 비슷한 프로그래밍 방법을 컴파일을 위해 C 코드를 생성하는 내부 컴파일러와 함께 사용할 수 있다. 코드의 정확함을 관리하기 위한 스택 및 힙 메모리 관리 구조와 툴도 있다. 로우*의 함수는 안전함과 정확함을 모두 나타내는 형식 시그니처가 있고, 이것이 코드가 의도한 기능을 수행함을 보장하는 데 사용되는 증명이 된다.
 

의존적 형식과 정리 증명자

F*의 중심은 의존적 형식 개념이다. 여기서 형식의 정의는 값에 따라 달라진다. 예를 들어 반환되는 형식이 함수 인수 중 하나의 값에 의존하는 의존적 함수, 또는 한 값의 형식이 첫 번째 값의 형식에 의존하는 의존 쌍을 구성한다. 이 접근 방법은 함수의 형식 안전을 확보해서 배열이 사전에 정의된 크기를 초과하지 않도록 하는 데 유용하다. 
 
이 접근 방법은 F* 툴이 증명 확인 기능의 일부로 형식과 값을 확인해서 사용된 의존적 형식의 구조를 기반으로 애플리케이션을 테스트하는 코드를 생성할 수 있게 해준다. F*는 이를 사용하여 코드의 증명을 확보한다. 이 증명을 예를 들어 보안 정책과 비교해서 메모리 안전을 확인할 수 있다.

F*는 자동화된 정리 증명자(theorem prover)를 사용하여 만족도 모듈로 이론(SMT)으로 코드를 확인한다. 코드가 확인되면 F*는 증명할 사실을 모아 증명을 구축하고, 이후 F* Z3 SMT 솔버(Solver)에서 이 증명을 실행한다. F* Z3 SMT 솔버는 원래는 상당한 컴퓨팅 시간이 드는 복잡한 문제를 신속하게 해결하는 데 사용되는 매우 뛰어난 툴이다. 예를 들어 원래는 까마득한 시간이 걸릴 애저 방화벽 코드를 검사하는 데 몇 초면 충분하다. Z3 사용 과정은 복잡할 수 있으며 특히 수동으로 모델을 구축해야 하는 경우 더욱 복잡하다. 그러나 F*이 이 프로세스를 자동화해주므로 누구나 사용할 수 있다.
 

컴퓨터과학에서 일상적인 코딩까지

F*의 유용한 특징은 웹어셈블리(WebAssembly)를 포함한 많은 개발 환경을 타겟으로 사용할 수 있다는 점이다. 온갖 종류의 기기를 위한 크로스 플랫폼 런타임으로서의 중요함이 갈수록 커지고 있는 WASM 지원은 매우 유익하다. F*의 컴파일러 측면을 간소화해주기 때문이다. 정확함을 입증할 수 있는 코드의 기본 타겟이 샌드박스된 런타임이라면 보안 위험이 크게 낮아진다. F*와 WASM(웹 어셈블리의 독립형 웹어셈블리 시스템 인터페이스 런타임 사용)의 조합은 SCADA 산업 시스템을 위한 향상된 보안을 제공할 수 있다.
 
불과 몇 년 전까지 컴퓨터과학의 순수 연구 분야였던 것이 이제 일상화되고 있다. F*는 아직 주류는 아니지만 최초의 Z3 SMT에서 먼 길을 왔고, 증명 가능한 코드가 일상적인 개발 환경의 일부가 될 수 있음을 보여준다.

F*에는 새로운 영역별 언어가 추가되고 있으므로 로슬린(Roslyn) 컴파일러와 같은 기술의 일부가 되는 것도 가능할 것이다. 닷넷을 사용해 의존적 형식을 생성하고 이를 또 다른 F* 영역별 언어로 취급하면 사용자가 직면하는 위험을 낮추는 훨씬 더 안전한 C# 애플리케이션도 상상할 수 있다. 아직 갈 길이 멀지만 마이크로소프트가 자체 QUIC 네트워킹 스택을 구축하고 검증하기 위해 내부적으로 F*를 사용한다는 것은 F*의 본격적인 전성기가 임박했음을 의미한다. editor@itworld.co.kr