seL4 nejbezpečnější mikrojádro dneška?

15.10. 05:16 | Programování | poslední úprava: 15.10. 07:49

Google AI mi řekla, že mikrojádro operačního systému seL4 je do dnešního dne nepřekonané v bezpečnosti. Zajímalo by mě, zdali jste ho někdo zkoušel přímo na hardwaru (na železe) a zdali se někde ve východní Evropě snaží o jeho překonání.

seL4 (security enhanced L4) je svobodné jádro operačního systému, přesněji mikrojádro třetí generace, zaměřené na vysokou bezpečnost a spolehlivost...

...seL4 je vyvíjen se zvláštním přihlédnutím k otázkám bezpečnosti a formální bezchybnosti mikrojádra organizací NICTA a dalšími vývojáři. Právě kvůli těmto vlastnostem byl vytvořen vývojový model, který umožňuje ověřit zdrojový kód seL4 ve funkcionálním jazyce Haskell pomocí formálních (matematických) důkazů...

více na české wikipedii

       

Anketa

Komentáře

[dario]

Bezpecne mikrojadro claude oneshotne do pul hodiny mezitim co budu sledovat serialy.

[mirefek]

O tom jsem slyšel -- že to je formálně (matematicky) verifikované. Takže jo, je to vskutku nejbezpečnejší, ale jestli se to dá pro něco opravdu použít, si jistý nejsem. Ale rozhodně jsem zvědavý -- když to zkusíš, tak dej vědět.

[seL4]

A další dotaz bude jak na tom rozjedu Wowko, ne? (Nezkoušel jsem a s Porshe jsem v TESCO na nákupech taky nebyl)

[novomente]

Kdepak Wokna Další dotaz by byl, kdo u nás v Čechách pracuje na podobném operačním systému.

[X]

Ja mam taky dotaz. Kam tim vsim smerujes? Mozna bude jednoduzsi napsat o co ti vlastne jde. Hodne by to urychlilo celou debatu. Hledas praci? Nemas co programovat?

[novomente]

Pracuji na novém programovacím jazyce se zcela novým paradigmatem. Jazyk je určen profesionálním programátorům na programování backendu aplikací. Zamýšlím ho pro procesory rodiny RISC-V, který by měl být srdcem zcela nového počítače. Zajímám se tedy jak o HW tak o operační systém, neboť samotný jazyk vyžaduje právě RISC-V a zcela bezpečné mikrojádro OS.

Našel jsem tedy seL4 a bylo by perfektní, kdyby se takový systém vyvíjel i v Čechách, anebo i na Slovensku.

nm

[Matlák]

Našel jsem tedy seL4 a bylo by perfektní, kdyby se takový systém vyvíjel i v Čechách, anebo i na Slovensku.

Asi není problém udělat fork, přidat do něj podporu své architektury CPU a vypálit protinožcům rybník. Jediná drobnost je že je to pod GPL takže ten vypalovač rybníků pak budeš muset zase zveřejnit, což ovšem nevylučuje že se tvůj CZsel4 stane trhákem

To zcela nové paradigma by mě zajímalo, nových jazyků je poslední dobou jako hub po dešti, ale většinou se používají osvědčená paradigmata.

[novomente]

No právě, že je to vydaný pod GPL.

Škoda, že o novém paradigmatu nemohu mluvit a ani nic ukázat, dokud nebude prog. jazyk hotový.

[Matlák]

No právě, že je to vydaný pod GPL.

To přeci není problém, čerpám z opensource, vracím do opensource, takhle to vždycky fungovalo. Až teď nedávno začaly některé americké firmy zabalovat rozporuplně licencovaný kód do vah v LLM a prodávat to ostatním jako "novou myšlenku". Uzavřením dosáhneš něčeho jedině když budeš někdo jako Altman a ukecáš všechny kolem sebe aby ti do toho tvého tajemného orákula nasypali prachy. To že to orákulum je ve skutečnosti černá díra na jejímž akrečním disku se živíš, to už jim říkat nemusíš, ale chce to umět přesvědčivě lhát a být na správném místě ve správný čas, což se nepodaří každému. Pro ostatní (a obzvlášť pro "one-man-show" projekty) je tu opensource a zveřejnění kódu, které může přitáhnout ty techničtější lidi, co jsou ochotní pomoct.

dokud nebude prog. jazyk hotový

Dle mého, programovací jazyk není nikdy "hotový". Možná tak ve chvíli, kdy jej lidi přestanou používat. Pak je opravdu "hotový"...

[novomente]

Nevadí mi, že je to vydaný jako open source, ale že je to pod licencí GPL. Co když to budu chtít vydat bez jakékoliv licence (což prý nelze), anebo pod jinou svobodnou licencí, která není kompatibilní s GPL?

