Политики безопасности SELinux — модуля ядра Linux, отвечающего за мандатный контроль доступа, состоят из тысяч правил и отличаются высокой сложностью. Проверить их вручную практически невозможно. При этом в критически важных средах, например, на промышленных объектах, требуется строгое математическое доказательство надежности конфигураций. Существующие инструменты автоматического аудита решают лишь точечные задачи, например, проверяют правила на целостность или непротиворечивость, но универсального подхода до сих пор не существовало.

Ученые Чжэцзянского университета (Китай) предложили решение: они описали язык правил SELinux с помощью среды математической верификации языков программирования K Framework. Ее формулами описывается синтаксис и законы работы языка, а K Framework генерирует симулятор языка, способный пошагово выполнять команды по этим законам. Кроме того, в среде предусмотрен модуль доказательства теорем, позволяющий логическим путем проверить, возможна ли в верифицируемой системе определенная ситуация.

Созданный авторами программный комплекс на базе K Framework выполняет правила SELinux на симуляторе и проверяет их с помощью модуля доказательства теорем. При этом инструмент дает пользователю возможность в едином формате задавать любые требования, как фундаментальные (конфиденциальность, целостность и др.), так и особые, зависящие от сценариев и сред.

Прототип системы проверили на реальных политиках SElinux — refpolicy и AOSP. Первая из них представляет собой эталонную базовую политику для различных систем, а вторая, разрабатываемая в Google, определяет правила изоляции приложений и системных сервисов в Android. Комплекс обнаружил в обеих значительное количество проблем, в том числе логические противоречия, скрытые конфликты, избыточные привилегии и не только.

В дальнейшем авторы собираются ускорить работу инструмента и упростить его интерфейс, чтобы системным администраторам не требовались глубокие знания математической логики для анализа правил.