Muen Separation Kernel

Kernel

A fejlesztői szerint a Muen Separation Kernel "a világ első nyílt forrású mikrokernele, amely formálisan bizonyítottan nem tartalmaz runtime error-t forráskód szinten". A svájci University of Applied Sciences Rapperswil egyetem Institute for Internet Technologies and Applications intézményében fejlesztett kernelt kifejezetten úgy tervezték, hogy az megfeleljen Intel x86/64 platformon "high-assurance" rendszerek kihívást jelentő magas követelményeinek. A fejlesztők, hogy biztosak legyenek abban, hogy a Muen megfelelő alap kritikus rendszerekhez, együttműködtek a német secunet Security Networks AG céggel.

A Muen funkciói, jellemzői:

  • Minimal SK for the Intel x86/64 architecture written in the SPARK language
  • Full availability of source code and documentation
  • Proof of absence of runtime errors
  • Multicore support
  • Nested paging (EPT) and memory typing (PAT)
  • Fixed cyclic scheduling using Intel VMX preemption timer
  • Static assignment of resources according to system policy
  • Event mechanism
  • Minimal Zero-Footprint Run-Time (RTS)
  • Support for 64-bit native and 32-bit VM subjects

A Muen a GPLv3 és későbbi verziói által meghatározott feltételek szerint terjeszthető. Részletek a projekt honlapján.

( freeoli v | 2014. 01. 23., cs – 13:19 )

Olvastam már róla, de nem gondoltam volna, hogy termék is lesz belőle.

( wachag | 2014. 01. 23., cs – 13:40 )

> "a világ első nyílt forrású mikrokernele, amely formálisan bizonyítottan nem tartalmaz runtime error-t forráskód szinten"

Ez szépen hangzik, csak élek a gyanúval, hogy a gyakorlatban semmit nem érsz ezzel az állítással. Avagy subscribe.

Egy kernel is lehet, de mondjuk annyit feltetlenul meg kell jegyzni, hogy a proven-in-use egy statisztikai valoszinuseget feltetelez, ok pedig ha jol ertem matematikailag bizonyitjak a hibamentesseget. Tehat az utobbi az elmelet helyessege eseten biztosan hibamanetes, a masik esetben pedig egy statisztikai uton kozelito hibamentesseget feltetelezunk. (Durva hiba, ami egy altalanos hasznalat eseten felmerulne nem varhato.) Ez compilerek es hardware chipek eseten azert jol hasznalhato, mert altalabn szeles korben hasznaltak, es a specifikaciojuk (a felhasznalo szemszogebol) jelllemzoen egyertelmu.

Nem értem a problémádat. Azt _nem_ jelentette ki senki, hogy egy olyan platformot hoztak létre, amelynél bizonyított, hogy nem fordulhat elő hibás működés.

Arról volt szó, hogy a kernel forráskódja futás idejű hiba lehetőségétől mentes. Nyilván hibás lesz a működés, ha hibás hardveren futtatják vagy ha a fordító hibát tesz bele.

Ez csak az első lépés. Szerintem fordítót "simán" lehet szintén bizonyítottan helyeset írni. A hardverre ugyanez eljátszható (HDL nyelv és bizonyítottan jó "fordító"). A gyártási hibák kizárása történhet pl. elektronkmikroszkóppal, a későbbiekben történő, környezeti behatásokból eredeő meghibásodás ellen pedig lehet redundanciával védekezni.
Biztosan nem egyszerű feladat, de ha valamiért igény lenne rá, biztos akadna, aki megcsinálja.

Tetszőleges mennyiségű komponensről tudod bizonyítani, hogy hibátlan, az összesről nem. Innentől kezdve szerintem csak elméletben érdekes, ott viszont igen.

Azt a tévedést érzem bennetek, hogy feltételezitek, hogy ha kizárjuk egy komponens hibalehetőségét, akkor biztosan jobb lesz a rendszer. Na ez nem feltétlen igaz. Mert lehet, hogy pont emiatt érzékenyebb lesz egy másik komponens hibájára (értsd: ő magától nem hibásodhat meg, de a másik hibája okozhat kritikus állapotot. Szóval hiába bizonyítod formálisan a hibamentességet, az alatta/fölötte levő részegységek ugyanannyira hibázóvá tehetik).

Azert azzal az ervelessel nem igazan tudok egyeterteni, hogy ha egy komponens hibatalan a rendszer akar hibaerzekenyebbe is valaht. Ez azert igy meredek.

Ami viszont lenyeges szempont: milyen hibakkal szemeben szeretnenk minel nagyobb hibamentesseget elerni.

Ha pl. security szempotnbol nezzuk a dolgot akkor eleg ritka, hogy chip hibabol adodoan torjenek egy rendszert. Jellemzoen az opracios rendszer valamely hibajat hasznaljak. Itt jelentos mertekben javit a helyzeten a kernel hibamentessege. Persze nyilvan van meg egy csomo szoftver komponens, de azert a kernel sokat tehet a security erdekeben.

