ПРЕСС-ЦЕНТР

LynxSecure: время операционных систем реального времени в MILS-архитектуре пришло

МКА 4/07

С.В. Золотарёв

Данная статья основана на многочисленных материалах, посвящённых MILS-архитектуре, которые опубликованы в последнее время в связи с появлением первых коммерческих ОСРВ на основе MILS-архитектуры от компаний LynuxWorks (www.lynuxworks.com), GreenHiilsSoftware (www.ghs.com) и WindRiver (www.windriver.com). Наиболее подробно будет рассмотрена ОСРВ LynxSecure компании LynuxWorks, которая должна появиться на рынке в 3-4 квартале 2007 года.

Системы на основе MILS-архитектуры – уже реальность

Под MILS-архитектурой (Multiple Independent Levels of Security) мы будем понимать систему с множественными независимыми уровнями защиты/безопасности, построенную на основе изолированных разделов. Уже сейчас появились первые образцы устройств, в которых реализована MILS-архитектура. В августе 2005 года Rockwell Collins получила от NSA (National Security Agency – Агентство Национальной безопасности США) сертификат на устройство криптографии, построенное в соответствии с архитектурой MILS.

Наибольший интерес к MILS-архитектуре проявляют военные в таких областях как авионика, системы вооружения и наземной защиты, системы безопасности различного назначения. Среди военных ведомств США наибольшую поддержку развитию MILS-архитектуры оказывает AFRL (U.S. Air Force Research Lab) в рамках проектов F-22 и F-35. Эти проекты стимулируют усилия различных компаний по оценке COTS-операционных систем и middleware-продуктов. Среди их участников – лидеры в области авиационной техники Boeing, Lockheed Martin, Raytheon и Northrop Grumman; поставщики ОСРВ Green Hills Software, LynuxWorks и WindRiver, разработчики middleware OIS и другие компании.

Серьёзный интерес к MILS-архитектуре проявляют и пользователи гражданских приложений для систем управления процессами, финансовых систем, биомедицины. Так в июле 2005 года в американском консорциуме по технологиям для финансового сектора FSTC проводилась демонстрация возможностей MILS-архитектуры, которая вызвала большой интерес и одобрение со стороны участников.

MILS-системы в оборонной отрасли

В военных системах современные средства, такие как беспилотные летательные аппараты, увеличивают зависимость изделий от новых аппаратно-программных технологий, обеспечивающих возможность создания так называемых систем высокой гарантии безопасности. Однако в последние годы ощущалась нехватка идей в исследовании архитектуры таких систем и со стороны коммерческих компаний, и со стороны правительств, спонсирующих их. Архитектура MILS (Множественные Независимые Уровни Защиты/Безопасности) предложена как решение, которое должно удовлетворить требованиям гарантии защиты в системах, обрабатывающих критическую информацию. Это компонентная архитектура, основанная на коммерческом (COTS) ядре разделения, которое проводит в жизнь концепцию взаимодействия по строго формализованным правилам и выполнения приложений в изолированных разделах. Архитектура MILS поддерживает множественные уровни безопасного взаимодействия, композиции политик безопасности и модульной структуры системы так, чтобы можно было оценить критические компоненты на самых высоких уровнях и гарантировать безопасную и защищённую работу.


Рис. 1. Сегодня справедливо утверждение, что именно информационное превосходство выигрывает войны

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

Безопасное разделение информации важно, чтобы позволить защитить любой объект, например, такой как фронтовой истребитель, не ставя под угрозу предписанную ему задачу. Проблема в том, что критичная информация для истребителя очень разнообразна. Инициативы, такие как Network Centric Warfare («сетевая война») или/и Global Information Grid («Глобальная Информационная Матрица») усиливают желание поделиться информацией с объектами, удовлетворяющими концепции множественных уровней безопасности/защиты (Multiple levels of security – MLS). MLS-системы исторически считаются предшественниками MILS-систем, они были одними из самых дорогих систем при разработке и развёртывании [1]. Концепция MLS как предшественник MILS имела одно ключевое отличие – ядро безопасности MLS-систем было монолитным. Поэтому часто MILS-архитектуру определяют как многоуровневую систему с изолированными разделами (в отличие от монолитной структуры MLS).

