한국전자통신연구원이 포항공대, 국민대학교와 협력해 정형기법(Formal Method) 기반의 사물인터넷(IoT) 보안 프로토콜 기술 개발을 추진한다. 정형기법을 적용한 보안성 검증은 시스템 설계 단계에서부터 오류나 보안 취약점을 엄격하게 검증해 서비스 신뢰성을 보장하는 기술이다.

기존 보안성 검증이 이미 개발된 소프트웨어(SW)를 대상으로 진행되는 반면, 정형검증은 설계 단계에서부터 보안성을 확인할 수 있어 시스템 내 오류 발생 가능성을 최소화할 수 있다는 게 ETRI의 설명이다. 

ETRI는 정형기법을 코드 수준으로 확장해 정형검증 기반의 TLS 솔루션 ‘HASP’를 개발하고 있다. HASP는 요구사항 정의와 설계 단계부터 엄격한 보안성 검증을 수반하는 모델 검증을 적용해 개발될 예정이다.

이를 통해 검증된 범위 내에서 시스템 오류와 보안 취약점이 없음을 보장할 수 있는 높은 수준의 검증 결과를 제공할 수 있다.

국제표준(ISO/IEC 29128:2011)에서는 암호 프로토콜의 보안성 검증에 대해 보증 수준을 4단계로 구분한다. 이번에 개발 중인 HASP 솔루션은 국제표준 규격 기준 3단계에 해당한다.

국민대는 ETRI와 함께 4단계 검증 기술을 확보하기 위해 정형기법 기반의 다양한 검증 도구를 활용한 연구를 진행하고 있다.

ETRI는 향후 정형검증의 범위를 기존 설계 단계에서 개발(코드 구현) 단계까지 확장해 신뢰성을 강화할 방침이다. 모델 기반 테스팅 기법으로 설계와 구현 단계에서의 불일치 가능성을 사전에 제거하고, 구현된 코드에 대한 오류나 보안 위협이 없음을 높은 신뢰도로 보장하기 위함이다. 

ETRI는 “소프트웨어 단계까지 정형기법을 적용한 IoT, 미션 크리티컬 시스템은 한층 더 높은 신뢰도를 갖게 될 것”이라고 기대하며 “TLS 보안 프로토콜의 다양한 솔루션에 대해 정형검증 기법을 용이하게 적용할 수 있도록 사용자 중심의 자동화된 검증 도구도 추후 개발할 방침”이라고 전했다. 

ETRI는 내달까지 정형기법 기반의 자동화 검증 도구의 프로토타입 개발을 완료하고, 자체 개발된 TLS v1.2 솔루션에 적용해 높은 수준의 신뢰도를 보장하는 HASP v1.0 개발을 완료할 예정이다.

개발 완료 후에는 LG U+의 5G 이동 통신망 테스트베드에 실증 적용하고, 관련 업체와 기술이전을 추진해 IoT 서비스 활성화에 기여할 계획이다. 

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