Исследователи Колумбийского университета представили SeKVM, устойчивый к взлому гипервизор. SeKVM — первая система для облачных вычислений, прошедшая формальную верификацию. Это значит, что ПО является математически правильным, что код программы работает так, как должен, и нет никаких скрытых ошибок безопасности, о которых следует беспокоиться, заявляют авторы.
«Это первый случай, когда программа доказала свою математическую корректность и безопасность, — заявил Джейсон Ние, профессор информатики и один из авторов разработки. — Это означает, что данные пользователей защищены от ошибок безопасности и хакеров».
За последние десять лет формальной верификации уделялось много внимания, но все эти исследования проводились на маленьких системах, которые никто не использует в реальной жизни. Проверка многопроцессорной системы считалась более или менее невозможной, утверждают исследователи.
Работа Ние и его коллеги Ронгхуэя Гу представляет собой гипервизор KVM с некоторыми изменениями. KVM — это гипервизор, который используется для запуска виртуальных машин облачными провайдерами, такими как Amazon. Как заявляют исследователи, им удалось доказать, что SeKVM безопасен и гарантирует изоляцию виртуальных компьютеров друг от друга.
«Мы показали, что наша система может защищать личные данные и вычисления, загруженные в облако, с математическими гарантиями. Это никогда не удавалось добиться раньше».
SeKVM проверили с помощью MicroV, нового фреймворка для проверки безопасности больших систем. Он основан на гипотезе о том, что небольшие изменения в системе могут значительно упростить проверку. Этот метод исследователи называют микроверификацией. Метод позволил проверить большую систему, такую ??как KVM, что раньше считалось невозможным.
Ши-Вэй Ли, студент Колумбийского университета и соавтор исследования, добавил, что SeKVM будет служить защитой в различных областях, от банковских систем и устройств Интернета вещей до автономных транспортных средств и криптовалют.
Статья о разработке будет представлена 26 мая на 42-м симпозиуме IEEE. Авторы технологии уже получили за нее награду Amazon Research Award. Дальнейшая разработка SeKVM будет продолжаться в рамках контракта с Агентством перспективных исследовательских проектов Минобороны США (DARPA). Кроме того, за эту работу Ние был удостоен стипендии Гуггенхайма.
Sarymian
raamid
Вообще-то круто. Вот как-то так и нужно будет сдерживать мощь ИИ, чтобы он нас не отформатировал.
Bavun
Звучит фантастически. И в прямом, и в переносном смысле.
Tyusha
Было бы здорово узнать, что такое формальная верификация, пару слов о принципах строгой математической проверки. Первый раз слышу. Это вообще как?
plus79501445397
на хабре например было (а по тегу еще куча находится). На мой взгляд при этом подходе уделяется внимание не всем аспектам безопасности: например как верификация одного ПО защитит от уязвимостей в процессорах/прошивке? В ПО для верификации так же могут быть ошибки. И т.д.
cepera_ang
Можете вот тут глянуть, если с английским нет проблем.
bakhirev
А по факту потом данные утекут через какую-нибудь XSS дырку или закладку АНБ. Вообще после всех историй о дырках и взломах всего, странно давать 100% гарантии.
dorne
Основная проблема систем формальной верификации в том, что они ограничены рамками математической модели. В случае полностью верифицированного ПО уязвимости надо искать в фактическом различии между реальностью и моделью.
Так, например, модель верифицирующая программу на уровне ассемблерного кода не сможет определить наличие уязвимости типа SPECTRE если:
1. Не знает о ней заранее.
2. Не умеет заглядывать на уровень процессорной архитектуры или микрокода ЦП.