[테크월드=방제일 기자] 서울대학교 컴퓨터공학부 허충길 교수 연구진이 소프트웨어를 엄밀히 검증해 보안성을 높이는 연구 내용을 인정받아 2020 Google ASPIRE(Android Security and PrIvacy REsearch) award를 수상했다. 이를 통해 연구진은 구글로부터 150,000달러의 연구 기금을 지원받게 된다.
구글은 2018년 말 안드로이드 에코시스템의 보안성과 개인정보 보호 강화를 위한 노력의 일환으로 ASPIRE 프로그램을 시작했다. 이 프로그램은 Android Security and Privacy 팀과 학계의 협력을 다양한 방식으로 지원해, 새로운 보안기술을 개발하고 이를 안드로이드 시스템에 적용하는 것을 목적으로 하고 있다.
이번 수상은 허충길 교수팀이 소프트웨어 검증을 단계별로 나눠 수행할 수 있는 이론과 기술을 개발한 것이 기반이 됐다. 기존의 프로그램 검증 기술은 주로 호어논리(Hoare Logic)와 이를 확장한 분리논리(Separation Logic)에 기반을 두고 있다. 이 이론은 프로그램을 모듈별로 나줘 검증하는 것은 충분히 지원한다. 하지만 큰 규모의 소프트웨어 검증을 효율적으로 수행하기 위해서는 각 모듈의 검증을 여러 단계로 나눠 한번에 한가지 성질만 검증하는 과정이 꼭 필요하다.
최근 허충길 교수 연구진이 개발한 RUSC(Refinement Under Self-related Contexts) 이론은 분리논리(Separation Logic)가 지원하는 다양한 모듈별 검증 기술뿐만 아니라 단계적 검증도 동시에 지원한다.
연구진은 이 이론에 기반한 검증 프레임워크를 개발하고 있으며, 이를 활용해 구글 주도로 개발되고 있는 보안용 하이퍼바이저인 PKVM(Protected Kernel-based Virtual Machine)을 검증하는데 기여할 계획이다.
그래도 삭제하시겠습니까?