WikiDer > Ядро разделения

Separation kernel

А ядро разделения это вид безопасности ядро используется для моделирования распределенной среды. Концепция была представлена Джон Рашби в статье 1981 г.[1] Рашби предложил ядро ​​разделения как решение трудностей и проблем, возникших при разработке и проверке больших и сложных ядер безопасности, предназначенных для «обеспечения многоуровневой безопасной работы в многопользовательских системах общего назначения». По словам Рашби, «задача ядра разделения состоит в том, чтобы создать среду, которая неотличима от среды, предоставляемой физически распределенной системой: она должна выглядеть так, как если бы каждый режим был отдельной изолированной машиной, и эта информация может поступать только с одной машины. с другим по известным внешним линиям связи. Следовательно, одно из свойств разделительного ядра, которое мы должны доказать, состоит в том, что нет каналов для потока информации между режимами, кроме тех, которые явно указаны ".

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

В 2007 году Управление по обеспечению информации США Национальное Агенство Безопасности (NSA) опубликовало Профиль защиты ядра разделения (SKPP),[2] спецификация требований безопасности для ядер разделения, подходящих для использования в наиболее агрессивных средах угроз. СКПП описывает, в Общие критерии[3] Говоря языком, класс современных продуктов, которые обеспечивают фундаментальные свойства концептуального ядра разделения Рашби. Он определяет функциональные требования безопасности и требования к обеспечению безопасности для построения и оценки ядер разделения, в то же время обеспечивая некоторую свободу выбора, доступную разработчикам.

SKPP определяет ядро ​​разделения как «аппаратные и / или микропрограммные и / или программные механизмы, основная функция которых состоит в создании, изоляции и разделении нескольких разделов и управлении потоком информации между субъектами и экспортируемыми ресурсами, выделенными этим разделам». Кроме того, основные функциональные требования ядра разделения включают:

  • защита всех ресурсов (в том числе ЦПУ, память и устройства) от несанкционированного доступа
  • разделение внутренних ресурсов, используемых Целевой функцией функций безопасности оценки (ФБО), от экспортируемых ресурсов, предоставляемых субъектам
  • разделение и изоляция экспортируемых ресурсов
  • посредничество информационных потоков между разделами и между экспортируемыми ресурсами
  • аудиторские услуги

Ядро разделения распределяет все экспортируемые ресурсы под своим контролем в разделы. Разделы изолированы, за исключением явно разрешенных информационных потоков. Действия субъекта в одном разделе изолированы от субъектов другого раздела (то есть не могут быть обнаружены или переданы), если этот поток не был разрешен. Разделы и потоки определены в данных конфигурации. Обратите внимание, что «раздел» и «субъект» являются ортогональными абстракциями. «Разделение», как показывает его математический генезис, обеспечивает теоретико-множественное группирование системных сущностей, тогда как «субъект» позволяет нам рассуждать об отдельных активных сущностях системы. Таким образом, раздел (коллекция, содержащая ноль или более элементов) не является субъектом (активным элементом), но может содержать ноль или более субъектов.[2]

Ядро разделения предоставляет своим размещенным программам высоконадежное разделение и свойства управления информационными потоками, которые являются защищенными от взлома и не допускающими обхода. Эти возможности обеспечивают настраиваемую надежную основу для различных системных архитектур.[2]

В сентябре 2008 г. ЦЕЛОСТНОСТЬ-178B из Программное обеспечение Green Hills стал первым разделительным ядром, сертифицированным по СКПП.[4]

Системы Wind River имеет технологию ядра разделения, которая находилась в активном процессе сертификации в 2009 году.

Lynx Software Technologies имеет разделительное ядро, LynxSecure.

В 2011 году Управление по обеспечению информации закрыло ЮКПП. АНБ больше не будет сертифицировать определенные операционные системы, включая ядра разделения, против SKPP, отмечая, что «соответствие этому профилю защиты само по себе не дает достаточной уверенности в том, что информация о национальной безопасности должным образом защищена в контексте более крупной системы, в которой соответствующий продукт интегрирован ».[5]

В микроядро seL4 имеет формальное доказательство того, что его можно настроить как ядро ​​разделения.[6] Доказательство обеспечения соблюдения информационного потока[7] вместе с этим подразумевает очень высокий уровень гарантии для этого варианта использования. Муэн[8] Ядро разделения также является официально проверенным ядром разделения с открытым исходным кодом для машин x86.

Смотрите также

Рекомендации

  1. ^ Джон Рашби, «Проектирование и проверка защищенных систем», Восьмой симпозиум ACM по принципам операционных систем, стр. 12–21, Асиломар, Калифорния, декабрь 1981 г. (Обзор операционных систем ACM, Vol. 15, № 5).
  2. ^ а б c Управление обеспечения информации, Агентство национальной безопасности, Форт Джордж Г. Мид, доктор медицины. «Профиль защиты правительства США для разделительных ядер в средах, требующих высокой устойчивости», версия 1.03, июнь 2007 г.
  3. ^ «Общие критерии оценки безопасности информационных технологий», версия 3.1, CCMB-2006-09-001, 002, 003, сентябрь 2006 г.
  4. ^ http://www.niap-ccevs.org/cc-scheme/st/st_vid10119-st.pdf
  5. ^ https://www.niap-ccevs.org/pp/archived/PP_SKPP_HR_V1.03/
  6. ^ https://github.com/seL4/l4v/blob/master/proof/bisim/Syscall_S.thy
  7. ^ https://www.nicta.com.au/publications/research-publications/?pid=6464
  8. ^ https://muen.sk/muen-report.pdf