Kad god se povede priča o operativnim sistemima, obično se ode u jednom od dva smera: ili u rasprave tipa Windows protiv Linuxa, ili u tešku akademsku priču koja deluje daleko od stvarnog rada. seL4 je zanimljiv baš zato što uredno izmiče i jednoj i drugoj fioci.

Nije operativni sistem koji bismo sutra stavili na laptop i zaboravili da postoji. Ali nije ni čista teorijska igračka. Njegova vrednost postaje jasna onda kada nas zanima sistem u kome granice između delova moraju da budu precizne, gde odgovornost ne sme da bude zamagljena i gde loš raspored komponenti može da napravi stvaran problem.

Zato je zanimljiv iz vrlo konkretnog ugla. Ne kao odgovor na pitanje 'koji je OS bolji', nego kao odgovor na mnogo korisnije pitanje: kako napraviti mali sistem u kome su izolacija, vlasništvo nad resursima i tajming zaista oblikovani, a ne prepušteni sreći.

Nije poenta da kernel radi sve

Kod seL4 najpre treba skloniti jednu čestu zabludu: poenta nije da sam kernel 'rešava' aplikativnu logiku, kontrolu, bezbednost ili arhitekturu umesto ostatka sistema. Magija ne počinje onog trenutka kada izgovorimo ime formalno verifikovanog jezgra.

Poenta je drugačija. seL4 nas podstiče da ozbiljnije razmišljamo o pitanjima koja drugde lako ostanu zamagljena:

  • ko tačno poseduje koji resurs
  • ko sme da pristupi uređaju, memoriji ili prekidu
  • koji deo sistema sme da padne bez rušenja svega
  • šta je kritična putanja, a šta nije

To je već primetna promena ugla iz kog gledamo arhitekturu.

Zašto je seL4 poseban

seL4 je microkernel. U praksi to znači da se jezgro drži vrlo usko definisanog posla, a da se veći deo sistemske logike namerno izmešta van njega. Umesto velikog monolita koji zna sve i radi svašta, dobijamo manju osnovu i mnogo eksplicitnije granice.

Kratka istorijska digresija

Vredi tu zastati na trenutak, jer priča o microkernelima nije nastala juče. Još od osamdesetih postoji jaka ideja da jezgro treba da bude što manje, a da se servisi, drajveri i veći deo sistemske logike guraju van njega, u odvojene procese sa jasnijim granicama. To nije predstavljano samo kao akademska estetika, nego i kao pokušaj da se dobiju bolja pouzdanost, prenosivost i čišća arhitektura.

U toj priči MINIX je važna stanica. Andrew Tanenbaum ga je napravio 1987. kao sistem za nastavu, uz knjigu Operating Systems: Design and Implementation, da studenti ne uče operativne sisteme samo iz teorije nego i iz stvarnog, čitljivog koda.[1] MINIX nije bio zamišljen kao veliki komercijalni Unix konkurent, nego kao obrazovni sistem koji jasno pokazuje kako je operativni sistem sastavljen. U tome leži veliki deo njegovog istorijskog značaja: bio je napravljen za nastavu, a preko njega su studenti mogli da uče unutrašnjost operativnih sistema iz stvarnog koda. Za Linusa Torvaldsa postoje i javni tragovi da je koristio MINIX dok je radio na ranim kernel eksperimentima, a i sama istorija MINIX-a navodi ga kao jednog od ranih korisnika.[1][2][3]

Odatle dolazi i čuvena Tanenbaum-Torvalds rasprava iz januara 1992. na comp.os.minix.[4] Tanenbaum je tada tvrdio da je monolitni kernel, kakav je Linux tada bio, korak unazad i da microkernel pravac dugoročno ima više smisla. Torvalds je uzvratio iz mnogo pragmatičnije pozicije: važno mu je bilo da sistem radi dobro na tadašnjem hardveru, da bude upotrebljiv i da ne bude paralisan arhitektonskom čistotom. Ta rasprava se danas često navodi kao klasičan primer napetosti između elegantne arhitekture i praktičnog inženjerskog kompromisa.

A onda dolazi ono po čemu se seL4 danas najčešće prepoznaje: formalna verifikacija određenih svojstava jezgra.[5] Ne treba od toga praviti religiju, ali ne treba ni umanjivati značaj. U svetu sistemskog softvera to ga izdvaja od velikog dela uobičajenog softverskog okruženja. Ako nam je stalo do toga da najniži sloj sistema bude ne samo 'verovatno dobar', nego i strože analiziran, onda seL4 prirodno privlači pažnju.

Ovde je važan i pristup otvorenog koda.[5] Poenta nije da bezbednost počiva na skrivenosti implementacije, nego da mehanizmi, granice i tvrdnje budu otvoreni za proveru. To je blisko onome što se danas često sažima kao Shannonova maksima: bezbednost sistema ne bi trebalo da zavisi od tajnosti njegovog dizajna. Drugim rečima, skrivenost nije isto što i bezbednost.

