Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

EROS ( Чрезвычайно надежная операционная система ) - операционная система, разработанная в 1991 году компанией EROS Group, LLC, Университетом Джона Хопкинса и Университетом Пенсильвании . Возможности включают автоматическое сохранение данных и процессов , некоторую предварительную поддержку в реальном времени и безопасность на основе возможностей . EROS - это чисто исследовательская операционная система, которая никогда не использовалась в реальных условиях. По состоянию на 2005 год разработка остановилась в пользу двух систем-преемников, CapROS и Coyotos .

Ключевые понятия [ править ]

Основная цель системы EROS (и ее родственников) - обеспечить надежную поддержку на уровне операционной системы для эффективной реструктуризации критически важных приложений на небольшие коммуникационные компоненты. Каждый компонент может взаимодействовать с другими только через защищенные интерфейсы и изолирован от остальной системы. «Защищенный интерфейс» в этом контексте - это тот, который обеспечивается частью самого нижнего уровня операционной системы ( ядром ). Ядро - единственная часть системы, которая может передавать информацию от одного процесса к другому. Он также полностью контролирует машину и (при правильной конструкции) не может быть обойден. В EROS предоставляемый ядром механизм, с помощью которого один компонент называет и вызывает службы другого, - это возможности, использующиемежпроцессное взаимодействие (IPC). Применяя интерфейсы с защищенными возможностями, ядро ​​гарантирует, что все сообщения к процессу поступают через намеренно экспортированный интерфейс. Это также гарантирует , что не вызов не возможен , если применение компонент не имеет действительную способность к invokee. Защита в системах возможностей достигается путем ограничения распространения возможностей от одного компонента к другому, часто с помощью политики безопасности, известной как ограничение .

Системы возможностей естественным образом продвигают компонентную структуру программного обеспечения. Этот организационный подход аналогичен концепции объектно-ориентированного программирования в языке программирования , но проявляется на большей степени детализации и не включает концепцию наследования . Такая реструктуризация программного обеспечения дает несколько преимуществ:

  • Отдельные компоненты наиболее естественно структурированы как циклы событий . Примеры систем, которые обычно структурируются таким образом, включают системы управления полетом (см. Также рекомендации по программному обеспечению DO-178B при сертификации бортовых систем и оборудования ) и системы телефонной коммутации (см. Коммутатор 5ESS ). Программирование, управляемое событиями, выбрано для этих систем прежде всего из-за простоты и надежности, которые являются важными атрибутами в жизненно важных и критически важных системах.
  • Компоненты становятся меньше, и их можно тестировать по отдельности, что помогает разработчику легче выявлять недостатки и ошибки.
  • Изоляция каждого компонента от других ограничивает масштаб ущерба, который может возникнуть, если что-то пойдет не так или неправильно работает программное обеспечение.

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

В отличие от многих более ранних систем, возможности являются единственным механизмом для именования и использования ресурсов в EROS, что делает ее тем, что иногда называют чистой системой возможностей. Напротив, IBM AS / 400 является примером коммерчески успешной системы возможностей, но это не чистая система возможностей.

Архитектуры с чистыми возможностями поддерживаются хорошо проверенными и зрелыми математическими моделями безопасности. Они использовались для формальной демонстрации того, что системы на основе возможностей можно сделать безопасными, если они будут реализованы правильно. Было показано, что так называемое «свойство безопасности» разрешимо для систем с чистыми возможностями (см. Lipton ). Конфайнмент, который является фундаментальным строительным блоком изоляции, был официально проверен на предмет обеспечения его соблюдения с помощью чистых систем возможностей [1] и сводится к практической реализации с помощью «конструктора» EROS и «фабрики» KeyKOS. Для любого другого примитивного механизма защиты сопоставимой проверки не существует. В литературе есть фундаментальный результат, показывающий, что «безопасность»математически неразрешима в общем случае (см. HRU, но заметим, что это, конечно, доказуемо для неограниченного множества ограниченных случаев [2] ). Что еще более важно с практической точки зрения, безопасность оказалась ложной для всех примитивных механизмов защиты, используемых в текущих массовых операционных системах. Безопасность - необходимое условие успешного применения любой политики безопасности. В практическом плане, этот результат означает , что не представляется возможным в принципе обеспечить существующие системы товарных, но потенциально возможно защищенных систем потенциалами на основе предоставленныхони выполняются с достаточной тщательностью. Ни EROS, ни KeyKOS никогда не были успешно взломаны, и их механизмы изоляции никогда не были успешно побеждены каким-либо внутренним злоумышленником, но неизвестно, были ли эти две реализации достаточно осторожными. Одна из целей проекта Coyotos - продемонстрировать, что изоляция и безопасность компонентов были окончательно достигнуты за счет применения методов проверки программного обеспечения.

Система L4.sec, которая является преемником семейства микроядер L4 , является системой, основанной на возможностях, и на нее значительно повлияли результаты проекта EROS. Влияние взаимно, поскольку работа EROS над высокопроизводительным вызовом была сильно мотивирована успехами Йохена Лидтке с семейством микроядер L4 .

История [ править ]

