Development of Vericoding Techniques for Formally Verifying the Correctness of C-to-Rust Pointer Translation Using LLM Agents
개인기초연구(과기정통부)(R&D) · 우수연구-핵심연구(기본연구B)
2026년
2710111712
과학기술정보통신부
한국연구재단
울산과학기술원
홍재민
2명
2026.09.01 ~ 2027.08.31
2026.09.01 ~ 2028.08.31
6,396만원
6,396만원
기초연구
대학
울산광역시 울주군
정보/통신 > 정보이론 > 프로그래밍 언어/자연어 처리
본 과제의 최종 목표는 LLM 에이전트를 통해 C 코드의 포인터 사용을 메모리 안전성이 보장되는 러스트 코드로 번역하고, 그 올바름을 정형 검증으로 보장하는 베리코딩 기반 C-러스트 번역 검증 기술을 개발하는 것이다. 이를 위해 본 과제는 ① C 코드의 포인터 사용 정보를 정적 분석으로 추출하고, ② LLM이 이를 활용해 번역 전후 코드의 정형 명세와 증명...
최종 목표 달성을 위해 연구과제는 2년에 걸쳐 진행하며, 1차년도에는 올바름의 기준이 되는 번역 전 코드의 정형 명세 생성에 주력하고, 2차년도에는 번역 생성 및 명세에 기반한 번역의 올바름 증명에 집중한다. 검증 프레임워크로는 Rocq 기반의 RefinedRust를 사용하며, 포인터 사용을 변환하는 데 집중할 수 있도록, 평가에는 VERT 및 TRACTO...
... 레거시 시스템을 메모리 안전성이 보장되는 러스트로 전환하는 데 활용될 수 있다. 특히, 안전·보안이 중요한 시스템 소프트웨어의 포인터 번역 결과를 정형 검증함으로써, 산업 현장의 코드 현대화와 ... 올바름까지 검증하는 기술을 제공함으로써, AI 기반 취약점 탐색과 방치된 시스템 취약점 악용 등 고도화되는 사이버보안 위협을 줄이고 신뢰 가능한 디지털 사회 기반을 강화하는 데 기여한다.