ETRI-Knowledge Sharing Plaform

KOREAN
기술이전 검색
Year ~ Transaction Count Keyword

Detail

User Interface Technology for a Formal-Methods-Based Automated TLS Software Verification Tool

Manager
Lim Jae Deok
Participants
Kim Jeong Nyeo, Lim Jae Deok, Choi Min Suk, Ha Su Jung
Transaction Count
2
Year
2025
Project Code
23HR8600, Development of security verification technology against vulnerability to assure IoT/IIoT device safety., Lim Jae Deok
24HS3500, Development of security verification technology against vulnerability to assure IoT/IIoT device safety., Lim Jae Deok
25HS1500, Development of security verification technology against vulnerability to assure IoT/IIoT device safety., Lim Jae Deok
- 본 기술이전은 IoT를 포함하는 다양한 네트워크 보호를 위해 사용되는 표준 규격 보안 프로토콜(RFC 5246(TLSv1.2) & RFC 8446(TLSv1.3)) 구현물(SW)에 대해 높은 수준의 신뢰도를 보장하는 보안 프로토콜 규격 검증(Conformance Test) 및 보안성 검증(Attack Testing)을 제공하는 “정형기법 기반 TLS SW 자동화 검증 도구 사용자 인터페이스 기술”에 대한 것이며, 크게 다음과 같은 두 개의 기술로 구성되어 있고 각 기술은 ETRI와 포스텍이 공동 개발하였음.
● 정형기법 기반 TLS SW 자동화 검증 도구 사용자 인터페이스 기술(ETRI)
.. 정형기법에 대한 사전 지식이 없더라도 정형기법 기반 검증을 수행할 수 있도록, 다양한 검증 환경 및 검증 항목의 설정, 정형기법 기반 검증 결과에 대해 직관적 파악이 가능하도록 하는 검증 결과 분석 및 시각화 기술을 제공함
● 정형기법 기반 TLS SW 자동화 검증 기술(포스텍)
.. 수학적 기법에 기반한 엄격한 검증을 제공하는 모델 검증(Model Checking) 기술을 활용하여, TLS v1.2 및 TLS v1.3 구현(SW)에 대한 표준 규격 검증 및 Dolev-Yao 공격 모델에 대한 보안성 검증 기능을 제공함
● 두 기술은 첨부된 자료에서 설명한 것과 같이 서로 연동이 되어야 완전한 도구 기능을 제공할 수 있으며, 각 기술을 개발한 기관에서 별도의 기술이전 절차로 추진함

- 본 이전기술은 정형기법 기반의 TLS SW 자동화 검증 도구 중 “정형기법 기반 TLS SW 자동화 검증 도구 사용자 인터페이스 기술”에 대한 것으로, 정형기법 기반의 검증이 높은 신뢰를 보장할 수 있지만, 수학적 모델과 논리적 추론을 사용함에 따라 관련 지식과 전문성이 없을 경우 적용하기 어려운 점을 감안하여, 정형기법 및 정형기법 기반 검증에 대한 지식이 없어도 용이하게 정형기법에 기반하여 구현된 TLS SW에 대한 표준 규격 정합성과 Dolev-Yao 공격 모델에 대응하는 보안성을 검증하고 검증 결과를 직관적으로 확인할 수 있는 사용자 인터페이스를 제공하는 기술임
- 본 이전기술은 IoT 등 네트워크 기반의 서비스 특히, 스마트교통, 스마트시티, 스마트팩토리 등 오류 발생가 발생되면 파급력이 큰 분야에, 신뢰할 수 있는 표준 규격의 네트워크 보안 프로토콜 운영 시 운영하려는 프로토콜 SW에 대해 규격 및 보안성 검증에 있어, 검증 범위 내에서 오류가 없다는 보장이 필요한 매우 높은 수준의 신뢰성을 보장하는 시험/검증 수행에 활용될 수 있음.
정형기법 기반의 TLS SW 자동화 검증 도구 중 “정형기법 기반TLS SW 자동화 검증 도구 사용자 인터페이스 기술”에 대한 것으로, 정형기법 기반의 검증이 높은 신뢰를 보장할 수 있지만, 수학적 모델과 논리적 추론을 사용함에따라 관련 지식과 전문성이 없을 경우 적용하기 어려운 점을 감안하여, 정형기법및 정형기법 기반 검증에 대한 지식이 없어도 용이하게 정형기법에 기반하여 구현된 TLS SW에 대한 표준 규격 정합성과 Dolev-Yao 공격 모델에 대응하는 보안성을검증하고 검증 결과를 직관적으로 확인할 수 있는 사용자 인터페이스를 제공하는기술임
- 본 이전기술인 “정형기법 기반 TLS SW 자동화 검증 도구 사용자 인터페이스 기술”에서 표준 규격 기반 네트워크 TLS SW SW 검증에 적용한 정형기법은 시스템의 설계, 개발(구현), 검증에 수학적 모델과 논리적 추론을 사용하여 오류와 결함을 체계적으로 검증하는 기법으로 검증 범위 내에서 오류가 없음을 보장할 수 있어 기존 테스팅 기법과 달리 높은 신뢰도를 제공하며, 본 이전기술은 정형기법에 대한 전문 지식이 없어도 네트워크 보안 프로토콜 SW의 표준 규격 정합성과 보안성 시험/검증을 높은 수준의 신뢰성을 제공하면서 수행할 수 있는 웹 기반의 인터페이스를 제공함