Ha pl. safety-rol beszelunk ott a kernel hibamentessege nem rossz dolog hiszen azt allithatjuk, hogy abban a komponensben nincs szisztematikus hiba, de hat a safety eseteben a veletlenszeru hardware hibak kikuszobolese izgalamasabb tema, es rogton a statisztikai megkozelitesnel talaljuk maunkat. Termeszetesen a hardwareben is lehetnek szisztematikus hibak, ezek szuresere is megvannak a modszerek. A hibemanetesseg matematikai bizonyitasa nem lenne rossz, de meg a gyakorlatban nem talalkoztam vele.

akkor eleg ritka, hogy chip hibabol adodoan torjenek egy rendszert.
Azért az USB és firewire kontroller bugokról (illetve bennfelejtett debug feature-ökről) ne feledkezzünk el. Ezeknek azért van gyakorlati relevanciája is, nemcsak elméleti lehetőségként tartják számon őket.
P1-es időkben is voltak ilyen F00F, COMA bug és hasonlók, amikkel legalábbis DoS-olni lehetett gépeket.
Emlékeim szerint DRM rendszerek esetén is voltak példák hardverhibákra alapozott törésekre. Azt hiszem pl az Xbox360 esetén használtak ki valami címzési anomáliát a processzorban, hogy kikerüljék a kód autentikációt.

Az utolsó példánál maradva sokszor van, hogy a hardverhiba és szoftverhiba között nehéz különbséget tenni. Minek számít az, ha a hardvernek van valami nyakatekert hülyesége, amit szoftverrel elvileg lehetne workaroundolni, de a fejlesztők nem tudnak róla/nem gondolnak rá, hogy jelentősége lehet/nem tartották fontosnak?
---
Régóta vágyok én, az androidok mezonkincsére már!

Ezt a bejelentést most nem olvastam végig, de pár éve volt már itt is hír egy L4-type formálisan ellenőrzött mikrokernelről (az noncommercial, ez most open source, mielőtt valaki meglátja hogy mind a kettő világelső) és ott jól összeszedték, mire terjed ki a bizonyítás, mire nem, és milyen körülményeket feltételeznek: http://ertos.nicta.com.au/research/l4.verified/proof.pml

Konklúzió ami ide is érvényes:
We have made these assumptions to fit into the carefully limited scope and the limited resources of a major research project. These specific assumptions are not a limitation of the general formal verification approach. In theory, it is possible to eliminate all of them: there are successful verification projects showing the correctness of even optimising C compilers; there are at least two prominent research groups that have demonstrated successful formal verification of assembly code and low-level hardware management functions; we have ourselves proved an earlier version of the boot code correct down to the level of a precise, executable specification; and we have a separate formalisation of ARM11 virtual memory from first principles. There are still significant scientific challenges in unifying all of these into a single framework, but it is clear at this point that it can be done.

( utpKabel | 2014. 01. 24., p – 08:18 )

A Hochschule für angewandte Wissenschaften (szokásos angol fordítása: University of Applied Sciences) magyarul főiskola. A másik szokásos elnevezés a Fachhochschule.

A Wikipédia szerint is így van, szóval tuti jól mondtam.

( utpKabel | 2014. 01. 24., p – 08:25 )

Most komolyan, GPLv3? Miért nem használnak inkább valami permissive licencet? Félnek attól, hogy valaki hasznos dologra (haszonszerzésre) használja majd a terméküket?

Miért kellene ennyire engedékeny licencet választaniuk? Beleteszik az időt, pénzt és a kódot is megnyitják, de ez nem elég. A cél legyen mindig más for profit cégek támogatása feltételek nélkül? Miért? A for profit cégen kívül kinek lenne ez jó?

A GPL pont a közkincset gyarapítja.

Nyugodtan használják fel, és adják ki a forrását a cuccuknak. És éljenek meg a szolgáltatásból meg a hardver forgalmazásból.

A Linux kernelnél is biztos vagyok benne hogy pont ez számít, mikor valaki arról dönt, hogy hosszú távon folyamatosan belefeccel munkát. Tudja hogy nem fog eltűnni az általa létrehozott értékre alapozott jövőbeli munka, hanem a terjesztésnél meg kell osztani. Hiszem hogy a Linux kernel sem tartana ott ahol, GPL nélkül.

Az implicit (le nem írt) állításokat nem vitatom.

Az például egy ilyen le nem írt állítás, hogy egy "for profit" cég nem kooperálhat az egyetemmel egy zárt forrású piaci termék létrehozásának érdekében.

Baj az, ha egy ilyen együttműködésből az egyetem is nyerne, nem csak a "for profit" cég?

De nem ők fektették bele a munkát. Ez a más nemi szervével csollány csapkodás esete.

Egyébként meg el tudok képzelni esetet, amikor a fejlesztők rosszabbul járnának BSD licencel. Pl. több cég felkapja a terméket a konkurenciából -> nagyobb verseny -> hamarabb telítődik a piaca a terméknek.

> Most komolyan, GPLv3? Miért nem használnak inkább valami permissive licencet?

Nekem a GPL-ről a kaláka jut az eszembe http://mek.oszk.hu/02100/02115/html/2-1770.html

"A közösség bármelyik tagja akármikor visszahívhatja a megsegítettet, s az a munka visszaadását, a kalákában való részvételt kötelességének tartja."

"A kaláka megléte valamely közösségben a közösség egységét, bizonyos fokú homogenitását jelzi."

Vagyis szerintem azért választottak GPL-t, mert kalákában szeretnének a témán dolgozni.