A seL4 kernel lehetséges felhasználási területei

Kernel

A napokban nyitották meg (GPLv2) a kutatók a világ első, formális módszerekkel igazolt, általános célú kernelének, a seL4 mikrokernelnek forrását. Felmerülhet a kérdés, hogy vajon mire használható egy ilyen nem szokványos rendszermag. A fenti videó azt mutatja be, hogy hogyan képes a seL4 detektálni és megfelelően lekezelni például egy drone ellen indított cybertámadást.

( zrubi v | 2014. 07. 31., cs – 12:07 )

Érdekes...

de ha maga az eszköz dönti el, hogy melyik parancs támadás, arról egyből a skynet jut eszembe ;)

--
zrubi.hu

( tr3w v | 2014. 07. 31., cs – 12:55 )

Elég BS szagú ez a demo...

"...handing C++ to the average programmer seems roughly comparable to handing a loaded .45 to a chimpanzee." -- Ted Ts'o

( bbandi | 2014. 07. 31., cs – 13:14 )

Én ezt nem értem. Mi köze a kernelnek ahhoz, hogy a "commercially available" drónra be lehet lépni telneten root jogokkal?

Mivel a monolitikus/hibrid kernelnél az eszközkezelés és tsai a kernelen keresztül mennek át, egy alkalmazáshibából adódóan kód/adat injektálható egy másik alkalmazásba, vagy épp a kernel megállásához vezethet.
Pl. Adott egy drón egy vezérlési és egy telemetria csatornával. Egy monolitikus kernellel szerelt drón esetében a telemetria csatorna meghackkelésével, elhasaltatható a kernel, vagy épp át lehet venni az irányítás a vezérlőcsatorna felett. Ehhez csak annyi kell, hogy mondjuk egy a telemetria driverében ismert hibát kihasználva privilégiumszintet tudjon emelni a támadó vagy shellhez juson.
Hogy "lelőjjenek" egy ilyen drónt, elég ha csak a kernelt hasaltatják el, mondjuk egy túlcsordulással.

Mikrokernelnél, a támadó legfeljebb a telemetria alkalmazás futását tudja leállítani, nem tud privilégiumszintet állítani, nem tud kijutni az adott alkalmazásnak kijelölt memóriaterületből. Mivel a kernel nem végez eszközkezelést így a driverek hibájából eredő egymásra hatás is minimalizálható. Pl. A telemetria driverének elhasalása nem vonja maga után a kernel megállását.

Ha hasonlat kell, ott van egy toronyház 120 emelettel, meg egy falu 120 egyszintes házzal. Ha becsapódik egy repülőgép akkor a toronyházat lebontja alapig (a'la WTC), a falu esetében csak a direktben eltalált házakban tud kárt tenni.

Nem az a lényeg, hogy be lehet lépni telneten, hanem az is, hogy milyen útvonalon lép be.

--
"Maradt még 2 kB-om. Teszek bele egy TCP-IP stacket és egy bootlogót. "

IMHO, Linus az igyenszar módszerrel győzedelmeskedett.
Technológiailag a mikro és a makrokernel az alma és a körte esete. Mindegyiknek máshol és más formában van létjogosultsága, egyiket sem lehet abszolút jónak kijelenteni.
--
"Maradt még 2 kB-om. Teszek bele egy TCP-IP stacket és egy bootlogót. "

A vita kb arról szólt, hogy Tanenbaum szerint egy monolitikus kernel nem portolható a jövőben megjelenő architektúrák széles skálájára úgy, hogy az fenntartható, karbantartható marad hosszú távon. A gyakolat cáfolta meg. Az, hogy Linux fut a szuperszámítógépektől a telefonomig, mindenen.

Linus soha nem állította, hogy a mikrokernel abszolút hülyeség, csak Tanenbaum "támadását" hárította. Igaza lett.

Kösz a kifejtést, így sokkal világosabb miért jó egy formálisan ellenőrzött kernel.
Ettől még a videó nagyon bullshitnek tűnik, 2:41-nél annyi látszik a nagy hekkelésből, hogy belépett telneten és lefuttatott egy "killall program.elf"-et.
A behatolásfigyelmeztetés a seL4-esen meg megint spanyol viasznak tűnik.
Szóval látom én hogy jó ez a kernel, de ez a videó inkább befektetőknek meg potenciális felhasználók managereinek szól. Persze azt nyilván nehéz bemutatni hogy ott ül egy blackhat hacker és hümmög, hogy neki ez nem megy :)

Elvileg igaz, de kiváncsi leszek a gyakorlatra.

Első körben olcsóbbnak és biztonságosabbnak tűnik izolált chip-ek tucatját pakolni egy drónba, amik egymással csak erősen korlátozott API-n érintkezhetnek. A mikrokernel API (és így a különböző alrendszerek egymásra gyakorolt hatása) sokkal-sokkal bonyolultabb mint ami a feladathoz optimalizált hardveres izolációval elérhető. Persze ez utóbbinak is megvannak a korlátai, szóval meglássuk..

( solt87 | 2014. 07. 31., cs – 14:58 )

Gondolom, az NSA-kiskapu ebben is alaptartozék, nehogy "kirekesztődjenek" a Pista bácsi szívkütyüjéből, ha netán Pista bácsi terroristának "minősülődne":. :D

========================
Debian Wheezy with LXDE