Исследователи Колумбийского университета представили SeKVM, устойчивый к взлому гипервизор. SeKVM — первая система для облачных вычислений, прошедшая формальную верификацию. Это значит, что ПО является математически правильным, что код программы работает так, как должен, и нет никаких скрытых ошибок безопасности, о которых следует беспокоиться, заявляют авторы.
«Это первый случай, когда программа доказала свою математическую корректность и безопасность, — заявил Джейсон Ние, профессор информатики и один из авторов разработки. — Это означает, что данные пользователей защищены от ошибок безопасности и хакеров».
За последние десять лет формальной верификации уделялось много внимания, но все эти исследования проводились на маленьких системах, которые никто не использует в реальной жизни. Проверка многопроцессорной системы считалась более или менее невозможной, утверждают исследователи.
Работа Ние и его коллеги Ронгхуэя Гу представляет собой гипервизор KVM с некоторыми изменениями. KVM — это гипервизор, который используется для запуска виртуальных машин облачными провайдерами, такими как Amazon. Как заявляют исследователи, им удалось доказать, что SeKVM безопасен и гарантирует изоляцию виртуальных компьютеров друг от друга.
«Мы показали, что наша система может защищать личные данные и вычисления, загруженные в облако, с математическими гарантиями. Это никогда не удавалось добиться раньше».
SeKVM проверили с помощью MicroV, нового фреймворка для проверки безопасности больших систем. Он основан на гипотезе о том, что небольшие изменения в системе могут значительно упростить проверку. Этот метод исследователи называют микроверификацией. Метод позволил проверить большую систему, такую как KVM, что раньше считалось невозможным.
Ши-Вэй Ли, студент Колумбийского университета и соавтор исследования, добавил, что SeKVM будет служить защитой в различных областях, от банковских систем и устройств Интернета вещей до автономных транспортных средств и криптовалют.
Статья о разработке будет представлена 26 мая на 42-м симпозиуме IEEE. Авторы технологии уже получили за нее награду Amazon Research Award. Дальнейшая разработка SeKVM будет продолжаться в рамках контракта с Агентством перспективных исследовательских проектов Минобороны США (DARPA). Кроме того, за эту работу Ние был удостоен стипендии Гуггенхайма.
