ОС EROS: Операционная система на основе возможностей

Введение

Операционная система, основанная на возможностях (Capability based operating system) – операционная система, разработка которой началась в 1991 году в Университете Пенсильвании, а затем продолжалась в Университете Джона Хопкинса и The EROS Group, LLC. К её особенностям относятся автоматическое сохранение данных и процессов, частичная поддержка работы в реальном времени и безопасность, основанная на возможностях. EROS является исключительно исследовательской операционной системой и никогда не применялась на практике. В 2005 году разработка была остановлена в пользу системы-преемницы CapROS.

Основные понятия

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

Отдельные компоненты наиболее естественно структурируются как циклы обработки событий. Примеры систем, обычно структурированных таким образом, включают системы управления полетом воздушных судов (см. также DO 178B «Рекомендации по программному обеспечению в бортовых системах и оборудовании») и телефонные коммутаторы (см. коммутатор 5ESS). Программирование, управляемое событиями, выбирается для этих систем главным образом из-за простоты и надежности, которые являются важнейшими атрибутами в системах, критичных для жизни и миссии. Компоненты становятся меньше и индивидуально тестируемыми, что облегчает изоляцию и выявление дефектов и ошибок. Изоляция каждого компонента от других ограничивает масштаб любого ущерба, который может возникнуть в случае сбоя или некорректной работы программного обеспечения. В совокупности эти преимущества приводят к значительно более надежным и безопасным системам. Plessey System 250 — это система, первоначально разработанная для использования в телефонных коммутаторах, в которой архитектура, основанная на возможностях, была выбрана специально из-за ее надежности. В отличие от многих предыдущих систем, в EROS возможности являются единственным механизмом для именования и использования ресурсов, что делает ее иногда называемой «чистой системой возможностей». IBM i, напротив, является примером коммерчески успешной системы, основанной на возможностях, но не является чистой системой возможностей. Чистые архитектуры, основанные на возможностях, поддерживаются хорошо протестированными и зрелыми математическими моделями безопасности. Они использовались для формального доказательства того, что системы, основанные на возможностях, могут быть безопасными при правильной реализации. Так называемое «свойство безопасности» было показано как разрешимое для чистых систем возможностей (см. Липтон). Ограничение, являющееся фундаментальным строительным блоком изоляции, было формально проверено как применимое к чистым системам возможностей и реализовано на практике конструктором EROS и фабрикой KeyKOS. Для других примитивных механизмов защиты подобная проверка отсутствует. В литературе существует фундаментальный результат, показывающий, что безопасность математически неразрешима в общем случае (см. HRU, но обратите внимание, что она, конечно, доказуема для неограниченного набора ограниченных случаев). Более практическое значение заключается в том, что безопасность оказалась ложной для всех примитивных механизмов защиты, поставляемых с современными коммерческими операционными системами. Безопасность является необходимым условием успешного применения любой политики безопасности. На практике это означает, что в принципе невозможно обеспечить безопасность современных коммерческих систем, но потенциально возможно обеспечить безопасность систем, основанных на возможностях, при условии их тщательной реализации. Ни EROS, ни KeyKOS никогда не были успешно взломаны, и их механизмы изоляции никогда не были успешно обойдены внутренним злоумышленником, но неизвестно, были ли обе реализации достаточно тщательными. Одной из целей проекта Coyotos было продемонстрировать, что изоляция и безопасность компонентов были окончательно достигнуты посредством применения методов верификации программного обеспечения. L4.sec, являющаяся преемницей семейства микроядер L4, — это система, основанная на возможностях, и на нее оказали значительное влияние результаты проекта EROS. Влияние взаимно, поскольку работа EROS над высокопроизводительным вызовом была сильно мотивирована успехами Jochen Liedtke с семейством микроядер L4.

The individual components are most naturally structured as event loops. Examples of systems that are commonly structured this way include aircraft flight control systems (see also DO 178B Software Considerations in Airborne Systems and Equipment Certification), and telephone switching systems (see 5ESS switch). Event driven programming is chosen for these systems mainly because of simplicity and robustness, which are essential attributes in life critical and mission critical systems. Components become smaller and individually testable, which helps to more readily isolate and identify flaws and bugs. The isolation of each component from the others limits the scope of any damage that may occur when something goes wrong or the software misbehaves. Collectively, these benefits lead to measurably more robust and secure systems. The Plessey System 250 was a system originally designed for use in telephony switches, which capability based design was chosen specifically for reasons of robustness. In contrast to many earlier systems, capabilities are the only mechanism for naming and using resources in EROS, making it what is sometimes referred to as a pure capability system. In contrast, IBM i is an example of a commercially successful capability system, but it is not a pure capability system. Pure capability architectures are supported by well tested and mature mathematical security models. These have been used to formally demonstrate that capability based systems can be made secure if implemented correctly. The so called "safety property" has been shown to be decidable for pure capability systems (see Lipton). Confinement, which is the fundamental building block of isolation, has been formally verified to be enforceable by pure capability systems, and is reduced to practical implementation by the EROS constructor and the KeyKOS factory. No comparable verification exists for any other primitive protection mechanism. There is a fundamental result in the literature showing that safety is mathematically undecidable in the general case (see HRU, but note that it is of course provable for an unbounded set of restricted cases). Of greater practical importance, safety has been shown to be false for all of the primitive protection mechanisms shipping in current commodity operating systems. Safety is a necessary precondition to successful enforcement of any security policy. In practical terms, this result means that it is not possible in principle to secure current commodity systems, but it is potentially possible to secure capability based systems provided they are implemented with sufficient care. Neither EROS nor KeyKOS has ever been successfully penetrated, and their isolation mechanisms have never been successfully defeated by any inside attacker, but it is not known whether the two implementations were careful enough. One goal of the Coyotos project was to demonstrate that component isolation and security has been definitively achieved by applying software verification techniques. The L4. sec system, which is a successor to the L4 microkernel family, is a capability based system, and has been significantly influenced by the results of the EROS project. The influence is mutual, since the EROS work on high performance invocation was motivated strongly by Jochen Liedtke's successes with the L4 microkernel family.