От MLS-систем – к MILS-архитектуре

Разработка безопасных операционных систем и «ядер безопасности» началось в начале 60-70 годов. Среди первых таких систем следует назвать: Multics, MITRE Security Kernel, UCLA Data Secure Unix, Kernelized Secure Operating System (KSOS), Provably Secure Operating System (PSOS). Аналогичные работы по созданию безопасных и защищённых операционных систем продолжались в 80 и 90 годах 20 века. Традиционное ядро безопасности строилось на основе одного из вариантов мандатного контроля доступа (модель Белла-ЛаПадула) либо дискреционной политики безопасности (например, модель Харрисона-Руззо-Ульмана). Модель Белла-ЛаПадула составила теоретическую основу MLS-архитектуры. Она представляет собой формальную автоматную модель политики безопасности, описывающую множество правил управления доступом. В этой модели компоненты системы делятся на объекты и субъекты. Вводится понятие безопасного состояния и доказывается, что если каждый переход сохраняет безопасное состояние (то есть переводит систему из одного безопасного состояния в другое безопасное состояние), то согласно принципу индукции система является безопасной.

В большинстве коммерческих (COTS) операционных систем и коммуникационных технологий уровень защищённости/безопасности развивается «задним числом», а именно на основе парадигмы «сбой вначале – заплатка потом». Когда в систему проникают вредоносные объекты, тогда выполняются действия, призванные исключить их влияние и устранить «дырку», через которую они проникли. После того, как новый вирус размножается, на слабое место ставится «заплатка», чтобы остановить дальнейшее заражение. Подход «сбой вначале – заплатка потом» соответствует не любой системе, выполняющей ответственные задачи, потому что это решение является пассивным и всегда на один шаг позади нападающего. В системах для решения ответственных задач повреждения необходимо избегать или, в крайнем случае, ограничить его действие. Превентивные меры обязаны оберегать информацию и сам объект (например, фронтовой истребитель), а также препятствовать тому, чтобы повреждение случилось где-либо ещё.

Ещё два десятилетия тому назад существовали серьезные основания для того, чтобы в традиционной архитектуре назначить осуществление политики безопасности на монолитное ядро: вычислительная мощь процессоров была недостаточна для выполнения переключения контекста и изоляции данных между слоем обеспечения защиты/безопасности и прикладными задачами пользователя. Это ядро безопасности должно было удовлетворять следующим требованиям (так называемая концепция NEAT): гарантировать, что функции защиты нельзя обойти или отключить (Non-bypasssable), функции невелики и математически подтверждены (Evalautable), вызываться постоянно и регулярно при любых действиях прикладных и системных программ (Always invoked) и не могут быть ни повреждены, ни модифицированы (Tamperproof) [3].

Монолитное ядро безопасности с его набором функций часто производило большие, сложные, неструктурированные программы, которые было трудно удостоверить на более высокие уровни гарантии [4]. Профиль SCOMP, которому удалось достигнуть самой высокой оценки безопасности A1 по критериям исторической «Оранжевой книги» [5], был основан на очень простом ядре безопасности [3]. Большинство основанных на ядре безопасности систем никогда не добирались до самого высокого уровня свидетельства, которое требовало формальной проверки. Система Шифрования Сети Моторолы, которая обращалась с данными MLS через шифрование, достигла намного более низкой оценки B2, и XTS-300, преемник SCOMP, был удостоверен по уровню B3 [3].

Кроме трудности удостоверения систем со сложными монолитными ядрами при попытке провести в жизнь единственную политику безопасности для всей системы возникает другая более важная проблема.

Множественные Независимые Уровни Безопасности/Защиты (MILS) являются архитектурой, которая делает развитие, работу с конфиденциальной информацией и внедрение адекватных MLS-систем более практичными, достижимыми и возможными. Архитектура MILS значительно увеличивает защиту, уменьшает время разработки и снижает планируемый риск при развёртывании технологии для того, чтобы обеспечить создание системы высокой гарантии, которая является и безопасной, и защищённой [1].

