리서치 연구
C*: C 언어 프로그래밍과 검증을 통합하는 새로운 접근
C*: Unifying Programming and Verification in C
Hacker News시스템 소프트웨어의 안전성 확보를 위해, 프로그래밍 코드와 논리적 검증을 통합한 새로운 언어 디자인 'C*'가 개발되었습니다.
세 줄 요약
- C*는 C 코드를 기반으로 하며, 구현 코드와 증명(Proof) 코드를 같은 환경에 임베딩하여 실시간 검증이 가능하도록 개발 과정을 통합합니다.
- 기존에는 프로그래밍과 검증 과정의 분리로 높은 비용이 발생했으나, C*를 통해 개발자가 직접 안정성을 확인하며 신뢰도 높은 시스템 소프트웨어를 만들 수 있습니다.
- 현재는 프로토타입 단계이며, 작은 C 프로그램부터 pKVM 할당자 함수 같은 복잡한 실제 사례까지 광범위한 검증 능력을 성공적으로 입증했습니다.
안전성이 중요한 시스템 소프트웨어의 정확한 기능 구현은 형식 검증 연구 및 응용 분야에서 핵심 과제입니다. 기존에는 개발 과정에서 프로그래머가 자신의 코드를 직접 검증하는 경우가 드물어, 검증된 소프트웨어를 개발하고 유지보수하는 데 높은 비용이 발생했습니다. 이러한 문제의 주요 장벽 중 하나는 프로그래밍과 검증 실습 간에 존재하는 환경 및 패러다임의 단절입니다.
이에 C*라는 증명 통합 언어 디자인이 제안되었습니다. C*는 C를 확장하여 검증 기능을 추가했으며, 심볼릭 실행 엔진과 LCF 스타일의 증명 커널을 기반으로 합니다. 이 언어는 프로그래머가 구현 코드 옆에 증명 코드를 할 수 있게 함으로써 실시간 검증이 가능하며, 현재의 증명 상태를 상호작용적으로 업데이트하는 것이 용이합니다. C*는 C를 공통 언어로 사용하여 구현과 증명 코드 개발을 통합한다는 특징이 있습니다.
C*의 프로토타입은 작은 규모의 C 프로그램 와 pKVM의 버디 할당자(buddy allocator)의 attach 함수 같은 복잡한 실제 사례 연구에 적용되어 평가되었습니다. 그 결과, C*가 광범위한 C 프로그래밍 관용구(idioms)를 검증할 수 있음을 입증했으며, 실세계 시나리오에서 복잡한 추론 작업을 효과적으로 처리하는 능력을 보여주었습니다.
용어 풀이
- 임베딩
- 글이나 이미지의 의미를 숫자 목록으로 바꾼 것. 의미가 비슷한 것을 찾을 때 써요.
- 벤치마크
- 모델 성능을 같은 조건에서 비교하려고 만든 시험 문제 모음.