История

Основным разработчиком EROS был Джонатан С. Шапиро. Он также был движущей силой Coyotos, который представлял собой «эволюционный шаг» по сравнению с операционной системой EROS. Проект EROS начался в 1991 году как воссоздание в чистой комнате более ранней операционной системы KeyKOS. KeyKOS была разработана компанией Key Logic, Inc. и являлась прямым продолжением работы над более ранней системой Great New Operating System In the Sky (GNOSIS), созданной компанией Tymshare, Inc. Обстоятельства, связанные с прекращением деятельности Key Logic в 1991 году, сделали лицензирование KeyKOS невозможным. Поскольку KeyKOS в любом случае не работала на популярных коммерческих процессорах, было принято решение восстановить её на основе общедоступной документации. К концу 1992 года стало ясно, что архитектура процессоров значительно изменилась с момента появления концепции возможностей, и практичность компонентно-ориентированных систем стала сомнительной. Системы на основе микроядра, которые также отдают предпочтение большому количеству процессов и IPC, сталкивались с серьезными проблемами производительности, и было неясно, можно ли их успешно решить. Архитектура x86 явно становилась доминирующей, но высокая задержка переключения между режимами пользователя и ядра на процессорах 386 и 486 создавала серьезные проблемы для изоляции на основе процессов. Проект EROS превратился в исследовательскую работу и был перенесен в Университет Пенсильвании, где стал темой диссертации Шапиро. К 1999 году была продемонстрирована высокопроизводительная реализация для процессора Pentium, которая напрямую конкурировала по производительности с семейством микроядер L4, известным своей исключительной скоростью IPC. Механизм ограничения EROS был формально верифицирован, в процессе чего была создана общая формальная модель для безопасных систем, основанных на возможностях. В 2000 году Шапиро присоединился к преподавательскому составу факультета компьютерных наук Университета Джона Хопкинса. В Хопкинсе целью было показать, как использовать возможности, предоставляемые ядром EROS, для создания безопасных и устойчивых к атакам серверов на уровне приложений. EROS, финансируемый Агентством передовых исследовательских проектов Министерства обороны и Исследовательской лабораторией ВВС, использовался в качестве основы для надежной оконной системы, высокопроизводительного и устойчивого к атакам сетевого стека, а также для разработки безопасного веб-браузера. Он также использовался для изучения эффективности легковесной статической проверки. В 2003 году были обнаружены серьезные уязвимости, присущие любой системной архитектуре, основанной на синхронных примитивах IPC (в частности, EROS и L4). Работа над EROS была приостановлена в пользу Coyotos, которая решила эти проблемы. По состоянию на 2006 год EROS и его преемники являются единственными широко доступными системами, основанными на возможностях, которые работают на стандартном оборудовании.

The primary developer of EROS was Jonathan S. Shapiro. He was also the driving force behind Coyotos, which was an "evolutionary step" beyond the EROS operating system. The EROS project started in 1991 as a clean room reconstruction of an earlier operating system, KeyKOS. KeyKOS was developed by Key Logic, Inc., and was a direct continuation of work on the earlier Great New Operating System In the Sky (GNOSIS) system created by Tymshare, Inc. The circumstances surrounding Key Logic's demise in 1991 made licensing KeyKOS impractical. Since KeyKOS did not run on popular commodity processors in any case, the decision was made to reconstruct it from the publicly available documentation. By late 1992, it had become clear that processor architecture had changed significantly since the introduction of the capability idea, and it was no longer obvious that component structured systems were practical. Microkernel based systems, which similarly favor large numbers of processes and IPC, were facing severe performance challenges, and it was uncertain if these could be successfully resolved. The x86 architecture was clearly emerging as the dominant architecture but the expensive user/supervisor transition latency on the 386 and 486 presented serious challenges for process based isolation. The EROS project was turning into a research effort, and moved to the University of Pennsylvania to become the focus of Shapiro's dissertation research. By 1999, a high performance implementation for the Pentium processor had been demonstrated that was directly performance competitive with the L4 microkernel family, which is known for its exceptional speed in IPC. The EROS confinement mechanism had been formally verified, in the process creating a general formal model for secure capability systems. In 2000, Shapiro joined the faculty of Computer Science at Johns Hopkins University. At Hopkins, the goal was to show how to use the facilities provided by the EROS kernel to construct secure and defensible servers at application level. Funded by the Defense Advanced Research Projects Agency and the Air Force Research Laboratory, EROS was used as the basis for a trusted window system, a high performance, defensible network stack, and the beginnings of a secure web browser. It was also used to explore the effectiveness of lightweight static checking. In 2003, some very challenging security issues were discovered that are intrinsic to any system architecture based on synchronous IPC primitives (notably including EROS and L4). Work on EROS halted in favor of Coyotos, which resolved these issues. as of 2006, EROS and its successors are the only widely available capability systems that run on commodity hardware.

Статус

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