RISC-V Foundation mahitungod sa pag-verify sa operasyon sa microkernel sa mga sistema nga adunay RISC-V instruction set architecture. Ang pag-verify moabot sa kasaligan sa seL4 nga operasyon, nga nagpakita sa bug-os nga pagsunod sa mga detalye nga gipiho sa pormal nga pinulongan. Pamatuod sa pagkakasaligan seL4 sa mission-critical nga mga sistema nga gibase sa RISC-V RV64 nga mga processor nga nagkinahanglan og dugang nga lebel sa pagkakasaligan ug garantiya nga walay mga kapakyasan. Ang mga nag-develop sa software nga nagdagan sa ibabaw sa seL4 kernel mahimong hingpit nga masaligon nga kung adunay kapakyasan sa usa ka bahin sa sistema, kini nga kapakyasan dili mokaylap sa nahabilin nga sistema ug, labi na, ang mga kritikal nga bahin niini.
Ang seL4 microkernel sa sinugdan gi-verify alang sa 32-bit ARM processors, ug sa ulahi alang sa 64-bit x86 processors. Namatikdan nga ang kombinasyon sa bukas nga RISC-V hardware nga arkitektura nga adunay bukas nga seL4 microkernel makab-ot ang usa ka bag-ong lebel sa seguridad, tungod kay ang mga sangkap sa hardware mahimo usab nga hingpit nga mapamatud-an sa umaabot, nga imposible nga makab-ot alang sa proprietary hardware nga mga arkitektura.
Kung gipamatud-an ang seL4, gituohan nga ang mga ekipo molihok sama sa gipahayag ug ang detalye hingpit nga naghulagway sa pamatasan sa sistema, apan sa tinuud ang kagamitan dili gawasnon sa mga sayup, nga tin-aw nga gipakita sa kanunay nga mga problema nga mitumaw sa mekanismo sa espekulatibo nga pagpatuman sa mga instruksyon. Ang bukas nga mga plataporma sa hardware nagpasayon ββsa pag-integrate sa mga kausaban nga may kalabutan sa seguridad - pananglitan, sa pagbabag sa tanang posibleng side-channel leaks, diin mas episyente ang pagtangtang sa problema sa hardware kaysa pagsulay sa pagpangita og mga workaround sa software.
Hinumdomi nga ang seL4 nga arkitektura pagbalhin sa mga bahin alang sa pagdumala sa mga kahinguhaan sa kernel ngadto sa wanang sa gumagamit ug paggamit sa parehas nga paagi sa pagkontrol sa pag-access alang sa mga kapanguhaan sama sa mga kapanguhaan sa gumagamit. 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.
Ang RISC-V naghatag ug bukas ug flexible nga sistema sa instruksiyon sa makina nga nagtugot sa mga microprocessor nga matukod alang sa arbitraryong mga aplikasyon nga wala magkinahanglan og royalties o mga kuwerdas nga gilakip sa paggamit. Gitugotan ka sa RISC-V sa paghimo sa hingpit nga bukas nga mga SoC ug mga processor. Sa pagkakaron base sa RISC-V nga espesipikasyon sa lain-laing mga kompanya ug komunidad ubos sa nagkalain-laing mga libre nga lisensya (BSD, MIT, Apache 2.0) pipila ka dosena nga mga variant sa microprocessor cores, SoCs ug nahimo na nga mga chips. Ang suporta sa RISC-V anaa na sukad sa pagpagawas sa Glibc 2.27, binutils 2.30, gcc 7, ug ang Linux kernel 4.15.
Source: opennet.ru