LLMs are making formal software verification feasible at a much larger scale
거대 언어 모델(LLM)이 대규모 형식 검증을 실현 가능하게 만들고 있습니다. Anthropic과 Theorem의 협업을 통해 LLM이 이제 실제 소프트웨어에 대한 형식 증명을 자율적으로 생성할 수 있게 되었으며, 이는 보안 보장이 포함된 새로운 소프트웨어 개발 워크플로우를 가능하게 합니다. 이들은 Claude를 사용하여 100개 이상의 오픈 소스 라이브러리에 걸쳐 어셈블리 코드 수준(RISC-V)에서 보안 속성을 증명하는 데 성공했으며, 이 과정에서 수년간 탐지되지 않았던 버그들을 발견하기도 했습니다.
형식 검증은 코드를 수학적 모델로 변환하여 정의된 보안 규칙을 항상 준수하는지 증명하는 방법으로, 과거에는 seL4 운영체제 커널 검증에 수년이 걸릴 정도로 많은 노력이 필요했습니다. 하지만 LLM은 이러한 증명 과정을 훨씬 쉽게 만들었으며, 이는 소프트웨어의 보안을 보장하는 데 있어 이전보다 훨씬 넓은 범위와 규모를 달성하게 합니다. 이는 개발자들이 코드의 보안 속성을 검증하고 재사용할 수 있는 기반을 마련해 줍니다.
이러한 접근 방식은 소프트웨어 버그를 줄이고 보안을 강화하는 데 중요한 진전을 가져오지만 몇 가지 한계점도 존재합니다. LLM이 생성한 증명은 아직 모든 잠재적 버그를 해결하지 못하며, 하드웨어, 운영체제, 컴파일러에 대한 신뢰가 필요하다는 점을 고려해야 합니다. 또한, AI 모델이 의도하지 않은 결과를 도출하는 '보상 해킹(reward hacking)'과 같은 위험이 있으므로, 생성된 증명을 검증하고 재사용하는 과정에서 신중한 접근이 필요합니다.
형식 검증은 코드를 수학적 모델로 변환하여 정의된 보안 규칙을 항상 준수하는지 증명하는 방법으로, 과거에는 seL4 운영체제 커널 검증에 수년이 걸릴 정도로 많은 노력이 필요했습니다. 하지만 LLM은 이러한 증명 과정을 훨씬 쉽게 만들었으며, 이는 소프트웨어의 보안을 보장하는 데 있어 이전보다 훨씬 넓은 범위와 규모를 달성하게 합니다. 이는 개발자들이 코드의 보안 속성을 검증하고 재사용할 수 있는 기반을 마련해 줍니다.
이러한 접근 방식은 소프트웨어 버그를 줄이고 보안을 강화하는 데 중요한 진전을 가져오지만 몇 가지 한계점도 존재합니다. LLM이 생성한 증명은 아직 모든 잠재적 버그를 해결하지 못하며, 하드웨어, 운영체제, 컴파일러에 대한 신뢰가 필요하다는 점을 고려해야 합니다. 또한, AI 모델이 의도하지 않은 결과를 도출하는 '보상 해킹(reward hacking)'과 같은 위험이 있으므로, 생성된 증명을 검증하고 재사용하는 과정에서 신중한 접근이 필요합니다.