Безопасность компьютерных систем находится в отвратном состоянии, потому что в нашем ПО много дефектов и его невозможно полностью протестировать. Это благо для киберпреступников, но не для нас. Так почему бы не попытаться создать математически выверенное, безопасное и поддерживающее параллелизм ядро для x86 и ARM? Группа из Йельского университета это сделала.
Операционные системы находятся в сердцевине нашей цифровой цивилизации. Если они будут непробиваемы для хакеров, то миллиарды устройств — ПК, сетевые коммутаторы, IoT-девайсы, дроны и многое другое — станут гораздо безопаснее. Это вынудит киберпреступников переместить атаки на менее общие уровни софтверного стека.
Именно такой системой является CertiKOS, позволяющая создавать безопасные системные ядра. Она создана группой из Йельского университета под руководством профессора Жонга Шао и использована для создания защищенной ОС, в которой работает гипервизор, позволяющий параллельно запускать много экземпляров системы.
Крупнейший вызов
В интервью сайту YaleNews Аниндиа Банерджи, директор программы Национального научного фонда США (NSF), который помогает финансировать это исследование, отметил: «Построение функционально корректного системного ПО являлось одним из крупнейших вызовов для вычислительных технологий по крайней мере с середины
Создание доказуемо безопасной ОС, поддерживающей параллелизм (многопоточность) в многопроцессорных системах, многие годы считалось невозможным, учитывая сложность взаимодействий между слоями ПО, потоками, блокировками и процессорными ядрами. Ключевая идея группы CertiKOS, как следует из ее недавней статьи, состояла в том, чтобы разработать и удостоверить «композиционную спецификацию, способную распутать все взаимозависимости ядра и инкапсулировать интерференцию между разными ядерными объектами. Поскольку истинным предназначением ядра ОС является выстраивание слоев абстракции над машинным железом, мы настаиваем на методичном выявлении и специфицировании этих слоев и дальнейшей проверке каждого модуля ядра на характерном для него уровне абстракции».
А что на практике?
Группа разработала полностью сертифицированное ядро ОС под названием mC2 с тонко детализированной блокировкой, которое работает на стандартных многоядерных x86-процессорах. Оно также может дублироваться как гипервизор для запуска многих экземпляров Linux в гостевых виртуальных машинах на разных ядрах.
Хотя полноценный тест производительности не входил в задачи исследования, группа все же оценила ресурсопотребление гипервизора mC2 и нашла, что оно сравнимо с KVM. Однако пока еще имеются подсистемы, например файловая система и система ввода-вывода сохраняемых данных, которые еще не выстроены средствами CertiKOS. Но это вопрос времени и ресурсов, а не принципиальной возможности.
Наше мнение
CertiKOS — не единственный игрок на арене безопасных систем. «Лаборатория Касперского» недавно анонсировала собственную безопасную ОС, но не ясно, прошла ли она официальную аттестацию.
Имеется также безопасное микроядро seL4, которое официально верифицировано. FAQ на сайте seL4 содержит также хорошее обсуждение того, в чем состоит реальная суть официальной верификации. Краткий ответ следующий: чтобы обеспечить максимальную безопасность, системным архитекторам еще предстоит проявить внимание к исходным посылам и задачам своего решения. Вы не сможете бездумно положиться на верифицированное ядро и рассчитывать на безопасность.
Сегодняшний Интернет похож на Дикий Запад, где разгуливают преступники, а честные граждане становятся их жертвами. Однако постепенно инициативы типа CertiKOS приведут к тому, что в один прекрасный день мы сможем навести закон и порядок.
Но, по-моему, это произойдет не так уж скоро.