Dle mého, programovací jazyk není nikdy "hotový". Možná tak ve chvíli, kdy jej lidi přestanou používat. Pak je opravdu "hotový"...

To je taky pravda ale měl jsem na mysli, až bude prog. jazyk připraven k vydání, tedy alespoň verze 0.9, nebo tak něco.

[Want]

Nevadí mi, že je to vydaný jako open source, ale že je to pod licencí GPL.

Tak se jdi vycpat. Nikdo tě nenutí k tomu abys takový kód používal. Když se ti licence nelíbí, si to naprgej sám.

[Robus]

Nevim jestli si te s nekym nepletu, ale nevypiskali te na rootu jako nejvetsiho magora co porad neco vymysli ale nedela? Basix nebo tak nejak?

[novomente]

Jako největšího magora, co pořád něco vymýšlí, ale nedělá, mě nikdo nevypískal. Zveřejnění BASIXu byla fatální chyba, která se se mnou pak již jen táhla. Výsměch sice beru s rezervou, ale neměl jsem pokládat triviální dotazy. Z rootu jsem na čas odešel, abych v klidu pracoval na tom, na čem teď dělám. A když zde budu pokládat inteligentní dotazy, se kterými si AI nebude vědět rady, snad mě i někdo inteligentně odpoví.

A že nic nedělám? Předělat nějakou myšlenku do reality není lehké. To musí vědět každý.

Abych si dokázal ověřit funkčnost jedné myšlenky, neváhal jsem k tomu použít Python. Výsledný kód bych sice mohl zveřejnit, ale jen když o to bude zájem.

[Robus]

Příloha:

• Screenshot 2026-10-17 112005.png (23452 bytů)

aha, tak to jo

[novomente]

Když budeš moudrý a budeš chtít, tak si ten screenshot můžeš vytisknout na samolepku a přilepit na noťase. Ale ty se radši budeš smát. Anebo radši vysmívat?

[Want]

Kdo by stál o tvé vlhké sny..

[novomente]

Nemyslel jsem to zle. Jenom bych nerad, aby mě zde na ABCLinuxu potkal stejný osud, jako na rootu. Tam jsem toho namluvil až, až. A vůbec ničeho nelituji. Snad kromě toho, jestli jsem někoho urazil.

Chybami se člověk učí. Za život jsem udělal spoustu přehmatů. Ale je dobré se zvednout, poučit se z minulosti a jít dál.

Ale to už je moc offtopic.

[Want]

A co sis z té tvé image, kterou sis vybudoval na Rootu, vzal? Jak jsi změnil své chování?

[novomente]

Málo mluvit a více pracovat.

[Olaf]

Tak ukaž, co jsi skutečně udělal. Tady jsi taky kromě řečí vůbec nic neukázal, žádný kód, žádný funkční prototyp.

Talk is cheap. Show me the code.
      ~Linus Torvalds
          ~Michael Scott

[novomente]

Příloha:

• CPU_a_ASM_2026-10-16_v_python3_v3-10.zip (201506 bytů)

Tak jo. Něco ukážu.

Je to nedodělaný, ale nový programovací jazyk, na kterém dělám, a který nesmím zveřejnit, to není.

Naprogramoval jsem si, jak jsem se již zde zmínil, funkcionalitu CPU v Pythonu 3 verze 3.10. Chtěl jsem si ověřit jednu myšlenku a ten kód teď čeká, až ho dodělám.

Když budete mít náladu se na to kouknout (soubor archivu v příloze i s dokumentací), nebuďte šokovaní stylem, jakým jsem to programoval, neboť jsem neměl v té době ani páru o tom, jak se programuje překladač ze zdrojového kódu assembleru do strojových instrukcí naprogramovaného CPU.

Není to nic oslňujícího, tak doufám, že to tu nebude takové fiasko, jako jsem to zažil na rootu.

[Olaf]

Tak jestli je tohle tvoje vizitka, tak bych se tím zrovna nechlubil Na seminárku s odřenýma ušima. Ukaž nám ty revoluční nápady, Wozniaku.

[novomente]

Dobrá dobrá, zvedám bílou vlajku.

[_]

lol buch tě opustil

[novomente]

Ne. Právě naopak. Bůh s velkým 'B' mě neopustil.

[_]

buch tě má za čuraka

[Matlák]

To je pěkný malinký projekt, určitě by se to dalo přepsat do VHDL a zkusit spustit na nějakém malém FPGA. Je poučné si vyzkoušet, jak málo instrukcí stačí k tomu aby byl procesor prakticky použitelný.

Popravdě pořád mi do tohohle nezapadá, že jsi sem psal už před 15 lety, mám dojem, že tohle je věc kterou dělají programátoři když jsou v úplných začátcích a snaží si osahat ty základy, jak vlastně počítač funguje. Můžu se zeptat co jsi dělal v mezičase? Předpokládám nějakou úplnou změnu kariéry?