Однако следует заметить, что в то время, как архитектура MILS строится как система очень безопасных распределённых компонентов, она автоматически не гарантирует безопасность всей системы, составленной из этих независимых компонентов. Безопасность всей системы с MILS-архитектурой всё ещё зависит от проектировщика, обеспеченного стандартными блоками и инструментами построения необходимых уровней политики безопасности, которые могут быть проверены. Существуют инструменты [2], предназначенные доказать, что определённая политика безопасности соответствует нужному уровню для данной системы.

MILS были созданы, чтобы позволить приложениям с определённым высоким уровнем безопасности стать реальными. Эта архитектура использует в своих интересах рост производительности микропроцессоров в соответствии с Законом [6] Мура, что делает возможным формальное моделирование и математическую проверку компонентов с целью создания фундамента систем высокой гарантии защиты/безопасности. В MILS приложения уполномочены, чтобы провести в жизнь их собственную политику безопасности вместо того, чтобы положиться на обобщённые ядерные службы безопасности. MILS-архитектура также позволяет реализовать рациональное системное проектирование, где компоненты с высокой гарантией безопасности могут быть повторно эффективно использованы без модификации. Это понижает затраты на подтверждение уровня безопасности, так как артифакты сертификации применяются не единожды.

Свойства MILS-систем

Понятие MILS появилось в работах Джона Рашби (John Rushby), доктора философии Стэнфордского Научно-исследовательского института, в начале 1980 гг. [7, 8]. Он предложил, чтобы ядро разделения разбивало память на изолированные области, используя единицу управления памятью аппаратных средств (MMU), и допускало только строго формализованные коммуникации между тщательно управляемыми разделами. Такой подход позволял одному разделу оказывать услугу другому с минимальным вмешательством от ядра [7].

Традиционные сервисы операционной системы, которые ранее работали в привилегированном (или супервизорном) режиме – такие как драйверы устройств, файловая система, сетевые стеки и др. – теперь работают в непривилегированном (пользовательском) режиме (рис. 2).


Рис. 2. Выполнение компонентов MILS-системы в пользовательском и привилегированном режимах

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

  • Изоляция данных: жёсткое разделение адресного пространства между MILS-разделами.
  • Контроль потока информации. Защищённая и авторизованная связь между разделами. Каждое приложение выполняется в собственном адресном пространстве памяти и может взаимодействовать только с разделами своего или более низких уровней защиты/безопасности, используя для этого специальные MILS-сокеты.
  • Разделение интервалов работы процессора. Микропроцессор и любое сетевое оборудование не могут использоваться как тайный канал, чтобы «подслушать» информацию (то есть быть подслушивающим третьим лицом).
  • Изоляция ошибки. Последствия сбоя ограничены, отказ в одном разделе не распространяется на другие разделы. Отказы обнаруживаются, локализуются и восстанавливаются в месте возникновения.

Кроме этого, ядро выполняет функции обслуживания прерываний и работы с семафорами.

В результате ядро стало намного меньше (от 4K до 8K исходного кода) и проще, и появилась возможность провести строгое математическое доказательство правильности свойств формальными методами. Это сокращение размера отразилось в самой фундаментальной выгоде MILS: значительномуменьшении количества критического по отношению к безопасности кода – настолько, что можно существенно увеличить уровень строгости при верификации этого кода. Если делать совсем немного вещей, то вполне реально сделать их очень хорошо – так хорошо, что коду можно будет доверять в вопросе защиты наших самых ценных данных даже от угрозы самого высокого уровня.