Основным разработчиком EROS был Джонатан С. Шапиро. Он также является движущей силой Coyotos , что является «эволюционным шагом» [3] за пределы операционной системы EROS.

Проект EROS начался в 1991 году как реконструкция чистой комнаты более ранней системы KeyKOS . KeyKOS была операционная система , разработанная компанией Key Logic, Inc., и был прямым продолжением работы над ранее гнозиса (Great новой операционной системы в небе) система , созданная Tymshare, Inc. обстоятельства кончину Key Logic в 1991 году сделал лицензирования КейКОС непрактичный. Поскольку KeyKOS в любом случае не работал на популярных процессорах, было принято решение восстановить его по общедоступной документации.

К концу 1992 года стало ясно, что архитектура процессора значительно изменилась с момента появления идеи возможностей, и уже не было очевидно, что системы с компонентной структурой практичны. Системы на основе микроядра , которые также поддерживают большое количество процессов и IPC, сталкиваются с серьезными проблемами производительности, и было неясно, удастся ли их успешно решить. Архитектура x86 явно становилась доминирующей, но дорогостоящая задержка перехода пользователь / супервизор на 386 и 486 создала серьезные проблемы для изоляции на основе процессов. Проект EROS превратился в исследовательскую работу и переехал в Пенсильванский университет.стать центром диссертационных исследований Шапиро. К 1999 году была продемонстрирована высокопроизводительная реализация процессора Pentium, которая по производительности напрямую конкурировала с семейством микроядра L4 , которое известно своей исключительной скоростью в IPC. Механизм ограничения EROS был официально проверен, в процессе создания общей формальной модели для систем безопасности.

В 2000 году Шапиро поступил на факультет компьютерных наук Университета Джонса Хопкинса. В Hopkins целью было показать, как использовать возможности ядра EROS для создания безопасных и защищаемых серверов на уровне приложений. EROS, финансируемый Агентством перспективных исследовательских проектов Министерства обороны США и Исследовательской лабораторией ВВС США , использовался в качестве основы для доверенной оконной системы [4], высокопроизводительного, защищаемого сетевого стека [5] и положительных результатов для безопасного веб-браузера. . Он также использовался для изучения эффективности облегченной статической проверки. [6] В 2003 году были обнаружены некоторые очень сложные проблемы безопасности [7] , которые присущилюбая системная архитектура, основанная на синхронных примитивах IPC (в частности, включая EROS и L4). Работа над EROS остановлена ​​в пользу Coyotos, которая решает эти проблемы.

По состоянию на 2006 год EROS и ее преемники являются единственными общедоступными системами, работающими на стандартном оборудовании.

Статус [ править ]

Работа над EROS первоначальной группой остановлена, но есть две системы-преемники. Система CapROS строится непосредственно из кодовой базы EROS, а система Coyotos - это система-преемница, которая устраняет некоторые архитектурные недостатки EROS и изучает возможность полностью проверенной операционной системы. Ожидается, что и CapROS, и Coyotos будут выпущены в различных коммерческих версиях.

См. Также [ править ]

  • Наноядро

Ссылки [ править ]

  1. ^ Джонатан С. Шапиро; Сэмюэл Вебер (29 октября 1999 г.). «Проверка механизма удержания EROS» . Архивировано из оригинала 3 марта 2016 года.
  2. ^ Питер Ли. «Код подтверждения» . Архивировано из оригинального 22 сентября 2006 года.
  3. ↑ Джонатан Шапиро (2 апреля 2006 г.). «Различия между Coyotos и EROS - краткое изложение» . Архивировано из оригинала на 2012-07-31.
  4. ^ Джонатан С. Шапиро; Джон Вандербург; Эрик Нортап; Давид Чизмадиа. «Дизайн доверенной оконной системы EROS» . Архивировано из оригинала 3 марта 2016 года.
  5. ^ Аншумал Синха; Сандип Сарат; Джонатан С. Шапиро. «Перезагрузка сетевых подсистем: высокопроизводительная, защищенная сетевая подсистема» . Архивировано из оригинала 3 марта 2016 года.
  6. ^ Хао Чен; Джонатан С. Шапиро. «Использование встроенной статической проверки для сохранения инвариантов корректности» (PDF) . Архивировано из оригинала (PDF) от 3 марта 2016 года.
  7. ^ Джонатан С. Шапиро. «Уязвимости в синхронных проектах IPC» . Архивировано из оригинала 3 марта 2016 года.

Журналы [ править ]

  1. Р. Дж. Липтон и Л. Снайдер. «Алгоритм линейного времени для определения безопасности объекта». Журнал ACM , 24 (3): 455-464, 1977.
  2. Майкл А. Харрисон , У. Л. Руццо и Джеффри Д. Ульман . «Защита в операционных системах». Коммуникации ACM . 19 (8): 461-471, август 1976 г.

Внешние ссылки [ править ]

  • Домашняя страница Coyotos на Wayback Machine (архивировано 2 сентября 2016 г.)
  • Домашняя страница EROS на Wayback Machine (архивировано 4 марта 2016 г.)
  • Домашняя страница KeyKOS на Wayback Machine (архивировано 4 января 2016 г.)
  • Домашняя страница Джонатана Шапиро
  • CapROS