Қабілетке негізделген операциялық жүйе: EROS жүйесінің сипаттамасы

Кіріспе

Құзыреттік негізделген операциялық жүйе. Өте сенімді операциялық жүйе (EROS) – 1991 жылы Пенсильвания университетінде, кейін Джонс Хопкинс университетінде және EROS Group, LLC компаниясында әзірленген операциялық жүйе. Оның ерекшеліктері: автоматты деректер мен процестердің сақталуы, алдын ала нақты уақытты қолдау және құзыреттік негізделген қауіпсіздік. EROS – таза зерттеулік операциялық жүйе, ол ешқашан нақты қолданыста болған емес. 2005 жылдан бастап, даму CapROS жүйесінің пайдасына тоқтатылды.

Негізгі ұғымдар

EROS жүйесінің (және оның туыстарының) басты мақсаты – операциялық жүйе деңгейінде маңызды қосымшаларды шағын байланыс компоненттеріне тиімді қайта құрылымдау үшін күшті қолдау көрсету. Әрбір компонент басқаларымен тек қорғалған интерфейстер арқылы ғана байланыса алады және жүйеден оқшауланады. Осы жағдайда қорғалған интерфейс – операциялық жүйенің ең төменгі деңгейі, ядро арқылы қамтамасыз етілетін интерфейс. Бұл жүйеде ақпаратты бір процестен екіншісіне ауыстыра алатын жалғыз бөлік – осы ядро. Ол сондай-ақ машинаны толық бақылайды және (дұрыс құрастырылған болса) айналып өту мүмкін емес. EROS-та ядро бір компоненттің басқа компоненттің қызметін атауы мен шақыруы үшін процестер аралық байланысты (IPC) пайдаланады, бұл мүмкіндік болып табылады. Ядро мүмкіндіктерді қолдану арқылы процеске барлық байланыс қасатттан экспортталған интерфейс арқылы келуін қамтамасыз етеді. Сондай-ақ, шақырушы компонент шақырылған компонентке жарамды мүмкіндікке ие болмаса, шақыру мүмкін емес екенін қамтамасыз етеді. Қуаттылық жүйелеріндегі қорғаныс мүмкіндіктердің бір компоненттен екіншісіне таралуын шектеу арқылы жүзеге асырылады, көбінесе шектеу деп аталатын қауіпсіздік саясаты арқылы. Қуаттылық жүйелері компоненттік бағдарламалық жасақтама құрылымын табиғи түрде қолдайды. Бұл ұйымдастыру тәсілі объектіге бағытталған бағдарламалау тілінің тұжырымдамасына ұқсас, бірақ ірі гранулярлықта болады және мұрагерлік тұжырымдамасын қамтымайды. Бағдарламалық жасақтама осылай қайта құрылымдалғанда бірнеше артықшылықтар пайда болады: Жеке компоненттер оқиға циклдары ретінде ең табиғи түрде құрылады. Әдетте осылай құрылған жүйелерге әуе кемесінің ұшуды басқару жүйелері (сонымен қатар DO 178B Әуе жүйелері мен жабдықтарының сертификациясы бағдарламалық қамтамасыз етуі қарастырылады) және телефондық коммутация жүйелері (сонымен қатар 5ESS коммутаторы) жатады. Оқиғаға негізделген бағдарламалау осы жүйелер үшін негізінен қарапайымдылық пен беріктілік таңдалады, бұл өмірлік және миссиялық маңызды жүйелердегі маңызды қасиеттер. Компоненттер кішірейіп, жеке-жеке сынауға қолайлы болады, бұл кемшіліктер мен қателерді оңай оқшаулауға және анықтауға көмектеседі. Әрбір компоненттің басқалардан оқшаулануы, бірдеңе дұрыс болмағанда немесе бағдарламалық жасақтама дұрыс жұмыс істемегенде туындауы мүмкін кез келген зақымның ауқымын шектейді. Бұл артықшылықтардың жиынтығы айтарлықтай берік және қауіпсіз жүйелерге әкеледі. Plessey System 250 бастапқыда телефондық коммутаторларда пайдалану үшін жасалған жүйе болды, онда мүмкіндіктерге негізделген дизайн беріктік себептерімен арнайы таңдалды. Көптеген бұрынғы жүйелерден айырмашылығы, EROS-те ресурстарды атау және пайдаланудың жалғыз механизмі – мүмкіндіктер, сондықтан оны кейде таза мүмкіндіктер жүйесі деп атайды. IBM i – коммерциялық сәтті мүмкіндіктер жүйесінің мысалы, бірақ ол таза мүмкіндіктер жүйесі емес. Таза мүмкіндіктер архитектурасы жақсы сынақтан өткен және жетілген математикалық қауіпсіздік модельдерімен қамтамасыз етіледі. Бұл модельдерді қолдану арқылы, егер жүйе дұрыс іске асырылса, мүмкіндіктерге негізделген жүйелерді қауіпсіз етуге болатынын ресми түрде дәлелдеуге болады. "Қауіпсіздік қасиеті" деп аталатын қасиет таза мүмкіндіктер жүйелері үшін шешілетін болып табылған (Лipton қараңыз). Оқшаулаудың негізгі құрылыс блогы болып табылатын қамау, таза мүмкіндіктер жүйелерімен жүзеге асырылуы ресми түрде тексерілді және EROS конструкторымен және KeyKOS фабрикасымен практикалық іске асыруға дейін төмендетілді. Басқа ешқандай бастапқы қорғау механизмі үшін мұндай тексерулер жоқ. Әдебиетте қауіпсіздіктің жалпы жағдайда математикалық түрде шешілмейтінін көрсететін негізгі нәтиже бар (HRU қараңыз, бірақ бұл шектеусіз шектеулі жағдайларда дәлелденетінін ескеріңіз). Ең маңыздысы, қауіпсіздік қазіргі заманғы тауарлық операциялық жүйелердегі барлық бастапқы қорғау механизмдері үшін жалған екені дәлелденді. Қауіпсіздік – кез келген қауіпсіздік саясатын табысты жүзеге асырудың қажетті шарты. Іс жүзінде бұл нәтиже қазіргі тауарлық жүйелерді қамтамасыз ету мүмкін емес екенін білдіреді, бірақ мүмкіндіктерге негізделген жүйелерді жеткілікті күтіммен іске асырылса, қамтамасыз ету мүмкін. EROS немесе KeyKOS-қа ешқашан сәтті енген емес, олардың оқшаулау механизмдерін ішкі шабуылшы ешқашан сәтті жеңген емес, бірақ екі іске асыру жеткілікті күтіммен жасалған-жоқпын білуге болмайды. Coyotos жобасының мақсаты компоненттік оқшаулау мен қауіпсіздіктің нақты қол жеткізілгенін бағдарламалық жасақтаманы тексеру әдістерін қолдану арқылы көрсету болды. L4.sec жүйесі, L4 микроядролық отбасының мұрагері, мүмкіндіктерге негізделген жүйе болып табылады және EROS жобасының нәтижелеріне айтарлықтай әсер етті. Әсер өзара, өйткені EROS-тың жоғары өнімді шақыру жөніндегі жұмысы Jochen Liedtke-нің L4 микроядролық отбасымен жеткен жетістіктерімен күшті ынталандырылды.

