Рассматриваются приемы описания мандатной сущностно-ролевой ДП-модели управления доступом и информационными потоками в операционных системах семейства Linux (МРОСЛ ДП-модели) в математической нотации и формализованной нотации с использованием подтипов и тотальных функций на формализованном языке метода Event-B. Целью такого описания является упрощение дедуктивной верификации этой модели с применением инструментального средства Rodin и обеспечение более точного соответствия модели ее реализации непосредственно в программном коде операционной системы специального назначения Astra Linux Special Edition.