[novomente]

Upřímně? Hrál jsem online počítačové hry přes den až do pozdní noci, nebo spíše rána. Nic jsem nevymýšlel. Když jsem s hrami skončil, šel jsem na FEL ČVUT studovat software, obor Web a multimedia. Dělal jsem taky statické webové stránky (jen pár projektů), které dnes již neexistující.

Dlouhou dobu jsem tvořil dekorace oken pro MATE, XFCE a další. To mě hodně bavilo. Za použití XML, anebo GIMPu (viz výsledek zde: opendesktop.org)

Vymýšlet různé věci jsem začal před pár lety. To ještě nebyla AI tak rozjetá. Začal jsem více humanitními směry než technickými, jako jsou ekonomie, sociologie, psychologie, náboženství a hlavně filosofie.

Až pak jsem se nedávno pustil do technických záležitostí. Ostatně Steve Jobs tvrdil něco jako, že komu záleží na softwaru, musí se zajímat i o hardware. A měl pravdu. Teď, když je AI asistent, je to snadnější vymýšlet, neboť AI, přestože sama není schopna nic nového vymyslet, poradí věci, které již vymyšlené jsou. Takže se nemusím někde shánět po knížkách a skriptech, abych našel odpovědi. I když musím říct, že v těch knihách a skriptech jsou lepší a ucelenější informace, než kusé informace od AI.

Ten malý projekt "CPU_a_ASM_2026-10-16_v_python3_v3-10" z přílohy jsem dělal bez AI, když pominu, že jsem se AI (Google search) ptal na různé věci, ale kód jsem si od Clauda generovat nenechal. Všechno hezky ručně.

Nové CPU a BASIX jsem dělal s AI (Google a Claude), která mi generovala specifikace. Ale ten nový prograovací jazyk s tím novým paradigmatem již dělám bez AI. Opět pomíjím, že se AI (Google search) ptám na různé věci.

Takže od širokého záběru jsem se teď fokusnul na ten nový jazyk, se kterým jsem začal zhruba před měsícem.

No a to je zhruba tak všechno.

[Matlák]

Rozumím. Hry umí být návykové. Přeju s tím novým paradigmatem hodně štěstí. Přinejmenším věřím že se hodně naučíš.

[novomente]

Děkuju.

[RealJ]

takze novy jazyk, novy cpu, novy OS,... a co tak samoriditelne auto, nebo samoriditelne auto kombinovane s letadlem, ponorkou, kombajnem a marsovskym pristavacim modulem? „A není to málo, Antone Pavloviči" Nic ve zlym, ale doporucoval bych navstevu psychiatra, tohle manicke obdobi muze mit solidni diagnozu.

[novomente]

Na místo létání do vesmíru, hledání mimozemšťanů, stěhování se na jinou planetu apod. bych radši zůstal na Zemi, která je v současnosti ve vážném stavu. Úplně mi postačí nový jazyk, nové CPU, nový OS a nový stroj. To kdybych dokázal zrealizovat (samozřejmě ne sám), tak budu velmi spokojen.

[petr_p]

Doporučuji konzultace v Tachyum s.r.o. Ti mají mnohaleté zkušenosti novým CPU.

[mirefek]

Máš kódítko? Nedávno jsem Claudeho požádal, ať mi implementuje nový programovací jazyk (minimalistický, ve stylu JS, ale víc immutable, a s pár dalšimi featurami jako memoizace), a měl to asi za jeden večer .

Zejména na takovéhle experimenty doporučuju.

[novomente]

Claude je hodně dobrý a hlavně rychlý. Má ale také svoje mouchy, hlavně co se týká bezpečnosti výsledného kódu. Není to tak dávno, co prezident jedné velmoci prohlásil, že každý software, vyrobený v té zemi, musí mít zadní vrátka. Což se snaží, pokud to není již zavedeno, dostat do právního systému. A AI se to týká především.

[Olaf]

Nech ho, už se prý dokázal naučit základy céčka, a prý je to novodobý Steve Wozniak. Revoluce na spadnutí.

[novomente]

Dávám přednost Codasipu. Nikoliv kvůli konzultacím, ale kvůli již hotovýmu novýmu RISC-V čipu.

Jinak Steve Wozniak nejsem. Jsem malý český člověk, co chce něco dokázat, ale sám na to nestačí.

A co se týká revoluce, tak ta už probíhá - války, protesty, manipulace různýho druhu - bez níž se nový řád prý neobejde. I když ten řád bude vypadat jinak, než jak si kdokoliv dokáže dnes představit.

Ale mám dobrou zprávu: Věřím, že

"Čechy a Slovensko se v budoucnosti stanou jedny z technologických velmocí."

Takže to chce být ve správný čas na správném místě.

nm

[_]

takze ke vsemu jeste manlet?