The overriding goal of the EROS system (and its relatives) is to provide strong support at the operating system level for the efficient restructuring of critical applications into small communicating components. Each component can communicate with the others only through protected interfaces, and is isolated from the rest of the system. A protected interface, in this context, is one that is enforced by the lowest level part of the operating system, the kernel. That is the only part of the system that can move information from one process to another. It also has complete control of the machine and (if properly constructed) cannot be bypassed. In EROS, the kernel provided mechanism by which one component names and invokes the services of another is a capability, using inter process communication (IPC). By enforcing capability protected interfaces, the kernel ensures that all communications to a process arrive via an intentionally exported interface. It also ensures that no invocation is possible unless the invoking component holds a valid capability to the invoked component. Protection in capability systems is achieved by restricting the propagation of capabilities from one component to another, often through a security policy termed confinement. Capability systems naturally promote component based software structure. This organizational approach is similar to the programming language concept of object oriented programming, but occurs at larger granularity and does not include the concept of inheritance. When software is restructured in this way, several benefits emerge:

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-тың негізгі әзірлеушісі Джонатан С. Шапиро болды. Ол сонымен қатар EROS операциялық жүйесінен асып түскен, «эволюциялық қадам» болған Coyotos-тың қозғаушы күші де болды. EROS жобасы 1991 жылы бұрынғы операциялық жүйе KeyKOS-тің таза бөлмеде қайта жасалуы ретінде басталды. KeyKOS Key Logic, Inc. компаниясымен әзірленген және Tymshare, Inc. компаниясы жасаған бұрынғы Great New Operating System In the Sky (GNOSIS) жүйесіндегі жұмыстың тікелей жалғасы болды. Key Logic компаниясының 1991 жылы тарауына байланысты KeyKOS-ке лицензия алу мүмкін болмады. KeyKOS танымал, жеңілдетілген процессорларда жұмыс істемегендіктен, оны қолжетімді құжаттамадан қайта құру туралы шешім қабылданды. 1992 жылдың соңына қарай процессор архитектурасы мүмкіндіктер идеясы енгізілгеннен бері айтарлықтай өзгергені анық болды және компоненттік құрылымды жүйелердің практикалықтығы күмәнді болды. Микроядроға негізделген жүйелер, көптеген процестер мен IPC-ге басымдық беретін жүйелер, өнімділік бойынша қиындықтарға тап болды және оларды шешуге бола ма деген сұрақ туды. x86 архитектурасы басым архитектура ретінде көріне бастады, бірақ 386 және 486 процессорларындағы пайдаланушы/қадағалаушы арасындағы ауысудың жоғары уақыт шығыны процеске негізделген оқшаулау үшін үлкен мәселе тудырды. EROS жобасы зерттеу жұмысына айналды және Шапироның диссертациялық зерттеулерінің негізгі бағыты болу үшін Пенсильвания университетіне көшірілді. 1999 жылға қарай Pentium процессоры үшін жоғары өнімділікке ие нұсқа жасалды, ол IPC жылдамдығымен танымал L4 микроядролық отбасымен тікелей бәсекелесе алды. 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 әртүрлі коммерциялық жобаларда қолданысқа енгізіледі деп күтілуде.