본문 바로가기

Home > 열린마당 > 공개SW 소식

공개SW 소식

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

support 게시글 작성 시각 2021-08-31 16:09:36 게시글 조회수 4704

2021.08.31.
ⓒITWorld / Simon Bisson | InfoWorld

 

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

컴퓨터 과학의 최첨단에서는 이러한 기법을 구현하고자 하는 실험적인 툴과 언어에서 수학과 코드의 교차점을 볼 수 있다. 예를 들어 마이크로소프트 리서치와 프랑스 국립 연구 센터인 인리아(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*의 중심은 의존적 형식 개념이다. 여기서 형식의 정의는 값에 따라 달라진다. 예를 들어 반환되는 형식이 함수 인수 중 하나의 값에 의존하는 의존적 함수, 또는 한 값의 형식이 첫 번째 값의 형식에 의존하는 의존 쌍을 구성한다. 이 접근 방법은 함수의 형식 안전을 확보해서 배열이 사전에 정의된 크기를 초과하지 않도록 하는 데 유용하다. 
(후략)

 

[원문 기사 : https://www.itworld.co.kr/news/206384 ]

 

※ 본 내용은 한국아이디지(주) (https://www.idg.co.kr/)의 저작권 동의에 의해 공유되고 있습니다.
Copyright ⓒ 2020 International Data Group. 무단전재 및 재배포 금지. 
 

맨 위로
맨 위로