Проверяем capability-делегирование в стиле ОС Fuchsia средствами Isabelle/HOL
Доступ к ресурсам в Zircon, микроядре операционной системы Fuchsia от Google, построен на том, что процесс работает с объектом ядра только через дескриптор, а права этого дескриптора задают, что с объектом можно делать. Такая модель задумана как основа безопасности и модульности системы: ошибка в драйвере не должна превращаться в угрозу целостности ядра. Допустим, один процесс передаёт другому дескриптор объекта ядра с урезанными правами. Как убедиться, что получатель ни в одном сценарии не окажется с правом, которого не было у отправителя? Для ответа на этот вопрос мы построили в Isabelle/HOL учебную модель фрагмента capability-механизма Zircon и доказали это свойство для всех состояний, достижимых из корректного старта. Модель показывает и предел гарантии: один привилегированный обход через MMIO, прямая запись в память объекта, ломает изоляцию, хотя проверка прав остаётся на месте. Читать далее