포항공대·국민대와 협력, 설계부터 구현까지 정형검증
정형기법을 적용한 보안성 검증(정형검증)은 시스템 설계단계에서부터 오류나 보안 취약점을 엄격하게 검증할 수 있는 기술이다. 기존 보안성 검증은 개발된 SW를 대상으로 진행되지만 정형검증은 설계단계에서부터 보안성을 확인할 수 있어 시스템 내 오류 발생을 최소화할 수 있다.
ETRI 연구진이 개발에 나선 정형검증 기반의 TLS 솔루션은 정형기법을 코드수준으로 확장한 'HASP'다.
TLS(Transport Layer Security)는 인터넷에서 정보를 암호화해 개인정보와 데이터 보안을 용이하게 하기 위해 설계된 보안 프로토콜이고 HASP(High Assurance Device Authentication and Secure Protocol System)는 정형기법 검증이 적용된 고신뢰 TLS 보안프로토콜 시스템을 말한다.
이번에 개발 중인 HASP는 요구사항 정의와 설계단계부터 엄격한 보안성 검증을 수반하는 모델검증(Model-Checking)이 적용됐다. 이를 통해 검증된 범위 내에서 시스템 오류와 보안 취약점이 없음을 보장할 수 있는 높은 수준의 검증 결과를 제공할 수 있다.
또 연구진은 정형검증의 범위를 기존 설계단계에서 SW 개발(코드 구현)단계까지 확장해 설계와 구현단계에서의 불일치 가능성을 사전에 제거하고 구현된 코드에 대한 오류나 보안위협이 없음을 높은 신뢰도로 보장할도록 할 방침이다.
이와 함께 이미 표준으로 적용, 규격화돼 있는 TLS 보안 프로토콜의 다양한 솔루션에 대해 정형검증 기법을 용이하게 적용할 수 있도록 사용자 중심의 자동화된 검증도구도 개발 중이다.
연구진은 다음달까지 정형기법 기반의 자동화 검증도구 프로토타입 개발을 완료하고 자체 개발한 TLS v1.2 솔루션에 적용, 높은 수준의 신뢰도를 갖는 HASP v1.0 개발을 완료한다는 방침이다. 이어 12월부터는 관련 업체와 기술이전을 추진한다.
ETRI 사이버보안연구본부 임재덕 책임연구원은 "정형기법을 활용한 이번 연구는 IoT 서비스의 보안성과 신뢰성을 기존보다 한층 더 보장할 수 있는 중요한 기술적 토대를 제공할 것"이라며 "향후 국내 IoT 보안 시장의 경쟁력 제고와 사고발생 시 파급효과가 큰 미션 크리티컬 서비스의 신뢰도를 높일 수 있도록 노력하겠다"고 말했다.
◎공감언론 뉴시스 kys0505@newsis.com