- 본 기술은 IoT 서비스의 네트워크 보안을 위해 사용되는 표준 규격 보안 프로토콜(RFC 5246(TLS v1.2), RFC 8446(TLS v1.3)) 구현 기술로, 높은 수준의 신뢰도를 요구하는 미션 크리티컬 서비스에 활용할 수 있도록 정형기법 기반의 보안 프로토콜 규격 검증(Conformance Test) 및 보안성 검증(Attack Testing)을 적용한 “IoT용 고신뢰 보장 네트워크 보안프로토콜(HASP) 기술”임
- 본 이전기술에 적용된 정형기법 검증은 이론적으로 검증 범위 내에서 오류가 없음을 보장할 수 있는 유일한 검증 기법으로, 검증 범위에 대해 설계되지 않은 행위 즉, 의도하지 않은 행위가 발생하지 않는다는 높은 신뢰도를 제공하지만, 수학적 모델과 논리적 추론에 기반함에 따라 정형 기법 관련 지식과 전문성이 없을 경우 적용하기 어려운 점을 단점을 가지고 있음.
- 본 이전기술은 Maude 모델 검증 도구을 이용하여 설계서 명세(specification) 검증 및 모델 기반 테스팅(Model-based Testing) 기법을 적용하여, 설계 단계부터 구현(SW)에 이르기까지 정형기법 기반의 검증을 적용한 TLS 보안 프로토콜 기술이며, RFC 5246 및 RFC 8446 표준에 대한 규격 정합성과 Dolev-Yao 공격 모델에 대응하는 보안성을 검증을 진행하였음.
IoT 등 네트워크 기반의 서비스 특히, 스마트교통, 스마트시티,
스마트팩토리 등 보안 사고 및 오류 문제가 발생하면 파급력이 큰 분야에,
높은 수준의 신뢰성을 보장하는 표준 규격 보안 프로토콜 솔루션으로
활용함으로써, 보안사고 발생 시 국가 및 사회에 재앙 수준의 피해가
예상되는 미션 크리티컬 분야의 IoT/IIoT 서비스 활성화에 기여하고자 함
- 수학적 모델 및 논리적 추론 기반의 정형기법을 활용한 시스템 설계 및 개발(구현) 검증 수행
.. 검증 범위 내 오동작 및 보안취약점 없음 보장 가능
- 상태 모델 기반 시스템 설계를 통한 정형 기법 기반 설계 검증 수행
.. Designed by Security
- 설계 검증 과정에서 생성된 테스트케이스 기반 네트워크 보안프로토콜(TLS) 구현(SW) 검증 수행
.. 국내 최초 정형기법 기반 검증을 적용한 TLS SW 솔루션
.. 표준규격 정합성 검증 및 다양한 공격모델(Dolev-Yao) 기반 보안성 검증 수행
.. 정형기법 기반 RFC 5246(TLS v1.2) 규격정합성 검증 (24종) 완료
.. 정형기법 기반 RFC 8446(TLS v1.3) 규격정합성 검증 (44종) 완료
.. Buffer Overflow & Dos 공격 항목 대응 검증 (14종) 완료
.. Impersonation 공격 항목 대응 검증 (6종) 완료
- 오픈소스 솔루션(OpenSSL, wolfSSL, mbedTLS)과의 연동 테스트 완료
.. 표준규격 준수 검증
- 다양한 플랫폼으로의 이식이 용이한 표준 C 기반 경량화 및 라이브러리 형태 구현
- 기관 내부 SW 정적분석 검증 및 오픈라이선스 검증 완료
- 본 이전기술은 IoT 서비스의 네트워크 보안을 위해 사용되는 표준 규격 보안 프로토콜(RFC 5246(TLS v1.2), RFC 8446(TLS v1.3)) 구현 기술로, 높은 수준의 신뢰도를 요구하는 미션 크리티컬 서비스에 활용할 수 있도록 정형기법 기반의 보안 프로토콜 규격 검증(Conformance Test) 및 보안성 검증(Attack Testing)을 적용한 “IoT용 고신뢰 보장 네트워크 보안프로토콜(HASP) 기술”임
- 표준규격(RFC 5246, RFC 8446)에 대한 정형기법 기반 정합성 검증 수행
● 규격 정합성 검증 범위: Full handshake 기능(상호인증), 암호화 데이터 통신
● 규격 정합성 검증 항목: RFC 5246 (24종), RFC 8446 (44종)
● 기존 솔루션(OpenSSL, wolfSSL, mbedTLS)과의 클라이언트 및 서버 연동 기능
- 정형기법 기반 Dolev-Yao 공격 모델에 대한 보안성 검증(Attack Testing) 수행
● Buffer Overflow & Dos 공격 항목 대응 검증 (14종)
● Impersonation 공격 항목 대응 검증 (6종)
- 기기-서버 간 상호인증 기능
● PSK(Pre-shared Key) 기반 상호인증 기능
● ECC 인증서 기반 상호인증 기능
- 전송 메시지 보호용 암호키 교환 기능
● RFC 5246(TLS v1.2) 기반 암호키 교환 기능(Full Handshake)
● RFC 8446(TLS v1.3) 기반 암호키 교환 기능(Full Handshake)
- 전송 메시지 기밀성 및 무결성 기능
● 교환된 암호키 기반 전송 메시지 암호화 및 위변조 확인 기능
※ (참고) 암호알고리즘은 기술이전 및 검증 범위가 아니며, 본 이전기술은 mbedTLS 암호 라이브러리와 연동되어 있지만, 암호 IF 수정을 통해 타 암호 라이브러리와 연동이 가능함
- 프로그램(소스코드)
- 요구사항 및 요구사항 시험문서
- 사용자 매뉴얼
- 적용시장: IoT 기반 미션 크리티컬 서비스 및 고신뢰 네트워크 프로토콜 시장
? IoT 기반 미션 크리티컬 서비스 내 고신뢰 네트워크 보안프로토콜(TLS) 솔루
션으로 활용
? IP 기반 네트워크 환경에서의 고신뢰 네트워크 보안프로토콜(TLS) 솔루션으로
활용
- 검증 범위 내에서 오류가 없다는 것을 보장할 수 있는 유일한 기법인
정형기법 기반의 검증 수준을 SW 범위로 확장한 TLS 솔루션 기술로, 미션
크리티컬 분야의 높은 신뢰를 보장하는 네트워크 보안 프로토콜 기술 및 관련
시장을 선점할 수 있음