[연구의 필요성]
-신뢰 실행 환경(Trusted Execution Environment, TEE)은 프로그램을 격리된 환경에서 실행함으로써 민감한 데이터를 소프트웨어 및 하드웨어 공격으로부터 보호하기 위한 기술을 의미하며, 모바일, 금융, IoT 등 다양한 분야에서 널리 활용되고 있음.
-하지만 TEE가 안전한 격리 환경을 제공할 수 있는지는 구현의 정확성에 크게 의존하며, 구현 과정에서 발생할 수 있는 취약점은 보안성을 심각하게 위협할 수 있음. 따라서 TEE가 실제로 보안성을 유지할 수 있는지를 사전에 엄밀하게 검증하는 것이 필수적임.
-TEE에서 구동되는 응용프로그램(Trusted Application) 개발에 사용되는 TEE API에 대한 요구사항은 산업 표준으로 관리되고 있으나, 자연어로 기술된 문서이기 때문에 이를 바탕으로 엄밀한 검증 기술을 적용하기는 어려운 한계가 있음.

[포스텍이 가진 고유의 기술]
-TEE API의 산업 표준 요구사항을 수학적인 언어로 엄밀하게 기술하는 정형명세(Formal Specification)를 최초로 개발하였음. 특히, TEE에 기반한 응용프로그램의 구현에서 중요한 역할을 하는 TEE 저장소 API와 TEE 암호화 API를 모두 명세하였음.
-TEE API는 다양한 객체들이 복잡하고 동시(Concurrent)적인 상호작용을 수행할 수 있기 때문에 정형명세가 어려우며, 이를 해결하기 위하여 본 연구에서는 동시성 행동 명세에 효과적인 Rewriting Logic에 바탕을 둔 TEE API 정형명세 방법론을 제안하였음.
-개발한 TEE API 정형명세의 유효성을 입증하기 위하여, 정형모델을 기반으로 TEE 응용프로그램을 자동으로 검증할 수 있는 프레임워크를 개발하고, 이를 오픈소스 IoT 응용프로그램인 MQT-TZ에 적용하여 보안취약점을 발견하고 및 패치를 제안하였음.

[연구의 의미]
-본 연구는 TEE API에 대한 범용적인 정형명세를 개발하고, TEE 응용프로그램의 정형 검증을 위한 프레임워크를 제안함으로써, 신뢰성 높은 TEE 시스템을 구축하기 위한 모델을 제시하였다는 점에서 큰 의의를 가짐.
-본 연구에서 개발된 TEE API의 정형명세는, TEE 응용 프로그램 구현 시 발생할 수 있는 잠재적인 보안 취약점을 사전에 탐지하고 수정하기 위한, 정적분석, 자동 테스팅, 자동 패치 등 다양한 기술 개발에 활용될 수 있어 높은 파급효과를 기대함.
-궁국적으로, 본 연구는 TEE 기반 시스템의 신뢰성을 보장하고, 보안 무결성을 검증할 수 있는 기술적 토대를 마련함으로써 향후 더 안전하고 신뢰성 높은 TEE 환경 구축하고 이를 통해 다양한 산업 분야에서 시스템의 보안성을 향상시킬 수 있음.

[연구결과의 진행 상태 및 향후 계획]
-연구 결과는 정형기법 및 소프트웨어 공학 분야의 우수국제학회인 International Conference on Fundamental Approaches to Software Engineering 에 2024년 발표되었음.
-본 연구에서 개발한 정형명세를, 저장소 및 암호화 API 뿐만 아니라, TEE API의 전반적인 산업표준을 다룰 수 있도록 확장할 계획임.
-TEE 기반 오픈소스 보안 운영체제인 OP-TEE 등과 같은 실제적인 시스템의 검증을 개발한 정형명세를 바탕으로 수행하는 연구를 수행하고 있음.

[성과와 관련된 실적]
Geunyeol Yu, Seunghyun Chae, Kyungmin Bae, and Sungkun Moon. Formal Specification of Trusted Execution Environment APIs. International Conference on Fundamental Approaches to Software Engineering (FASE), 2024.

[성과와 관련된 이미지]

그림 1. 전반적인 TEE 아키텍처 예제

그림 2. TEE API 정형명세 개요