FSR: 안전한 인터도메인 라우팅을 위한 형식 분석 및 구현 툴킷
Source
Evernote/Papers/FSR Formal Analysis and Implementation Toolkit for Safe Interdomain Routing.md
Summary
본 논문은 인터넷의 안정성을 위해 인터도메인 라우팅 정책의 형식적 분석과 구현을 통합하는 ‘Formally Safe Routing (FSR)’ 툴킷을 제안합니다. FSR은 라우팅 대수(Routing Algebra)를 공통 표현 방식으로 사용하여, 이를 SMT 솔버를 위한 정수 제약 조건으로 변환해 안전성 분석을 수행하거나, 분산 구현을 위한 선언형 프로그램으로 생성합니다. 실제 토폴로지와 정책을 대상으로 한 실험을 통해 AS 내 iBGP 구성 오류 탐지, BGP 안전성 충분 조건 증명, 수렴 시간 평가 등의 효과를 입증했습니다.
Key Points
- 라우팅 대수(Routing Algebra)를 기반으로 라우팅 정책의 안전성 분석과 구현을 통합 처리
- SMT 솔버를 활용한 정형 안전성 분석 및 선언형 프로그램 기반 분산 구현 자동 생성
- iBGP 구성 오류 탐지, BGP 안전성 증명, 수렴 시간 평가 등 실제 네트워크 환경에서의 유효성 검증