Mradi wa seL4 open microkernel umepokea Tuzo la Mfumo wa Programu wa ACM, tuzo ya kila mwaka inayotolewa na Chama cha Mashine za Kompyuta (ACM), shirika linaloheshimika zaidi la kimataifa katika nyanja ya mifumo ya kompyuta. Tuzo hilo hutolewa kwa mafanikio katika nyanja ya uthibitisho wa utendakazi wa hisabati, ambayo huonyesha utiifu kamili wa vipimo vilivyotolewa katika lugha rasmi na kutambua utayari wa kutumika katika matumizi muhimu ya dhamira. Mradi wa seL4 umeonyesha kuwa haiwezekani tu kuthibitisha kikamilifu kuegemea na usalama kwa miradi katika ngazi ya mifumo ya uendeshaji ya viwanda, lakini pia kufikia hili bila kutoa sadaka ya utendaji na matumizi mengi.
Tuzo la Mfumo wa Programu wa ACM hutolewa kila mwaka ili kutambua uundaji wa mifumo ya programu ambayo imekuwa na athari dhahiri kwenye tasnia, kuanzisha dhana mpya au kufungua programu mpya za kibiashara. Kiasi cha tuzo hiyo ni dola elfu 35 za kimarekani. Katika miaka iliyopita, tuzo za ACM zimetolewa kwa miradi ya GCC na LLVM, na waanzilishi wake Richard Stallman na Chris Latner. Miradi na teknolojia nyingine ambazo zimetambuliwa ni pamoja na UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB, na Eclipse.
Usanifu wa microkernel ya seL4 inajulikana kwa kuondolewa kwa sehemu za kudhibiti rasilimali za kernel katika nafasi ya mtumiaji na kwa kutumia njia sawa za udhibiti wa ufikiaji kwa rasilimali kama vile rasilimali za watumiaji. Microkernel haitoi vifupisho vya hali ya juu vya kudhibiti faili, michakato, miunganisho ya mtandao na kadhalika, badala yake hutoa njia ndogo tu za kudhibiti ufikiaji wa nafasi ya anwani halisi, kukatizwa na rasilimali za kichakataji. Vidokezo vya hali ya juu na viendeshaji vya kuingiliana na maunzi hutekelezwa kando juu ya maikrofoni kwa namna ya kazi za kiwango cha mtumiaji. Ufikiaji wa kazi hizo kwa rasilimali zinazopatikana kwa microkernel hupangwa kupitia ufafanuzi wa sheria.
Chanzo: opennet.ru