Библиография
Аннотация
В статье рассматривается подход к обеспечению целостности в операционных системах, построенных на микроядерной архитектуре на примере KasperskyOS. Микроядерная архитектура операционной системы обеспечивает изоляцию доверенного и недоверенного кода и минимизацию доверенной вычислительной базы.
Это открывает возможность строить механизмы безопасности, которые сохраняют свои гарантии даже в случае некорректного поведения отдельных частей системы. В представленной модели вводится понятие драйвера объекта — посредника, который обрабатывает запросы сущностей к ресурсам. В результате модель может доказывать отсутствие запрещенных информационных потоков, которые могут нарушить целостность системы, а также формализовать взаимодействия в условиях потенциально небезопасных компонентов.
Авторы описывают набор требований, которым должны соответствовать драйверы объектов и другие сущности системы, а также показывают, что целостность доверенного компонента системы не нарушается при их выполнении. Более того, модель дает возможность проведения анализа поведения системы при нарушении требований. Формулируется и доказывается ключевая теорема: если все компоненты удовлетворяют предъявленным требованиям, информационные потоки от недоверенных компонентов к доверенным отсутствуют, а при наличии нарушений ущерб локализуется на ограниченных уровнях целостности. Это означает, что компрометация низкоцелостного компонента не приведёт к компрометации высокоцелостных частей системы.
Важной частью работы является разработка языка описания политик мандатного контроля целостности, адаптированного к особенностям модели. Язык позволяет задавать формальные правила для различных сценариев, включая процесс обновления KasperskyOS. Авторы приводят пример политики, гарантирующей безопасное проведение обновлений и предотвращающей распространение последствий возможных ошибок или атак.
Материал будет полезен специалистам в области кибербезопасности, разработчикам операционных систем и исследователям моделей управления доступом, которые занимаются проектированием архитектур, позволяющих минимизировать доверенную вычислительную базу. Модель и язык политик могут служить основой для построения и анализа защищённых систем как в промышленном, так и в научно-образовательном контекстах.