>> Если идти путем разработки микроядра с текущей мат моделью UNIX...

Зачем? Там свое. Кроме того, я не предлагал такое. Смысл моего прсыла был в том, что в сущности, при микроядре возможно достичь и в представлении реализации тех критериев безопасности, заданных формальной моделью,а не только на бумаге.

>> Cgruops, namespaces, виртуализация мне не нравятся вообще.

Именно на это я и указывал. Только вопрос не в том, что нравится, а что нет. Вопрос в том, что эти механизмы (плюс капабилити, конечно) - оооочень плохо формализуются (если это вообще возможно). А просто так их выкинуть не получится. Не учитывать их по желанию - это волюнтаризм чистой воды. Получаем неописанные ФБО в ядре, т.е., соответственно - НДВ, в чистом виде. А ведь капабилити это дискретка, которую надо бы заявлять, ибо она есть. Ну, или иначе выкидывать.

>> MAC от Bella и LaPadula просто подогнана под документооборот в DoD...

Нет. Это вовсе не так. Это просто хорошая, стррйная и простая формальная модель разграничения доступа и информационных потоков. То, что она применялась (точнее, реализация на ее базе) в DoD (и не только) - лишнее тому подтверждение.

>> Аудит кода трудоемок и не предполагался вообще. Кроме минимальных участков которые модифицируются.

Если аудит не предполагался, то как тогда планировалось убедиться в достижении критериев безопасности, заданных формальной моделью при реализации в коде? Неужели на бумаге?
Я уже указывал, что минимальных участков там нет и не будет. Это слова. Напоминаю, что функции, реализующие ФБО валяются в ядре ооооочень много где. Это совершенно точно сотни файлов исходников. Плюс - заголовочные файлы и файлы со структурами данных. Плюс, сюда надо добавить интерфейсы в виде сисколов, а это еще несколько десятков файлов, минимум. Плюс нетфильтр. Плюс - убедится в корректности работы интерфейсов, например, с помощью LTP тестов. Но они есть не на все сисколлы и не по всем входным/выходным данным. То есть там покрытие не стопроцентное, не позволяющее проверить все множество работы интерфейсов к функциям. Значит, надо дописывать тесты. Плюс, выполнить дальнейшее прослеживание, которое при проверке, скажем, команды chmod покажет, что дергается нужный сискол chmod(). А это значит, что и командные интерфейсы тоже надо исследовать и проверять. Одними бинутилсами и глибси в юзерспейсе не обойтись.

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