Дополнительно к идеям Рашби при построении MILS-систем на уровне приложений используются принципы минимума привилегий и проверки возможностей Зальцера и Шрёдера. Под привилегиями обычно понимается набор разрешений, установленных для исполнения каких-либо действий. Существует три пути минимизации привилегий:

  • Назначение привилегий для части программы (например, для клиент-серверных программ);
  • Назначение только абсолютно необходимых привилегий (например, назначать приложениям собственные идентификаторы пользователя или группы);
  • Ограничение времени привилегий (например, ситуация открытия TCP-портов меньших 1024, для доступа к которым необходимы привилегии администратора).

Промежуточный слой программного обеспечения в MILS-архитектуре

MILS middleware – обширная концепция с очень широкими возможностями, работающими в режиме пользователя. Промежуточный слой содержит много сервисов операционной системы, таких как драйверы устройства, которые ранее работали в привилегированном режиме. Работая в пользовательском режиме, они также должны осуществлять политики безопасности ядра. Уровень MILS middleware также выполняет такие функции, как включение файловой системы, сетевых сетей, разделяемых библиотек, шифрование, установление подлинности и т.д. Промежуточный слой MILS middleware также имеет традиционный промежуточный прикладной уровень – такие технологии, как CORBA [8], DDS, Веб-службы и др. Уровень MILS middleware может находиться в том же самом разделе в режиме пользователя как приложение, которое он поддерживает или в самостоятельных защищённых разделах в режиме пользователя.

Приложения также делают свою обработку и проводят в жизнь их собственную политику безопасности в разделе в режиме пользователя (user-mode). Приложения, работающие в своём разделе, могут получить только доступ к памяти, которая была явно выделена для этого раздела. Прикладные разделы могут только общаться друг с другом через пути, которые формировались, когда система была произведена. Ни в коем случае разделы с приложениями не могут иметь доступ напрямую к аппаратным средствам, если это явно не было предусмотрено при проектировании системы. Архитектура MILS, наряду с абстрактным набором допустимых потоков информации, показана на рис. 3.


Рис. 3.Потоки информации MILS-архитектуры

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

Как уже указывалось, ядро безопасности должно удовлетворять следующим требованиям:

  • Non-bypassable. Гарантировать, что функции защиты нельзя обойти или отключить;
  • Evalautable. Функции невелики и математически подтверждены;
  • Alwaysinvoked. Функции должны вызываться постоянно и регулярно при любых действиях прикладных и системных программ;
  • Tamperproof. Функции не могут быть ни повреждены, ни модифицированы.

Акроним для этих четырёх признаков – NEAT [9]. Осуществление политики безопасности, которая не удовлетворяет требованиям NEAT, является не эффективным. Хотя другие операционные системы и предложили некоторую форму функциональных возможностей non-bypassability и tamperproof, архитектура MILS впервые обеспечивает полный набор NEAT-свойств в коммерческих продуктах (COTS-системах), которые формально смоделированы и математически проверены на высоком уровне гарантии безопасности.

Другая цель MILS состоит в том, чтобы позволить оценке безопасности сложной системы быть разделённой на многие независимые маленькие оценки. Критические по отношению к безопасности компоненты программного обеспечения, которые обращаются к больше чем одному уровню информации, могут быть оценены высоким уровнем безопасности приблизительно по Уровню Гарантии Оценки (EAL) 6+ Общих Критериев [10]. Независимость этих оценок также допускает повторное использование кода, интерфейсов прикладного программирования (API), спецификаций, артифактов оценки и свидетельств до самой высокой возможной степени.

Взаимодействие с другими системами

Компоненты сети MILS, такие как протокольные стеки и связанные с ними интерфейсы драйверов устройств, могут быть помещены в собственный раздел. У этой архитектуры есть несколько преимуществ:

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

Приложения используют API, чтобы взаимодействовать с сетью. Сетевое API для MILS может иметь ту же самую семантику, что и в традиционной операционной системе, например, такую как знакомый интерфейс для IP-сокетов. Различие выполнения API может быть полностью «под капотом» или прозрачным для прикладного разработчика. Вместо того чтобы взаимодействовать непосредственно с протоколом, выполнение MILS-сокета использует ядерное средство коммуникаций между разделами для отправки выходных данных стеку протокола. Входные данные обрабатываются так же в обратном порядке.

