- 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.
- A hozzászóláshoz be kell jelentkezni
Hozzászólások
Olvastam már róla, de nem gondoltam volna, hogy termék is lesz belőle.
- A hozzászóláshoz be kell jelentkezni
> "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.
- A hozzászóláshoz be kell jelentkezni
A világ a másik oldaláról közelíti meg, runtime error detection, auto service redtart, stb :D Vagyis lehet szar, de átlagolva jónak kell lennie.
- A hozzászóláshoz be kell jelentkezni
Ezt kifejtenéd bővebben?
- A hozzászóláshoz be kell jelentkezni
Ha jól értettem: formálisan bizonyították, hogy a forrás szinten nem tartalmaz runtime hibát.
Na és a fordítóról bizonyították? A hardverről bizonyították? Stb.
- A hozzászóláshoz be kell jelentkezni
A fordito es a hardware tekintheto proven-in-use-nak, ha elegendoen szeles korben hasznalt.
- A hozzászóláshoz be kell jelentkezni
Ezzel az érveléssel: akkor egy kernel miért nem?
- A hozzászóláshoz be kell jelentkezni
Nem használják elég széleskörűen. :)
- A hozzászóláshoz be kell jelentkezni
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.
- A hozzászóláshoz be kell jelentkezni
Lehet, hogy írtak egy fordítót - assembly-ben - amiről bizonyították :)
A hardverről meg nem kell bizonyítani, mert az nem része az oprendszernek.
- A hozzászóláshoz be kell jelentkezni
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.
- A hozzászóláshoz be kell jelentkezni
Magyarul: a gyakorlatban nem érsz a formális bizonyítással semmit, mert a láncban más elemek is vannak.
Az megint más, hogy a módszer, a kutatás értékes.
- A hozzászóláshoz be kell jelentkezni
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.
- A hozzászóláshoz be kell jelentkezni
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).
- A hozzászóláshoz be kell jelentkezni
Én inkább ott fognám meg, hogy mi van, ha a helyességfeltevésben van a hiba. Tehát a komponensünk
megfelel annak, ami feltételt írtunk, de tényleg jól írtuk-e le?
- A hozzászóláshoz be kell jelentkezni
A specifikacios hiba ugyanugy szoftver hiba. Erre van a review es a validalas.
- A hozzászóláshoz be kell jelentkezni
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.
- A hozzászóláshoz be kell jelentkezni
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!
- A hozzászóláshoz be kell jelentkezni
Autos hasonlat jo lesz?
t
- A hozzászóláshoz be kell jelentkezni
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.
- A hozzászóláshoz be kell jelentkezni
szemantikailag meg ki tudja :)
--
NetBSD - Simplicity is prerequisite for reliability
- A hozzászóláshoz be kell jelentkezni
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.
- A hozzászóláshoz be kell jelentkezni
Svájcban a Fachhochschule az műszaki egyetem, nem főiskola...
- A hozzászóláshoz be kell jelentkezni
Nem. A technische Hochschule jelenthet műszaki egyetemet.
- A hozzászóláshoz be kell jelentkezni
Ne okoskodj. Nem az a lényeg, hogy mi a neve, hanem az, hogy ad MSc-t. Itthon az ilyent egyetemnek nevezzük, angolban is Universityt használják, és amúgy még két kolléga is lakott az irodámban onnan, és ők is Universität-ként hivatkoztak rá.
- A hozzászóláshoz be kell jelentkezni
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?
- A hozzászóláshoz be kell jelentkezni
Mitől ne tudná más haszonszerzésre használni?
- A hozzászóláshoz be kell jelentkezni
A GPLv3 nem zarja ki az uzleti hasznalatot.
--
Ki oda vagyik, hol szall a galamb, elszalasztja a kincset itt alant.
- A hozzászóláshoz be kell jelentkezni
Nem zárja ki, csak korlátozza a lehetséges üzleti modelleket... ergo bizonyos esetekben kizárja.
- A hozzászóláshoz be kell jelentkezni
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.
- A hozzászóláshoz be kell jelentkezni
De ez egy kutatómunka, nekik az az érdekük, hogy cikket publikáljanak róla. Emellett örülniük kellene, ha bárki anyagi hasznot tud előállítani belőle, hiszen akkor ez nem csak a tudósok szórakozása lesz, hanem közvetlenül is hasznos.
- A hozzászóláshoz be kell jelentkezni
Hasznosíthatja bárki.
Idegen, for profit cégek feltétel nélküli támogatása miért jó?
- A hozzászóláshoz be kell jelentkezni
Idegen for profit cégek nem fognak publikációt írni belőle, ergo nem vetélytársak. Miért fáj az, ha a másik jól jár?
- A hozzászóláshoz be kell jelentkezni
Miért fáj az, ha értesülni szeretnének a használatba vételkor felmerülő problémákról, és a megoldásukról?
- A hozzászóláshoz be kell jelentkezni
A GPLv3 nem kötelez semmiféle értesítésre.
- A hozzászóláshoz be kell jelentkezni
Valóban. És mi következik ebből? Mer a mondanivalót kifelejtetted.
- A hozzászóláshoz be kell jelentkezni
... értesülni szeretnének a ...
Az következik, hogy értelmetlen volt az előző kérdésed.
- A hozzászóláshoz be kell jelentkezni
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?
- A hozzászóláshoz be kell jelentkezni
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.
- A hozzászóláshoz be kell jelentkezni
De nem ők fektették bele a munkát.
De igen, ha továbbfejlesztik, és úgy árulják. Ha pedig nincs hozzáadott érték, akkor valóban ugyanúgy árulhatják a GPL-es változatot is.
- A hozzászóláshoz be kell jelentkezni
> 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.
- A hozzászóláshoz be kell jelentkezni
Common Criteria megfelelőség?
- A hozzászóláshoz be kell jelentkezni