Аннотация доклада.

В докладе анализируется опыт по применению научных подходов и основанных на их реализации инструментальных средств, позволяющих достичь высокое доверие к механизмам защиты операционной системы специального назначения (ОССН) Astra Linux Special Edition . В первую очередь в докладе показывается, что основой этого процесса много лет является доверие к механизму управления доступом, в основе разработки которого используется мандатная сущностно-ролевая ДП-модель безопасности управления доступом и информационными потоками в ОС семейства Linux (МРОСЛ ДП-модели). Эта модель, во-первых, включила детальное описание на математическом языке порядка функционирования механизма управления доступом ОССН, в том числе сочетания в нем ролевого управления доступом, мандатного управления доступом и мандатного контроля целостности. Во-вторых, в её рамках выполнено строгое доказательство условий безопасности механизма управления доступом, в том числе безопасности информационных потоков по времени. В-третьих, она переведена из классического «монолитного» в иерархическое представление, которое задаёт модель по уровням (слоям). В-четвертых, накопленный опыт её формирования и внедрения позволил на её основе осуществить моделирование единого механизма управления доступом для ОССН и её штатной СУБД PostgreSQL. Также в докладе обзорно показывается, что обоснование внутренней непротиворечивости МРОСЛ ДП-модели выполнено путём её представления на формальном языке Event -B и её дедуктивная верификация с применением инструментального средства Rodin. Корректность реализации модели непосредственно в программном коде ОССН демонстрируется в среде Frama-C с использованием инструментального средства статического анализа Why3. Распространение доверия от механизма управления доступом ко всему программному коду ОССН осуществляется с использованием широкого спектра инструментов статической (Svace, Clang Static Analyzer и др.) и динамической (Syzkaller4Astra, IibFuzzer, Crusher и др.) верификации кода.