>> Предлагал им разработку, внедрение и поддержку безопасной ОС, основанной на мат модели...
>> Да, GNU/Linux, но с расширенными возможностями ядра, компилятора, глибс и бинутилс

Это не спасает. Дело не только в формальной\матмодели как таковой (как в совокупности формальных\математических доказательств). Дело прежде всего в реализации как таковой. Чтобы реализация точно соответствовала модели. Чтобы все работало так, как требует математика. А для линукс это вряд ли возможно.

1. Вы пишете: "основанной на матмодели".
Но сложность именно в том, что Linux никогда и не основывался на матмодели. Позволю себе напомнить, что сам Торвальдс в своей книге "Just for Fun" (если правильно помню - 10 и 11 главы) неплохо описывает полемику с Танненбаумом про микроядро. Для микроядра формальная матмодель возможна в реальности (здесь "в реальности" я имею ввиду реализацию, а не просто декларацию в виде формул), наверное, как и ее верификация. В линуксе же - нет. Ибо вопросы формализации матмодели для Linux возможны только на бумаге.
Например, можно "натянуть" матмодель типа HRU для DAC (тут я понимаю как, даже с ACL). Но тогда что делать с capabilities? Выносить за рамки модели? Или пускай пухнет множество?
Можно, наверное, "натянуть" пресловутую модель Bella и LaPadula. Но это будет справедливая модель, описывающая MLS - т.е. только для SELinux, ну, или, parsec (хе-хе). Но тогда вопрос - а что делать c DAC? Не учитывать? Плюс ко всему - в ядре линукс (в зависимости от реализации и архитектуры) примерно 350-450 системных вызовов. Примерно сотни полторы из которых совершенно точно security relevant. Если не больше. Что с ними всеми делать?
Что делать со всякими namespaces, которые довольно дырявые до сих пор и постоянно переписываются? Что делать с моделью, которая должна описывать движение информационных потоков? А ведь это ведет за собой моделирование и NetFilter тоже. То есть потребется промоделировать безопасное состояние системы с огромным количеством атрибутов и операций. Плюс аудит. Плюс функции и сисколы, ответственные за время. И т.д. и т.п. Пока будем писать модели и проверять их корректность - это несколько лет пройдет и чудовищное количество человеко-часов. Запросто получим изменения в реализации.

2. Чтобы реально, а не на бумаге получить безопасную систему требуется представление реализации, в точности воспроизводящее формальную\матмодель. Реализация же не только сисколлов (как интерфейсов к функциям), а и самих функций и структур данных - чудовищно большая и размазана по ядру (и не только ядру), точек входа много. Достаточно посмотреть на количество поддерживаемых ФС и их связку с VFS, чтобы понять что монитор обращений не так то просто не то что формализовать и проверить, а хотя бы просто описать. Кроме того, напомню, что институт системного программирования РАН пытался несколько лет верифицировать сисколлы. Но не закончили, так и бросили. До функций даже и не дошли. Плюс - чудовищный объем ядра.

3. Именно поэтому практически не встречается в CCRA не то что линукса, а и вообще юникса, имеющего сертификат выше чем EAL4+. Там чуваки серьезные и они понимают, что дальше начинается моделирование, сопоставление с представлением реализации (EAL5), а еще дальше - и верификация (EAL5+).
К сожалению наш регулятор (при всем уважении) позволяет себе (по крайней мере пока) выдавать сертификаты на линукс систему, которая у нас тащит первый или второй уровень доверия (т.е. по-их нормативке выше, чем EAL5+).

Именно поэтому я бы не стал думать, что в Газпроме сидят люди, глупее нас с вами.
Они хорошо себе представляют, где шашечки, а где ехать.
Потому и отказали. Не надо удивляться.