Baš zato ovo danas dobija dodatnu težinu i zbog AI okruženja. Što više u sisteme ugrađujemo modele, agente i slojeve koji su po prirodi složeni, mutniji i teži za potpuno objašnjavanje, to više vrede discipline koje je microkernel svet dugo gajio: stroge granice, najmanji potrebni autoritet, proverljiva svojstva i jasno razdvojene odgovornosti. I to nije važno samo u svetu operativnih sistema. Te navike mogu da se vežbaju i u dizajnu servisa, bezbednosnih granica, agentskih sistema i AI-potpomognutog razvoja. Ako je gornji deo sistema neizbežno neuredniji, još je važnije da osnova ne bude.

Druga važna stvar je capability model. Umesto mutne predstave da 'sistem nekako ima pristup svemu', pristup resursima modeluje se mnogo eksplicitnije.[6] A to je zdrava disciplina, naročito kad sistem ima više delova koji ne bi trebalo da dele istu moć.

Gde to postaje stvarno korisno

Baš tu priča prestaje da bude slogan i postaje inženjersko pitanje. Kada je spustimo na mali sistem koji stvarno mora da radi, raspored delova odjednom više nije apstraktna tema.

Zamislimo sistem koji ima:

  • deo koji obrađuje kritičan posao u kratkom roku
  • deo koji upravlja uređajima ili spoljnim resursima
  • deo koji prima komande i spoljne događaje
  • deo koji vodi stanje i konfiguraciju
  • deo koji samo beleži metrike i dijagnostiku

Odmah više nije svejedno kako smo to rasporedili.

Ako sporo beleženje logova može da koči deo koji mora da ispoštuje rok, to je obično znak loše arhitektonske podele. Ako komponenta za dijagnostiku može da ugrozi kritičnu putanju, sistem nije zreo koliko god lepo izgledao na papiru. Ako granice nisu jasne, priča o ograničavanju posledica kvara ostaje prazna reč.

Tu seL4 postaje zanimljiv ne zato što pripada nekoj uskoj niši, nego zato što nas tera da granice, odgovornosti i kritične putanje crtamo ozbiljnije.

Od velikih reči do malog sistema

Zato je korisno da se ne kreće od prevelikog sistema, nego od malog sklopa u kome su granice već stvarne. Ne od svega odjednom, nego od nekoliko jasno razdvojenih delova koji nas prisiljavaju da odgovorimo na prava pitanja: da li je podela zdrava, da li su odgovornosti jasne i da li kritični deo sistema zaista može da diše bez oslanjanja na sporiji i bučniji ostatak.

Takav pristup deluje mnogo poštenije od velikih obećanja.

Zašto ovo nije samo za uski krug ljudi

Lako je pomisliti da su ovakve teme rezervisane samo za ljude koji već rade blizu jezgra sistema. Ali razlog zbog kog seL4 zaslužuje šire interesovanje jeste upravo obrnut: on tera da se neka arhitektonska pitanja, važna gotovo svuda, vide u čistijem obliku.

Na primer:

  • šta je stvarno kritično u sistemu
  • šta sme da bude sporo ili restartabilno
  • gde je granica odgovornosti
  • koliko sitne komponente mogu da budu, a da sistem ostane objašnjiv

To su dobra pitanja i izvan seL4 sveta. seL4 ih samo čini manje maglovitim.

Gde je zdrava mera

Vredi odmah reći i šta seL4 nije.

Nije prečica koja nas oslobađa potrebe da razumemo svoj domen. Nije zamena za loš algoritam, lošu podelu posla ili nerealna očekivanja od hardvera. Nije ni automatski najbolji izbor za svaki sistem.

Ali ako hoćemo da pravimo male ili srednje sisteme u kojima su izolacija, restartabilnost, vlasništvo nad resursima i granice između kritičnog i nekritičnog dela zaista prve klase arhitekture, onda je seL4 vredan ozbiljne pažnje.

To je možda i najbolji razlog da mu se čovek vrati bez mitologije i bez podsmeha.

Šta sledi

Ako sve ovo zvuči iole zanimljivo, sledeće logično pitanje nije 'kako da odmah napravimo veliki sistem', nego mnogo skromnije i korisnije: kako izgleda prvi mali sistem koji već ima zdrave granice.

Izvori

  1. MINIX istorija i nastavna namena: https://wiki.minix3.org/doku.php?id=www:documentation:read-more
  2. Linus Torvalds, jul 1991, 'project I'm working on (in minix)': https://groups.google.com/g/comp.os.minix/c/T9SjMGTSpXk/m/0C2oixEP6qQJ
  3. Linus Torvalds, avgust 1991, objava korisnicima MINIX-a o ranom Linuxu: https://groups.google.com/g/comp.os.minix/c/dlNtH7RRrGA/m/ru3QgAOM-7UJ
  4. Andy Tanenbaum, januar 1992, 'LINUX is obsolete': https://groups.google.com/group/comp.os.minix/msg/6372404c547d7ab4
  5. Zvanični seL4 sajt, formalna verifikacija i jake bezbednosne granice: https://sel4.systems/
  6. seL4 dokumentacija, capability model: https://docs.sel4.systems/Tutorials/capabilities.html