허충길 교수 연구진,
소프트웨어 검증 기술 연구로 2020 Google ASPIRE award 수상

허충길 교수 연구진은 소프트웨어를 엄밀히 검증하여 보안성을 높이는 연구 방향으로 2020 ASPIRE(Android Security and PrIvacy REsearch) award(150,000 USD)를 수상하였다.

구글(Google)은 2018년 말 안드로이드(Android) 에코시스템의 보안성과 개인정보 보호 강화를 위한 노력의 일환으로 ASPIRE 프로그램을 시작했다. 이 프로그램은 Android Security and Privacy 팀과 학계의 협력을 다양한 방식으로 지원하여, 새로운 보안기술을 개발하고 이를 안드로이드(Android) 시스템에 적용하는 것을 목표로 하고 있다. 연구진은 이번 수상으로 구글(Google)로부터 미화 150,000달러의 연구 기금을 지원받는다.

이번 수상의 기반이 된 연구로 허충길 교수 연구진은 소프트웨어 검증을 단계별로 나눠서 수행할 수 있는 이론 및 기술을 개발했다. 기존의 프로그램 검증 기술은 주로 호어논리(Hoare Logic) 및 이를 확장한 분리논리(Separation Logic)에 기반을 두고 있으며, 이 이론은 프로그램을 모듈별로 나줘서 검증하는 것은 잘 지원한다. 하지만 큰 규모의 소프트웨어 검증을 효율적으로 수행하기 위해서는 각 모듈의 검증을 여러 단계로 나눠서 한번에 한가지 성질만 검증하는 것도 꼭 필요하다. 최근 허충길 교수 연구진이 개발한 RUSC(Refinement Under Self-related Contexts) 이론은 분리논리(Separation Logic)가 지원하는 다양한 모듈별 검증 기술뿐만 아니라 단계적 검증도 동시에 지원한다. 연구진은 이 이론에 기반한 검증 프레임워크를 개발중에 있으며, 이를 활용하여 구글(Google) 주도로 개발되고 있는 보안용 하이퍼바이저인 PKVM(Protected Kernel-based Virtual Machine)을 검증하는데 기여할 계획이다.

Google의 ASPIRE 프로그램 소개 페이지: https://security.googleblog.com/2018/12/aspire-to-keep-protecting-billions-of.html