Исследователи Колумбийского университета разработали гипервизор SeKVM — решение коммерческого класса на базе KVM с доказаной безопасностью. Для этого они использовали собственный способ проверки гипервизоров, значительно сокращающий трудозатраты. По словам Ронхуи Гу (Ronghui Gu), одного из соавторов, SeKVM станет основой будущих инноваций в области проверки систем и даже приведёт к появлению нового поколения устойчивого к киберугрозам системного ПО.
Проверка безопасности гипервизоров до сих пор считалась достаточно сложной задачей. Взломщики, успешно использующие уязвимости, могут получить неограниченный доступ к данным миллионов клиентов облачных провайдеров «Достаточно одного слабого звена в коде, которое практически невозможно обнаружить с помощью традиционного тестирования, чтобы система стала уязвимой для хакеров», — говорит Гу.
В теории ученые могут формально проверить программное обеспечение, чтобы математически доказать, что его код безопасен при любых сценариях работы. Однако большинство проверенных гипервизоров зачастую намного проще своих коммерческих аналогов, поскольку они не ориентированы на практическое применение. Напротив, современные коммерческие гипервизоры редставляют собой огромные куски ПО, часто включающие целое ядро ОС, что может сделать их проверку на первый взгляд неразрешимой задачей.
Например, для проверки 6,5 тыс. строк кода гипервизора CertiKOS потребовалось три человеко-года, а для проверки 9 тыс. строк кода seL4 — 10 человеко-лет. Причём оба были специально разработаны так, чтобы можно было проверить их безопасность. Для сравнения, широко используемый на практике гипервизор KVM с открытым исходным кодом, интегрированный в ядро Linux, имеет более 2 млн строк кода.
Для упрощения задачи ученые из Колумбийского университета разработали новый способ проверки коммерческих гипервизоров — микроверификацию. В этом случае гипервизор разбивается на небольшое ядро и набор недоверенных сервисов, а затем доказывает безопасность только ядра. Если оно не имеет уязвимостей, и является посредником во всех взаимодействиях гипервизора с виртуальными машинами, то в этом случае гипервизор тоже считается безопасным.
На основе микроверификации ученые разработали программное обеспечение под названием MicroV для проверки крупных гипервизоров и применили его для создания безопасного ядра SeKVM длиной всего 3800 строк кода, на проверку которого потребовалось порядка двух человеко-лет.
В реальных нагрузках SeKVM работает так же, как и обычный KVM, теряя не более 10% производительности на родном оборудовании, но обеспечивая при этом более высокий уровень безопасности. В будущем на основе данной концепции планируется создать средства защиты и в других областях — от банковских систем и устройств IoT до автономных транспортных средств и криптовалют.