- 국내 최초, 정형기법 기반의 IoT 보안 프로토콜 기술 개발 나서

- 설계부터 구현까지 정형검증 적용, 높은 신뢰도 보증

ETRI, 포항공대, 국민대학교가 협력하여 정형기법 기반의 IoT 보안 프로토콜 기술 'HASP'를 개발 중이다. 이 기술은 설계부터 코드 구현까지 보안성을 검증하여 IoT 서비스의 신뢰성을 높일 것으로 기대된다.

▲ETRI 연구진이 정형검증 기반의 고신뢰 IoT 보안 프로토콜 기술 검증을 테스트하는 모습 (출처=ETRI)

국내 연구진이 안전하고 신뢰성있는 IoT 서비스를 위한 보안 프로토콜 기술 개발에 나섰다. 통신 시스템, 재난 안전 통신망, 항공기 운항 관제 시스템 등 높은 신뢰성을 요구하는 IoT 서비스에서의 신뢰성있고 안정적인 운용에 크게 기여할 것으로 기대되고 있다.

한국전자통신연구원은 포항공대, 국민대학교와 협력하여 국내 최초로 정형기법(Formal Method) 기반의 IoT 보안 프로토콜 기술을 개발 중이라고 밝혔다. 

정형기법을 적용한 보안성 검증(이하 정형검증)은 시스템 설계 단계에서부터 오류나 보안 취약점을 엄격하게 검증할 수 있는 기술이다. 기존 보안성 검증은 이미 개발된 SW를 대상으로 진행되는 데 반해, 정형검증은 설계 단계에서부터 보안성을 확인할 수 있어 시스템 내 오류 발생 가능성을 최소화할 수 있다.

ETRI 연구진은 정형기법을 코드 수준으로 확장하여, 정형검증 기반의 TLS 솔루션인 ‘HASP’를 개발 중이다. 특히, 이번에 개발 중인 HASP는 요구사항 정의와 설계 단계부터 엄격한 보안성 검증을 수반하는 모델 검증(Model-Checking)을 적용했다. 이를 통해 검증된 범위 내에서 시스템 오류와 보안 취약점이 없음을 보장할 수 있는 높은 수준의 검증 결과를 제공한다.

더불어, 연구진은 정형검증의 범위를 기존 설계 단계에서 SW 개발(코드 구현) 단계까지 확장하였다. 모델 기반 테스팅(Model-based Testing) 기법을 통해 설계와 구현 단계에서의 불일치 가능성을 사전에 제거하고, 구현된 코드에 대한 오류나 보안 위협이 없음을 높은 신뢰도로 보장할 수 있다.

본 기술은 기존의 정형검증이 주로 설계 단계까지만 적용되던 것과 달리, 실제 동작하는 SW 단계까지 정형기법을 적용한 국내 첫 사례이다. 본 기술이 IoT 및 미션 크리티컬 시스템에 적용될 경우, 기존 정형검증 기술 대비 높은 신뢰도를 제공할 수 있을 것으로 전망된다.

▲정형검증 기반 고신뢰 보안 프로토콜 및 검증 자동화 기술 개요

▲정형기법 기반 보안 프로토콜 자동화 검증 도구 개요

또한, 연구진은 이미 표준으로 적용, 규격화되어 있는 TLS 보안 프로토콜의 다양한 솔루션에 대해 정형검증 기법을 용이하게 적용할 수 있도록, 사용자 중심의 자동화된 검증 도구도 개발 중이다.

연구진은 올해 11월까지 정형기법 기반의 자동화 검증 도구 프로토타입 개발을 완료하고, 자체 개발된 TLS v1.2 솔루션에 적용하여 높은 수준의 신뢰도를 보장하는 HASP v1.0 개발을 완료할 예정이다. 이와 함꼐 올해 12월부터는 관련 업체와 기술이전을 추진할 예정이다.

향후 연구진은 정형검증 기반 자동화 검증 도구의 검증 범위를 확장하고 기능 안정화와 성능 개선 등 기술의 완성도 제고를 추진할 예정이다. 또한, 이를 수요기업인 LG U+의 5G 이동 통신망 테스트베드에 실증 적용하여, 기술의 상용화 가능성을 검증할 예정이다.

국제표준(ISO/IEC 29128:2011)에서는 암호 프로토콜의 보안성 검증에 대해 보증 수준을 4단계로 구분하고 있으며, 이번에 개발 중인 HASP 솔루션은 국제표준 규격 기준 3단계에 해당한다. 또한, 국민대에서는 ETRI와 함께 4단계 검증 기술을 확보하기 위해 정형기법 기반의 다양한 검증 도구를 활용한 연구를 진행 중이다.

ETRI 연구진이 개발하는 정형기법 기반 검증 기술과 HASP 솔루션은 글로벌 IoT 보안 기술 시장에서 국내 IoT 보안 기술의 산업 경쟁력을 높이는 데 큰 기여를 할 것으로 기대하고 있다.

이번 기술 개발 분야를 총괄하는 ETRI 사이버보안연구본부 임재덕 책임연구원은 “정형기법을 활용한 이번 연구는 IoT 서비스의 보안성과 신뢰성을 기존보다 한층 더 보장할 수 있는 중요한 기술적 토대를 제공할 것이다. 향후 국내 IoT 보안 시장의 경쟁력 제고와 사고 발생 시 파급효과가 큰 미션 크리티컬 서비스의 신뢰도를 높일 수 있는 토대를 마련하도록 노력하겠다”고 말했다.

본 연구는 과학기술정보통신부와 정보통신기획평가원(IITP)이 지원하는 ‘정보보호핵심원천기술개발사업’의 일환으로 진행되었다. ‘IoT/IIoT 디바이스 안전성 보장을 위한 취약점 보안검증 기술 개발’(주관: 라온시큐리티(대표 양정규)) 과제를 통해 2025년까지 ETRI, 포항공대, 국민대, 한국정보통신기술협회(TTA), LG U+ 등과 공동으로 수행할 예정이다. 

<용어설명>

1) 정형기법(Formal Method) : 소프트웨어와 시스템의 설계, 개발, 검증에 수학적 모델과 논리적 추론을 사용하여 오류와 결함을 체계적으로 검증하는 기법. 크게 모델검증(Model Checking)과 정리증명(Theorem Proving)으로 구분됨.

2) TLS(Transport Layer Security) : 인터넷에서의 정보를 암호화하여, 개인 정보와 데이터 보안을 용이하게 하기 위해 설계된 보안 프로토콜

3) HASP(High Assurance Device Authentication and Secure Protocol System) : 정형기법 검증이 적용된 고신뢰 TLS 보안프로토콜 시스템

4) 모델 검증(Model-Checking) : 시스템의 상태와 동작을 수학적 모델로 표현한 후, 이 모델을 자동으로 탐색하여 시스템이 특정 요구사항을 만족하는지, 오류가 없는지를 검증하는 기법

5) 모델 기반 테스팅(Model-based Testing) : 시스템의 동작을 모델로 표현한 후, 이 모델을 기반으로 테스트 케이스를 자동으로 생성하고 실행하여 시스템의 동작을 검증하는 방법

6) 미션 크리티컬 시스템(Mission Critical System) : 악의적으로 이용되거나 정상적인 동작을 하지 않을 경우, 해당 시스템이 개입된 서비스 전체에 치명적인 영향을 미쳐 사회나 조직에 혼란 등을 줄 수 있는 시스템으로, 스마트교통, 스마트팩토리, 스마트에너지 등의 인프라에 사용되는 시스템 및 디바이스 등이 될 수 있음