>> Там вполне достаточно чтобы сложить 2+2.Да я и не сомневался, что сразу все ясно.
>> Дополнения для безопасности.
Решение, безусловно, новаторское. Сначала надо вырвать с мясом из ядра те вещи, которые и так уже работают, поломав по дороге совместимость пользовательского окружения. А потом надо затолкать в ядро непонятно что. И обозвать это непонятное - "расширенными возможностями" и "дополнениями безопасности". Подход тоже ясен, да.
>> Писал уже, capabilities учитываются как независимые от DAC и MAC.
Это тоже прорыв. К сведению: capabilities - есть типичный DAC. Ибо это дискреционное разграничение доступа на основе атрибутов. Не считать capabilites механизмом DAC - это точно такое же гениальное решение, как и предыдущее.
Кроме того, сам термин "учитываются" - вот он что означает? Как именно множество то капабилитей планировалось формализовать в модели и увязывать с другими механизмами DAC? Ау? Или не планировали все-же? Хотели как то "учесть"? А что такое - "учесть"?
Посчитать, сколько их в конкретном ядре есть и написать какая для чего нужна? И все? Так для этого и писать то ничего не надо. Все в манах есть. Даже на русском языке. А формально доказывать, что они всегда корректно работают? Нет? Не надо делать? Ну и правильно.
>> Тяжело, но можно.
Это демагогия. Есть ли независимо подтверждаемые и научно обоснованные примеры?
Их нет. Как уже справедливо писали выше - формальная модель в каком-то виде (не полном, ибо я то ее как раз читал, и не одну) есть для Astra линукс, но это мало что дало на практике.
Мандатка там текла, да, тупо зная пароль пользователя и используя su можно было зафигачить эскалацию привилегий и инициировать факт НСД. Находясь в одном уровне, прямо и без затей из оболочки можно было запросить доступ к файлу на другом уровне. Не знаю, как там у них с этим делом сейчас. Закрыли эту дыру или нет. Зато была модель, да.
Этот пример отлично иллюстрирует как раз корень проблемы - косая реализация "бумажной" формальной модели, неверифицированной и с плохим аудитом - привела к дыре в механизме безопасности. И во всех виденных мной моделях - есть грабли. Модели не полные. А значит реализация, таким образом, как минимум содержит неформализованные ФБО в ядре.
А у ведущих разработчиков ОС Linux, коими в том числе являются Red Hat, SUSE и Canonical - моделей нет совсем. Они и не претендуют. Ибо они то как раз хорошо понимают чудовищность и объем проблемы. Кроме того, я уже предлагал - можно не соглашаться с моими доводами, я не заставляю. Можно не считать мою агрументацию убедительной, я не заставляю. Но есть факты, они упрямая вещь, а моя аргументация может быть независимо от меня проверена. Не согласны с аргументацией и фактами - ну попробуйте обратиться в какую-нибудь аккредитованую CCRA испытательную лабораторию. Их много. Можно обратиться к IBM, Red Hat, Suse, Canonical, написать хоть Таненбауму. И предложить им написать формальную модель или модели. Может, они что-то ответят?
>> Вы пытаетесь построить одну большую мат модель.
Вовсе нет. Я пытаюсь сказать, что количество моделей не имеет значения. Одна она, две, или двадцать две. Важно то, что модель или модели должны на формальном языке описывать все без исключения (еще раз повторю - все без исключения!) механизмы принятия решений, включая решения по разграничению информационных потоков тоже (то есть и фильтр пакетов тоже, если он есть, а в линуксе он есть, а сейчас и не один). Именно для этого модель(и) и нужна(ы). И кроме этого, модель(и) должна(ы) иметь непротиворечивое(ые), независимо проверяемое(ые) доказательство(а). Проще всего это сделать с помощью математики. Доказательство даст алгоритм. А алгоритм уже можно реализовать в коде. И проверить реализацию. А ну как в коде ошибка, и алгоритм реализован не верно? Если этого не сделать, то никакой реальной пользы не будет.
>> На бумаге мы оперируем уже моделями и следим чтобы они закрывали все теоретические дыры
Демагогия. Что такое - "теоретическая дыра"? Модель (ну или совокупность моделей, если угодно, сути это не меняет) не призвана закрывать какие-то там дыры. Хоть "теоретические", хоть "практические". Доброе утро.
Модель должна доказывать (и не только доказывать формальным способом, а и иметь как минимум еще ссылки на проверяемую реализацию) - что цели безопасности достижимы, угрозам безопасности можно успешно противодействовать, политики безопасности реализуемы, предположения безопасности выполнимы.
А все эти угрозы, цели, политики и предположения уже давным-давно сформулированы, определены и заданы заранее. И у нас и у них. Смотрим любой профиль защиты - и там (о ужас!) их находим. Как для самой ОС, так и для среды её выполнения. Так что никаких "теоретических дыр" нет. Есть вполне конкретные, четко сформулированные цели безопасности, которых нужно достичь, угрозы, которым нужно противостоять и т.д. Зачем вы пишите про "теоретические дыры", которых нет в природе? Просто почитайте уже хотя бы любой профиль защиты и постарайтесь понять, что там написано, и почему именно так написано.
Подытожим:
а) некие люди пришли в Газпром и предложили (создать?) некую реализацию ОС на базе Линукс, содержащую некие "расширенные возможности ядра", задекларированные как "дополнения для безопасности";
б) те же лица предложили (создать?) еще некую документацию на систему. Как минимум - формальную модель безопасности;
в) при всем этом - в модели не предполагалось приводить описание и формализацию cgroups, namespaces и capabilities, и, похоже, netfilter тоже. Все это, конечно, привело бы к возникновению проблемы НДВ\РДВ и потенциальному обходу описанных и формализованных в модели механизмов безопасности. Но кому оно надо? Зачем бумагу и время тратить, и что-то там описывать и формализовывать, правда?;
г) при всем этом, на сколько я понял, реализация предполагала отключение cgroups и namespaces, что привело бы к заметной деградации в юзерспейсе. Вместо них в реализацию должны были бы быть включены некие магичесикие и никак по переписке не идентифицируемые "расширенные возможности ядра", задекларированные как "дополнения для безопасности". Что это - не ясно. Что это дает, кроме поломок в юзерспейсе - не ясно;
д) проверка реализации не предполагала аудита кода, но, странным образом, предполагала его верификацию. Цитата: "Аудит всего кода не предполагался. Вот изменяемой, для дачи гарантий, часть кода предполагалось верифицировать с формальной мат моделью". Верификация - это не просто аудит. Это проверка доказательств правоты, помимо просто аудита. Ну да ладно. Про чудовищные объемы аудита и верификации, а также осуществление прослеживания (алгоритм -> структура данных -> конкретная функция в ядре -> системный вызов, взаимодействующий с функцией -> прикладная программа) - писать и повторяться не буду, писал ранее. Если не проверить и не проследить все, что в скобках в предыдущем предложении - имеем неясно что, с точки зрения ИБ. Очевидно, что это все и не планировалось. Опыт Red Hat, SUSE и Canonical был проигнорирован.
В целом, мне все ясно. Тут налицо какая-то мутная попытка выдать непонятно что за защищенную систему. Хорошо, что такое не получилось.
За сим более писать не буду. И так все понял.
И про уровень экспертизы, и про модель, и про реализацию системы.
