더 적은 노력, 더 짧은 증명: Tamarin의 보안 프로토콜 분석을 위한 강화학습 (RL)

Tamarin 및 ProVerif와 같은 도구들은 EMV, 5G, WPA2와 같은 복잡한 실세계 프로토콜을 분석하고 검증하는 데 있어 주목할 만한 성공을 거두었으며, 제로데이 취약점 (zero-day exploits)을 탐지하기도 했습니다. 이러한 성공에도 불구하고, 해당 프로토콜들을 검증하는 것은 여전히 많은 시간과 노력이 소요되는 어려운 과제이며, 종종 상당한 인간의 노력과 전문 지식을 필요로 합니다. 본 논문에서는 AlphaZero 및 AlphaProof에서 영감을 얻어 Tamarin을 위한 새로운 방식의 증명 탐색 (proof search)을 구현하는 강화학습 (Reinforcement Learning, RL) 프레임워크를 제시합니다. 우리는 고전적인 RL 환경 역할을 하는 Tamarin용 상태 비저장 API (stateless API)를 개발했습니다. 우리는 완료된 하위 증명 (subproofs)으로부터 학습하는 신경망 휴리스틱 (neural heuristic)을 통해 몬테카를로 트리 탐색 (Monte Carlo Tree Search, MCTS)을 유도합니다. 우리는 고전적인 프로토콜 모델부터 최근 출판된 도전적인 최첨단 (state-of-the-art) 프로토콜 모델에 이르기까지 16개의 사례 연구를 통해 우리의 프레임워크를 평가합니다. 우리의 방법은 Tamarin의 표준 탐색보다 더 많은 증명을 자동으로 찾아내며, 표준 휴리스틱 및 인간이 설계한 휴리스틱보다 더 짧은 증명을 생성합니다. 우리의 파이프라인은 즉시 적용 가능하여 활발한 연구를 수행하는 Tamarin 사용자들을 보조하고 필요한 인간의 노력을 줄여줍니다. 또한, 우리의 표준화된 인터페이스는 사용자가 Tamarin과 상호작용할 수 있는 프로그래밍 방식 (programmatic way)을 제공합니다. 마지막으로, 우리의 연구는 RL 기반 방법론을 Tamarin 도메인에 적응시키는 것의 유망한 잠재력을 입증합니다.