State-inferer: LLM-Driven State Machine Extraction and Formal Verification for Secure Protocol Implementations
이 논문은 프로그램 슬라이싱, 대규모 언어 모델, 그리고 형식 모델 검증을 통합하여 소스 코드로부터 프로토콜 상태 머신을 정확하게 추출하고 검증하는 화이트박스 프레임워크인 State-inferer를 소개하며, 이를 통해 우수한 전이 수준 정확도를 달 achievement하고 TLS, IKEv2 및 SSH 구현에서 이전에 알려지지 않았던 4개의 보안 취약점을 발견하였다.
원본 논문은 CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기
디지털 세계의 보안은 컴퓨터가 서로 어떻게 통신하는지를 규정하는 보이지 않는 규칙들에 크게 의존하고 있습니다. 네트워크 프로토콜이라고 알려진 이 규칙들은 데이터가 송신자로부터 수신자에게 안전하게 전달되도록 보장하고, 신원을 확인하며, 비밀을 유지하도록 설계되었습니다. 그 핵심에서 이 프로토코들은 엄격한 대본처럼 작동합니다. 즉, 컴퓨터는 특정 상태에 있어야 하고, 특정 메시지를 받아야 하며, 그 후에 다음 단계로 진행하기 위해 새로운 상태로 이동해야 합니다. 만약 컴퓨터가 단계를 건너뛰거나 잘못된 상태에서 메시지를 수락한다면, 전체 시스템이 침해될 수 있으며 공격자가 보안 검사를 우회하거나 민감한 정보를 훔치는 것을 허용할 수 있습니다. 수십 년 동안 보안 전문가들은 서버에서 실행되는 실제 코드가 이 대본을 완벽하게 따르는지 검증하려고 노력해 왔습니다. 그러나 코드는 종종 복잡한 변수와 숨겨진 로직으로 가득 차 있어, 표준 테스트 도구들이 매핑하기 어려운 지저도 매우 무질서합니다. 프로그램의 실제 동작이 작성된 설계와 달라질 때, 위험한 결함이 눈에 띄지 않는 곳에 숨어 있다가 악용될 수 있습니다.
PLA 정보공학대학교의 연구팀은 이 문제를 해결하기 위해, 복잡한 컴퓨터 코드와 그 코드가 따라야 할 논리적 규칙 사이를 이어주는 번역기 역할을 하는 'State-inferer'라는 새로운 도구를 개발했습니다. 이 도구는 전체 코드베이스를 한꺼번에 읽으려 하거나 무작위 메시지를 보내 프로그램의 동작을 추측하는 대신, 코드를 작고 관리 가능한 조각들로 나눕니다. 이 도구는 '프로그램 슬라이싱(program slicing)'이라는 기술을 사용하여 특정 데이터 조각이 소프트웨어 내에서 어떻게 변화하는지를 추적함으로써, 컴퓨터가 한 상태에서 다른 상태로 전환하게 만드는 정확한 로직을 분리해 냅니다. 이 과정은 마치 엉킨 실타래 속에서 단 하나의 실을 따라가며 그 실이 정확히 어디로 이어지는지 확인하는 것과 같으며, 나머지 복잡한 부분들은 무시합니다. 이러한 특정 실들을 집중적으로 파고듦으로써, 시스템은 표준 도구들이 놓치기 쉬운 숨겨진 내부 조건들을 포함하여 프로그램이 따르는 정확한 사건의 순서를 재구성할 수 있습니다.
연구진은 이렇게 재구성된 시퀀스들을 코드에 대해 이해하고 추론하도록 훈련된 인공지능의 일종인 대규모 언어 모델(LLM)에 입력했습니다. 단순히 대량의 텍스트를 AI에게 읽게 했던 이전의 시도들과 달리, 이 시스템은 프로토콜의 매 전환(transition)마다 하나의 작고 집중된 코드 파편을 AI에게 제공했습니다. 이를 통해 AI는 불필요한 정보에 압도되지 않으면서도 상태 변화의 전체 맥락을 파악할 수 있었습니다. 그 후 AI는 프로그램의 동작에 대한 완전한 지도를 구축하였는데, 어떤 메시지가 변화를 유발했는지뿐만 아니라, 그 변화가 일어나기 위해 반드시 충족되어야 하는 내부 변수들까지 기록했습니다. 마지막으로, 연구진은 공식적인 보안 규칙에 이 지도를 대조하기 위해 형식 검증 엔진(formal verification engine)을 사용했습니다. 이 엔진은 엄격한 감사관처럼 작동하여, 프로그램이 취할 수 있는 모든 가능한 경로를 체계적으로 테스트함으로써, 예를 들어 보안 연결이 완전히 확립되기 전에 데이터를 전송하는 것과 같은 규칙 위반이 발생하는지 확인합니다.
TLS, IKEv2, SSH를 포함한 7가지의 주요 보안 프로토콜 오픈 소스 구현체에 대해 테스트했을 때, 이 새로운 방식은 놀라울 정도로 정확한 모습을 보였습니다. 이 방식은 95.2%의 정밀도로 코드의 동작을 정확히 식별해 냈으며, 이는 약 78.9%의 정확도를 보였던 기존의 가장 우수한 도구들을 크게 상회하는 수치입니다. 이 차이는 단순한 미세한 오류의 문제가 아니었습니다. 새로운 도구는 기존 방식들이 완전히 놓쳤던 복잡한 내부 로직, 예를 들어 외부 메시지가 아닌 내부 타이머나 리소스 체크에 의해 발생하는 전환 등을 성공적으로 포착해 냈습니다. 실제로 연구진은 기존 방식들이 프로그램의 단순화된 뷰에 의존하여 이러한 내부 세부 사항을 무시했기 때문에, 중요한 전환의 거의 절반을 보지 못하는 경우가 많다는 것을 발견했습니다. 전체 그림을 포착함으로써, 이 새로운 도구는 소프트웨어에서 이전에 발견되지 않았던 4개의 새로운 취약점을 찾아낼 수 있었습니다. 이 결함들은 이전에 발견된 적이 없는 심각한 수준이었으며, 공식 보안 식별 번호(CVE 등)가 부여되었고 소프트웨어 유지 관리자들에게 수정될 수 있도록 보고되었습니다.
가장 중요한 발견 중 하나는 이러한 결함들이 이론적인 가능성에 그치는 것이 아니라, 실제로 악용 가능한 약점이라는 점이었습니다. 한 사례에서는 서버가 필요한 키 교환을 마치기 전에 중요한 보안 메시지를 수락하도록 속일 수 있어, 사실상 인증을 우회할 수 있다는 점이 발견되었습니다. 또 다른 사례에서는 누락된 체크 기능으로 인해 서버가 끝없는 메시지 스트림을 처리하게 되어 잠재적으로 리소스를 고갈시킬 수 있음이 드러났습니다. 이러한 발견은 현재의 소프트웨어 분석 방식에 존재하는 결정적인 간극을 강조합니다. 즉, 입력과 출력만을 살펴보는 것으로는 프로그램이 실제로 어떻게 작동하는지 이해하기에 충분하지 않다는 것입니다. 연구진은 정밀한 코드 분석과 인공지능의 추론 능력을 결합함으로써, 프로그램의 내부 로직에 대한 완전하고 정확한 모델을 구축하는 것이 가능하다는 것을 입증했습니다. 이 접근 방식은 소프트웨어를 수정하거나 연구자가 모든 줄의 코드를 수동으로 추적할 필요가 없으므로, 우리 디지털 인프라를 보호하는 복잡한 시스템을 감사하기 위한 확장 가능한 방법을 제시합니다.
또한 이 연구는 텍스트 유사성을 기반으로 코드를 검색하는 기존 방식의 한계를 다루었습니다. 그러한 방식들은 프로그램의 상태를 변화시키는 데 함께 작동하는 서로 다른 함수들 사이의 연결 고리를 찾지 못해 실패하는 경우가 많았습니다. 반면, 이 새로운 시스템은 실제 데이터와 제어의 흐름을 따르기 때문에, 인공지능에게 제공되는 맥락이 완전하고 연결되어 있음을 보장합니다. 이를 통해 시스템은 일반적인 템플릿을 적용하여 목표를 놓치는 대신, 각 고유한 구현체의 변수와 로직에 특화된 보안 검사를 생성할 수 있었습니다. 그 결과, 다양한 코딩 스타일의 특성에 적응하면서도 시스템의 동작에 대한 신뢰할 수 있는 모델을 생성할 수 있는 프레임워크가 탄생했습니다.
궁극적으로, 이 작업은 소프트웨어 보안에 접근하는 방식의 변화를 의미합니다. 이는 모든 코드 줄을 수동으로 검사하거나 표면만을 볼 수 있는 블랙박스 테스트에 의존해야 한다는 생각에서 벗어나는 것입니다. 대신, 기계 내부를 들여다보고 기계가 정확히 어떻게 생각하고 반응하는지를 이해하는 길을 제시합니다. 연구진은 코드를 슬라이싱하고, 분석하고, 검증할 수 있는 논리적 단계들의 집합으로 취급함으로써, 수년간 숨어 있던 오류들을 찾아낼 수 있음을 발견했습니다. 이 도구는 오픈 소스 프로젝트를 대상으로 테스트되었지만, 이 방법론은 인터넷을 구동하는 방대한 양의 독점 시스템(proprietary systems)을 보호하기 위한 진로를 제시합니다. 복잡한 프로토콜의 상태 머신(state machines)을 자동으로 추출하고 검증할 수 있는 능력은 보안을 그 어느 때보다 철저하고 빠르게 점검할 수 있게 함으로써, 수십 년간 디지털 세계를 괴롭혀 온 침해 사고들을 예방할 수 있게 해줄 것입니다. 이번 연구 결과는 프로토콜이 수행해야 하는 바와 실제로 수행하는 것 사이의 간극에 위험이 존재하며, 그 간극을 메우기 위해서는 코드 자체에 대한 더 깊고 정밀한 관찰이 필요하다는 점을 확인시켜 줍니다.
연구 분야의 논문에 파묻히고 계신가요?
연구 키워드에 맞는 최신 논문의 일일 다이제스트를 받아보세요 — 기술 요약 포함, 당신의 언어로.