구글이 국내 컴퓨터 공학 분야의 발전을 위해 서울대학교와 KAIST의 공동 연구를 지원합니다.
2020년 2월 24일 월요일
구글은 스탠포드 대학원에서 컴퓨터 공학을 공부하던 대학원생들의 아이디어에서 처음 시작되었습니다. 대학 및 연구 기관과의 강력한 유대는 구글 DNA의 근간이 되는 중요한 요소이며, 이에 구글은 전 세계 대학의 학문적 발전과 기술 혁신을 위한 다양한 프로그램을 진행하고 있습니다.Read More
구글은 스탠포드 대학원에서 컴퓨터 공학을 공부하던 대학원생들의 아이디어에서 처음 시작되었습니다. 대학 및 연구 기관과의 강력한 유대는 구글 DNA의 근간이 되는 중요한 요소이며, 이에 구글은 전 세계 대학의 학문적 발전과 기술 혁신을 위한 다양한 프로그램을 진행하고 있습니다.
그 일환으로, 구글코리아는 지난해 7월 AI 분야를 연구하는 국내 대학의 교수진⋅교육⋅학생들을 지원하기 위해 서울대학교 및 KAIST와 산학협력 파트너십을 체결했습니다. 이를 통해 각 대학의 우수 학생들에게 해외 학회, 구글 인턴십 참여 등 성장의 기회를 제공하고, AI 분야에서 훌륭한 연구를 진행하는 각 대학의 교수진에게 최대 5만 달러를 지원했습니다.
구글은 이번 협력을 통해 얻은 성과를 바탕으로 서울대학교와 KAIST가 공동으로 연구하는 ‘하프늄 검증 인프라 구축(Foundations of Hafnium Verification Infrastructure)’ 관련 프로젝트에도 총 15만 달러를 추가로 지원하고자 합니다.
하프늄은 시스템 설계자가 보다 정교한 보안 도메인으로 민감한 데이터의 기밀성과 무결성을 달성할 수 있도록 보안 하이퍼바이저(hypervisor)를 구축하는 오픈 소스 프로젝트입니다. 서울대학교 컴퓨터공학부 허충길 교수와 KAIST 전산학부 강지훈 교수는 하프늄을 엄밀하게 검증(formal verification)하는 과정에서 발생하는 기술적 문제를 해결하고, 하프늄의 기능적 정확성과 안전성을 증명하기 위해 네 명의 연구생들과 함께 하프늄 검증 인프라를 구축하는 연구를 진행할 예정입니다.
서울대학교와 KAIST의 연구진은 하프늄의 엄밀한 검증 과정에서 예상되는 어려움을 세 가지로 예상했습니다. 첫 번째는 하프늄의 동시성 때문에 엄밀한 검증에 필요한 하이퍼바이저의 불변 성질(invariant)을 포착하기가 어렵다는 것입니다. 두 번째는 임의의 가상 컴퓨터(VM)과 하프늄의 상호작용을 추론하기 위해 기능적 명세서(functional specification)와 정보 흐름 제어(information flow control)를 통합해야 한다는 점이며, 세 번째는 하프늄의 크기와 복잡성으로 인해 현재의 대규모 시스템 검증 기술로도 엄밀한 검증이 어렵다는 것이었습니다.
이에, 연구진은 하프늄의 동시성에서 오는 문제를 해결하기 위해 하프늄을 C에서 Rust로 이식(porting)하여 동시적 불변 성질은 물론 하프늄을 구현하는 데 숨겨진 모든 안전 관련 불변 성질까지도 철저하게 발견하고자 합니다. 또한 보안과 기능의 상충된 요구사항 간 균형을 적절하게 맞춰 정보 흐름 제어와 기능적 명세서를 통합하여 임의의 가상 컴퓨터와 하프늄의 상호작용을 설명하고자 합니다. 그리고 하프늄 검증 과정의 규모와 복잡성을 극복하기 위해 하프늄을 위한 모듈식 검증 전략을 개발할 예정입니다.
구글은 이번 공동 연구를 진행하는 각 대학에 7만 5천 달러 씩 추가로 지원함으로써 두 대학 기관과의 연구 협력 및 협업 체계를 강화해나갈 예정입니다. 더불어, 앞으로도 더욱 다양한 국내 대학 기관의 AI 연구 및 인재 양성에 힘을 보태어 훌륭한 산학 연구 성과를 함께 도모할 수 있기를 기대하고 있습니다. 구글이 진행하는 산학협력 프로그램에 대한 자세한 내용은 구글 산학협력 페이지에서 확인하실 수 있습니다.
작성자: 구글코리아 블로그 운영팀
