정형기법, 수학적 논리 표현 빌려 시스템 모델링
통신 프로토콜(TLS)에 적용, 검증 완성도 높여
[녹색경제신문 = 우연주 기자] IoT(사물인터넷) 서비스의 신뢰도를 높이기 위한 신기술 개발이 한창 진행 중이다. 수학적 표현법의 무결성을 활용해 TLS(인터넷 보안 프로토콜의 일종)의 신뢰도를 높이겠다는 계획이다.
ETRI(한국전자통신연구원) 관계자는 "수학적 증명을 통해 모델이 기능/보안 요구사항을 만족하는지 엄밀히 검증할 수 있다. 결과적으로 높은 수준의 신뢰성을 제공하기 때문에 정형기법이 사용된다"고 설명했다.
해당 기술 개발을 위헤 ETRI는 포항공대, 국민대학교와 협력하고 있다고 밝혔다. 정형기법을 적용한 보안성 검증(이하 정형검증)은 시스템 설계 단계에서부터 오류나 보안 취약점을 엄격하게 검증할 수 있는 기술이다.
ETRI 연구진은 정형기법을 코드 수준으로 확장하여, 정형검증 기반의 TLS 솔루션인 ‘HASP’를 개발 중이다.
이번에 개발 중인 HASP는 요구사항 정의와 설계 단계부터 엄격한 보안성 검증을 수반하는 모델 검증(Model-Checking)을 적용했다.
이를 통해 검증된 범위 내에서 시스템 오류와 보안 취약점이 없음을 보장할 수 있는 높은 수준의 검증 결과를 제공한다.
연구진은 정형검증의 범위를 기존 설계 단계에서 SW 개발(코드 구현) 단계까지 확장했다.
모델 기반 테스팅(Model-based Testing) 기법을 통해 설계와 구현 단계에서의 불일치 가능성을 사전에 제거하고, 구현된 코드에 대한 오류나 보안 위협이 없음을 높은 신뢰도로 보장할 수 있다.
본 기술은 기존의 정형검증이 주로 설계 단계까지만 적용되던 것과 달리, 실제 동작하는 SW 단계까지 정형기법을 적용한 국내 첫 사례이다.
이 기술이 IoT 및 미션 크리티컬 시스템에 적용될 경우, 기존 정형검증 기술 대비 높은 신뢰도를 제공할 수 있을 것이라는 전망도 나온다.
연구진은 이미 표준으로 적용, 규격화되어 있는 TLS 보안 프로토콜의 다양한 솔루션에 대해 정형검증 기법을 용이하게 적용할 수 있도록, 사용자 중심의 자동화된 검증 도구도 개발 중이다.
연구진은 올해 11월까지 정형기법 기반의 자동화 검증 도구 프로토타입 개발을 완료하고, 자체 개발된 TLS v1.2 솔루션에 적용하여 높은 수준의 신뢰도를 보장하는 HASP v1.0 개발을 완료할 예정이다.
이와 함꼐 올해 12월부터는 관련 업체와 기술이전을 추진할 예정이다.
LG유플러스도 현재 수요기관으로 참여 중이다.
기술개발이 완료되면 외부에 공개되지만 LG유플러스가 개발 과정에서 실증에 참여하는 만큼 기술에 대한 접근성과 이해도가 높아질 것이라는 추측도 가능하다.
LG유플러스는 현재 스마트철도 사업에 참여 중인 것을 비롯, IoT 기술 저변 확대에 힘쓰는 모양새다.
지난해 9월 KT의 가입자 수를 앞지른 것도 LG유플러스의 IoT 회선 수가 포함된 것이 원인인 만큼 LG유플러스의 IoT 행보에 관심이 쏠린다.
우연주 기자 lycaon@greened.kr