- 본 이전기술은 정형기법 기반의 검증의 범위가 대부분 설계 수준인 것을 SW 수준까지 확장한 모델 기반 테스팅 기법을 수행할 수 있는 웹 기반 자동화 인터페이스로서, 특히 모델 기반 테스팅에 대한 지식 없이도 검증하고자 하는 시험항목의 선택만으로 네트워크 보안 프로토콜 SW에 대한 표준 규격 정합성 및 보안성을 시험/검증할 수 있음
● 특히 SW 수준까지 정형기법 기반 검증 범위를 확장한 모델 기반 테스팅 기법은 국내 최초로 제공되는 기능이자, 해외에서도 보편적이지 않은 난이도가 높은 고급 기술로, 본 이전기술은 시험자는 해당 기법의 사용 여부를 인지하지 않으면서 해당 기법 기반의 검증을 수행할 수 있음

- 본 기술은 검증하려는 대상의 상태 및 검증 결과에 대한 직관적인 피드백을 위해 검증 결과를 분석하고 시각화하여 제공하는 기능을 제공함

- 본 기술은 정형기법 기반 TLS SW 자동화 검증 기술(포스텍)과 연동되어 완성된 도구로써 정상적인 기능을 수행하며, 본 기술이전 시 포스텍 기술도 같이 기술이전될 수 있도록 협의가 되어 있음
- 본 이전기술은 표준 규격(RFC 5246 & RFC8446) 기반 보안 프로토콜(TLS v1.2 & TLS v1.3)에 대해 구현 정합성과 네트워크 환경에서 발생할 수 있는 다양한 공격 모델(Dolev-Yao)에 대응하는 보안성 검증을, 정형기법에 대한 전문지식 없이도 정형기법 기반 검증을 용이하게 수행할 수 있도록 하는 “정형기법 기반 TLS SW 자동화 검증 도구 사용자 인터페이스 기술”임

- 본 이전기술은 사용자(시험자) 관점에서 정형기법 기반 검증 수행과 결과 확인을 용이하게 하기 위해 웹기반 시각화 인터페이스로 제공되며, 기능 및 운용 개념은 첨부파일 참조

- 사용자(시험자) 중심 웹 기반 시각화 인터페이스
- 정형기법 기반 RFC 5246(TLS v1.2) 규격 및 보안성 검증 설정 인터페이스
- 정형기법 기반 RFC 8446(TLS v1.3) 규격 및 보안성 검증 설정 인터페이스
- 정형기법 기반 RFC 5246(TLS v1.2) 규격 정합성 검증(Conformance Testing) 항목별 검증 결과 데이터 분석 및 시각화 (24종)
- 정형기법 기반 RFC 8446(TLS v1.3) 규격 정합성 검증(Conformance Testing) 항목별 검증 결과 데이터 분석 및 시각화 (44종)
- 정형기법 기반 Dolev-Yao 공격 모델에 대한 보안성 검증(Attack Testing) 시각화 (20종)
● Buffer Overflow & Dos 공격 항목 대응 검증 결과 분석 및 시각화(14종)
● Impersonation 공격 항목 대응 검증 결과 분석 및 시각화 (6종)
- 정형기법 기반 검증 결과 통합 로그 관리
- 프로그램(소스코드)
- 요구사항 및 요구사항 시험문서
- 사용자 매뉴얼
IoT 등 네트워크 기반의 서비스 특히, 스마트교통, 스마트시티,스마트팩토리 등 오류 발생가 발생되면 파급력이 큰 분야에, 신뢰할 수 있는 표준규격의 네트워크 보안 프로토콜 운영 시 운영하려는 프로토콜 SW에 대해 규격 및보안성 검증에 있어, 검증 범위 내에서 오류가 없다는 보장이 필요한 매우 높은 수준의 신뢰성을 보장하는 시험/검증 수행에 활용될 수 있음.