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