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

Доказано что любая реализация DAC и MAC в микроядерных OS будет работать более чем в 10 раз медленнее по сравнению с монолитными OS! И пока нет других мат моделей заменяющих DAC и MAC, рандомизация не дает таких гарантий, в разработке микроядерных OS ставим точку.

> > Cgruops, namespaces, виртуализация мне не нравятся вообще.
> Вопрос в том, что эти механизмы (плюс капабилити, конечно) - оооочень плохо формализуются (если это вообще возможно). А просто так их выкинуть не получится.

У меня получается эти механизмы выкинуть. С ними выкидывается сразу systemd, elogind.

У вас ниукого нет никакого понимания общей безопасности ОС! В РФ об этом по чему-то никто не знает!!!

Распределите все существующие модели безопасности по их ВРЕМЕНИ, ПОРЯДКУ, МЕСТУ применения в OS. Узрите что большинство применяется последовательно, а не паралельно и  можно считать независимыми друг от друга.

Capabilities применяется последовательно с Integrity, сразу после нее и паралельно с DAC и MAC, но почти независимо от них, применяется ядром на всем протяжении работы программы. Оно дробит права root по областям и следит за тем чтобы не использовалось более чем заявлено самой прогой и/или разрешено ядром OS. Реализация на стороне программы дорогая.

Вы не видите лес в целом ч высоты, а пытаетесь понять, что такое лес, рассматривая листочки и веточки.

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

DoD имела свою бумажную инструкцию бумажного документооборота, а Bella и LaPadula, тупо, вместо разработки MAC для OS, сперли модель бумажного документооборота и написали по ней свой MAC. И это плохо для общего применения.

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

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

А иначе никак, даже с ресурсами Газпрома. Людей подготовленных просто столько нет.

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

Ниукого нет одной большой мат модели, которая учитывает все. Есть безопасность как совокупность многих методов, каждый с которых имеет свою хорошую мат модель. Есть понимание где, в каких конкретных точках все эти методы применяются: последовательно или параллельно к друг другу. Есть допущение что каждый метод безопасности почти не взаимодействует с другими и его можно рассматривать отдельной мат моделью.

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