Безопасные сетевые системы

Встроенный компьютер, который не связан с другим процессором, можно назвать редким исключением. Проводя в жизнь свои четыре основополагающих политики безопасности, архитектура MILS создаёт надёжный информационный фундамент гарантии безопасности в единственном узле. Таким образом, мы можем создать надёжный информационный фундамент гарантии безопасности всюду в распределённой системе и обеспечить непрерывное осуществление той же самой политики безопасности с помощью middleware-компонента PCS – Partitioning Communications System. Он всегда находится между приложением и протоколами/драйверами, которые производят передачу данных. Такая конфигурация показана на рис. 4.


Рис. 4.Безопасная конфигурация сетевой системы

PCS проводит в жизнь политику безопасности от начала до конца, обеспечивая:

  • сильную идентичность каждого узла в пределах множества MILS-узлов (анклав);
  • разделение по уровням и/или по группам интересов. Анклавы тогда связаны вместе через высокую гарантию MILS у кросс-доменных серверов;
  • безопасную загрузку изображений;
  • безопасную синхронизацию часов (времени);
  • работу полосы пропускания и качество обслуживания;
  • подавление скрытых каналов.

Сетевые средства middleware-уровня

Проектировщики решений для распределённых систем часто используют сетевые COTS middleware-средства для различных прикладных задач:

  • для Клиент/сервер-приложений часто используют CORBA [11] и DDS;
  • Web-ориентированные сервисы, используя HTTP-сервисы и компоненты, такие как XML, SOAP (Простой Протокол Доступа Объекта); WSDL(Язык Описания Веб-служб) и др. Это позволяет обмениваться информацией между большими разнообразными распределёнными системами.

Все эти технологии могут быть рассмотрены как инструменты, которые предоставляют прикладному программисту высокоуровневую абстракцию на основе элементарного интерфейса сокетов. Большая часть кода для этих сетевых middleware-технологий может или находится вместе в том же самом разделе, что и приложение, которое оно поддерживает, или оно может находиться в отдельном разделе. В любом случае, портирование существующего кода в MILS-среду – простая задача, потому что API-сокет не нуждается в изменении. Компонент PCS всё еще находится между сетевым middleware и стеком протокола и/или драйверами устройства.

Гостевые операционные системы

Традиционная операционная система или встраиваемая операционная система реального времени (например, Integrity, VxWorks или LynxOS), или настольная операционная система (например, Linux, Windows или Solaris) может работать в разделе MILS как гостевая операционная система. У операционных систем, написанных с поддержкой мобильности в памяти, есть слой абстракции аппаратных средств (HAL), который ограничивает все определённые для процессора функции. Создание нового HAL-слоя считается главной задачей в перенесении на новый центральный процессор. Вы можете использовать те же самые знания для написания HAL, который абстрагирует ядро разделения MILS так же, как аппаратные средства для гостевой операционной системы.

Концепция гостевой операционной системы позволяет старым приложениям быть легко перенесёнными в среду MILS c высокой гарантией безопасности. Другая возможность заключается в том, что каждый из MILS-разделов может содержать экземпляр гостевой операционной системы. Это эффективно создаёт множество виртуальных операционных систем на единственном реальном микропроцессоре. Ядро MILS обеспечивает разделение, заслуживающее доверия и относительно доступа памяти и относительно времени центрального процессора. Коммуникации среди разделов ограничены путями, явно созданными в момент, когда система была произведена. Это – практический путь к реализации кросс-доменных решений. Это – также практический путь к выполнению автоматизированных рабочих мест высокой гарантии, подходящих для MLS или операций коалиционных вооружённых сил.

MILS-архитектура и международные стандарты

