Certora, 스마트 계약 보안 검증을 위한 AI 도구 출시

Certora는 목요일 AI Composer의 출시를 발표했습니다. 이는 스마트 계약을 위한 인공지능 코드 생성에 형식 검증을 내장한 오픈소스 플랫폼으로, AI가 생성한 코드의 보안 취약점에 대한 우려가 높아지고 있는 상황에 대응합니다.

텔아비브에 본사를 둔 이 보안 회사의 새로운 도구는 실행 전에 모든 코드 스니펫이 안전 요구사항을 충족하는지 수학적으로 검증함으로써 기존의 AI 코딩 보조 도구와 차별화됩니다. 이 플랫폼은 Aave, Lido, Uniswap을 포함한 주요 탈중앙화 금융 프로토콜에서 이미 사용 중인 Certora의 Prover 기술을 AI 생성 루프에 직접 통합합니다.

AI 생성 코드의 보안 우려 증가

이러한 시기는 AI 생성 코드의 보안 위험에 대한 증거가 증가하고 있음을 반영합니다. 100개 이상의 대규모 언어 모델을 분석한 2025년 Veracode 연구에 따르면, AI 생성 코드의 45%가 보안 취약점을 야기하며, 코드 생성 정확도의 발전에도 불구하고 보안 실패율은 정체 상태를 유지하고 있습니다. 연구 결과 AI 모델은 안전한 대안이 제시되었을 때 45%의 경우 안전하지 않은 코딩 방법을 선택했습니다.

스마트 컨트랙트 보안은 여전히 중요하며, OWASP 스마트 컨트랙트 상위 10에 따르면 2024년에 접근 제어 취약점만으로 9억 5,300만 달러의 손실이 발생했습니다. Certora의 창립자이자 수석 과학자인 Mooly Sagiv는 “AI를 사용한다고 해서 안전을 타협해서는 안 됩니다”라고 말했습니다. “Certora AI Composer는 AI와 형식 검증이 함께 작동하여 스마트 컨트랙트 개발을 기본적으로 신뢰할 수 있게 만들 수 있음을 증명합니다”.

오픈 소스 출시 및 산업 영향

알파 버전은 12월 4일부터 GitHub에서 이용 가능하게 되며, 이날 Certora는 “AI Meets Verification: An Open Discussion with Certora Researchers”라는 제목의 라이브스트림을 개최할 예정입니다. 이 플랫폼은 통합된 형식 검증 검사, 맞춤형 안전 모듈을 위한 오픈소스 확장성, 그리고 Web3 프로토콜 전반에 걸쳐 1,000억 달러 이상의 총 예치 가치를 보호해 온 Certora Prover의 지원을 특징으로 합니다.

형식 검증은 규제 기관들이 그 중요성을 인식하면서 주목을 받고 있습니다. 프랑스 금융 규제 당국은 2025년 스마트 계약 인증을 위한 이 기술을 승인하며, 다른 분석 방법에 비해 “코드의 무결성에 관해 더 높은 수준의 보증을 제공한다”고 언급했습니다. 미국 사이버 보안국장 역시 2024년에 형식 방법론을 “국가 소프트웨어 보안에 필수불가결한 것”으로 규정했습니다.