Ang proyekto nga nagpalambo sa bukas nga seL4 microkernel nakadawat sa ACM Software System Award, nga gihatagan matag tuig sa Association for Computing Machinery (ACM), ang labing awtoritatibo nga internasyonal nga organisasyon sa natad sa mga sistema sa kompyuter. Ang premyo gihatag alang sa mga nakab-ot sa natad sa matematika nga pruweba sa pagkakasaligan sa operasyon, nga nagpakita sa hingpit nga pagsunod sa mga detalye nga gipiho sa usa ka pormal nga sinultian ug giila ang pagkaandam alang sa paggamit sa mga aplikasyon nga kritikal sa misyon. Gipakita sa proyekto sa seL4 nga dili lamang posible nga hingpit nga pormal nga mapamatud-an ang kasaligan ug seguridad alang sa mga disenyo sa lebel sa operating system sa industriya, apan aron usab makab-ot kini nga wala ikompromiso ang pasundayag ug versatility.
Ang ACM Software System Award gipresentar kada tuig aron sa pag-ila sa pagpalambo sa mga sistema sa software nga adunay usa ka piho nga epekto sa industriya, pagpaila sa bag-ong mga konsepto o pag-abli sa bag-ong mga dapit sa komersyal nga aplikasyon. Ang kantidad sa award mao ang 35 ka libo nga US dolyares. Sa nangaging mga tuig, ang ACM awards nahatag sa mga proyekto sa GCC ug LLVM, ug ang ilang mga founder nga sila si Richard Stallman ug Chris Latner. Giila usab sa award ang mga proyekto ug teknolohiya sama sa UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB ug Eclipse .
Ang seL4 microkernel nga arkitektura talagsaon alang sa paglihok sa mga bahin alang sa pagdumala sa mga kahinguhaan sa kernel ngadto sa luna sa user ug paggamit sa samang access control nga mga himan alang sa mga kapanguhaan sama sa mga kapanguhaan sa user. Ang microkernel wala maghatag ug andam nga gihimo nga taas nga lebel nga abstraction alang sa pagdumala sa mga file, proseso, koneksyon sa network, ug uban pa; hinoon, kini naghatag lamang ug gamay nga mekanismo sa pagkontrolar sa access sa pisikal nga address space, interrupts, ug processor resources. Ang taas nga lebel nga abstraction ug mga drayber alang sa pagpakig-uban sa hardware gipatuman nga gilain sa ibabaw sa microkernel sa porma sa mga buluhaton sa lebel sa user. Ang pag-access sa ingon nga mga buluhaton sa mga kapanguhaan nga magamit sa microkernel giorganisar pinaagi sa kahulugan sa mga lagda.
Source: opennet.ru