MILS-архитектура базируется на широко применяемых и отработанных международных и отраслевых стандартах, таких как:

  • DO-178B, «Software Consideration in Airborne Systems and Equipment Certification» (Требования к ПО для сертификации авиационных систем и оборудования), разработка RTCA (www.rtca.org). Стандарт DO-178B принят в 1992 году.
  • ARINC-653, «Avionics Application Software Standard Interface» (Стандартный интерфейс программного обеспечения для приложений в области авионики), разработка ARINC (Aeronautical Radio, Inc., www.arinc.com/cf/store/index.cfm), 1997 год.
  • Common Criteria for Information Technology Security Evaluation (Общие критерии оценки безопасности информационной технологии). РазработкаNIST, 1996 год. [10].
  • Director of Central Intelligence Directive 6/3, Protecting Sensitive Compartmented Information Within Information Systems, Protection Level 5 [12].

Первоеядроразделения LynxSecure набазе Intel Virtualization Technology длявоенныхиавиационныхсистемот LynuxWorks

Компания LynuxWorks (www.lynuxworks.com) представила первое в мире встраиваемое ядро разделения (separation kernel) LynxSecure в MILS-архитектуре. Новая разработка LynuxWorks базируется на технологии виртуализации Intel Virtualization и поднимает на более высокий уровень стандарты защиты и безопасности ПО встраиваемых систем.


Рис. 5. Пример системы на базе LynxSecure

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

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

«Ядро LynxSecure представляет собой будущее встраиваемых защищённых и безопасных операционных систем, – комментирует Гуриот Сингх (Guriot Singh), исполнительный директор LynuxWorks. – Безопасность данных – один из основополагающих принципов построения встраиваемых систем. Совершенствованием средств защиты, как правило, занимаются разработчики встраиваемых систем военного назначения, но мы стремимся реализовать эти усовершенствования и для гражданских приложений. Сочетание ядра LynxSecure и технологии виртуализации Intel VT является одним из решений этой задачи».

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

В отличие от обычного ядра безопасности, реализующего все высоконадёжные функции безопасной операционной системы, LynxSecure представляет собой ядро разделения. Оно разграничивает все данные и системные ресурсы и управляет информационными потоками между разделами. Ядро LynxSecure поддерживает симметричную мультипроцессорную обработку, а также 32- и 64-разрядную адресацию, что обеспечивает широкие возможности масштабирования. В ближайшем будущем планируется сертификация ядра LynxSecure на соответствие как общим требованиям EAL 7, так и требованиям DO-178B уровня А, причём реализованная в нём технология разделения обеспечивает для этого уникальные возможности.

Дополнительную информацию об архитектуре MILS, можно найти на сайте http://mils.ois.com.

Литература

  1. Vanfleet, Willard Mark, et al. «An Architecture for Deeply Embedded, Provable High Assurance Applications». May 2003.
  2. Freeman, James, George Dinolt, and Richard Neely. An Internet System Security Policy and Formal Model. Proc. of 11th National Computer Security Conference, Oct. 1988: 10-19.
  3. Anderson, Ross. Security Engineering. New York: Wiley & Sons, 2001.
  4. Rushby, John. A Trusted Computing Base for Embedded Systems. Proc. of the 7th Department of Defense/NBS Computer Security Conference, Sept. 1984: 294-311.
  5. Department of Defense. Trusted Computer System Evaluation Criteria (The Orange Book). DoD 5200.28STD. Washington: DoD, 1983.
  6. Moore, G. «Cramming More Components Onto Integrated Circuits». Electronics Magazine 19 Apr. 1965.
  7. Rushby, John. «The Design and Verification of Secure Systems». ACM Operating Systems Review 15.5.
  8. Rushby, John. «Proof of Separability: A Verification Technique for a Class of Security Kernels». Computer Science 137: (1982) 352-367.
  9. Partitioning Kernel Protection Profile, May 2003.
  10. Common Criteria for Information Technology Security Evaluation, Ver. 2.1, 19 Sept. 2000.
  11. Currey, Jonathan, Bill Beckwith, et al. Real-Time CORBA 1.1 Specification, Object Management Group Aug. 2002.
  12. Director of Central Intelligence. «Protecting Sensitive Compartmented Information Within Information Systems». Directive 6/3. Washington: DCID, 5 June 1999 www.fas.org/irp/offdocs/DCID_6-3_20Policy.htm.