한국전자통신연구원(ETRI)이 포항공대, 국민대와 공동연구로 국내 최초 정형기법(Formal Method) 기반 IoT 보안 프로토콜 기술을 개발한다.
이를 통해 통신시스템, 재난안전 통신망, 항공기 운항관제 등 높은 신뢰성을 요구하는 IoT 서비스가 획기적으로 개선될 전망이다.
10일 ETRI에 따르면 정형기법을 적용한 보안성 검증은 시스템 설계단계부터 오류나 보안 취약점을 엄격하게 검증할 수 있는 기술이다.
기존 보안성 검증은 개발 완성된 소프트웨어(SW)를 대상으로 진행하지만, 정형검증은 설계단계부터 보안성을 확인할 수 있어 시스템 오류 가능성을 최소화할 수 있다.
이에 따라 ETRI 연구진은 정형기법을 코드 수준으로 확장, 정형검증 기반 TLS 솔루션 ‘HASP’를 개발 중이다. TLS(Transport Layer Security)는 인터넷에서 정보를 암호화해 개인정보와 데이터 보안을 용이하게 만드는 보안 프로토콜이며, HASP(High Assurance Device Authentication and Secure Protocol System)는 정형기법 검증이 적용된 고신뢰 TLS 보안프로토콜 시스템이다.
ETRI가 개발 중인 HASP는 요구사항 정의 및 설계 단계부터 엄격한 보안성 검증을 수반하는 모델검증을 적용한 것이 특징이다.
이는 검증된 범위 내에서 시스템 오류와 보안 취약점이 없음을 보장할 수 있는 높은 수준의 검증 결과를 제공한다.
아울러 연구진은 정형검증의 범위를 기존 설계 단계에서 SW 개발 단계까지 확장했다. 이를 위해 모델 기반 테스팅 기법을 적용, 설계와 구현 단계에서의 불일치 가능성을 사전 제거하고 구현한 코드에 대한 오류나 보안 위협이 없음을 높은 신뢰도로 보장할 수 있게 됐다.
이 기술은 기존 정형검증이 설계 단계까지 적용되던 것과 달리 실제 동작하는 SW 단계에도 적용한 국내 첫 사례로, IoT 및 미션 크리티컬 시스템에 적용될 경우 기존 정형검증 기술 대비 높은 신뢰도를 제공할 전망이다.
또 연구진은 이미 표준 규격화된 TLS 보안 프로토콜의 다양한 솔루션에도 정형검증 기법을 용이하게 적용할 수 있도록 사용자 중심 자동 검증도구를 내달까지 프로토타입 개발을 완료하고, 자체 개발한 TLS v1.2 솔루션에 적용해 높은 신뢰도를 보장하는 HASP v1.0을 개발해 연말부터 기술이전을 추진한다.
아울러 향후 정형검증 기반 자동화검증 도구의 검증 범위를 확장하고 기능 안정화와 성능개선 등 기술완성도를 높여 수요기업인 LGU+의 5G 이동통신망 테스트베드에 적용할 예정이다.
ETRI는 이번에 개발한 정형기법 기반 검증기술과 HASP 솔루션이 글로벌 IoT 보안기술 시장에서 국내 IoT 보안기술의 산업 경쟁력을 높이는 데 큰 기여를 할 것으로 기대하고 있다.
임재덕 ETRI 사이버보안연구본부 책임연구원은 “정형기법을 활용한 이번 연구는 IoT 서비스 보안성과 신뢰성을 기존보다 한층 더 강화하는 중요한 기술적 토대를 제공할 것”이라고 말했다.
