RISC-V сан бичил цөмийн ажиллагааг шалгах тухай RISC-V зааврын багц архитектуртай системүүд дээр. Баталгаажуулалт нь унадаг seL4-ийн үйл ажиллагааны найдвартай байдал нь албан ёсны хэл дээр заасан техникийн үзүүлэлтүүдэд бүрэн нийцэж байгааг харуулж байна. Найдвартай байдлын баталгаа seL4 нь RISC-V RV64 процессор дээр суурилсан чухал ач холбогдолтой системүүд бөгөөд найдвартай байдлын өндөр түвшинг шаарддаг бөгөөд алдаа гарахгүй байх баталгаа юм. seL4 цөм дээр ажиллаж байгаа програм хангамжийг хөгжүүлэгчид системийн аль нэг хэсэгт доголдол гарсан тохиолдолд энэ алдаа нь системийн бусад хэсэгт, ялангуяа түүний чухал хэсгүүдэд тархахгүй гэдэгт бүрэн итгэлтэй байж болно.
seL4 бичил цөмийг анх 32 битийн ARM процессоруудад, дараа нь 64 битийн x86 процессоруудад баталгаажуулсан. Нээлттэй RISC-V техник хангамжийн архитектурыг нээлттэй seL4 микро цөмтэй хослуулснаар аюулгүй байдлын шинэ түвшинд хүрэх болно, учир нь ирээдүйд техник хангамжийн бүрэлдэхүүн хэсгүүдийг бүрэн шалгаж үзэх боломжтой бөгөөд хувийн техник хангамжийн архитектурт хүрэх боломжгүй юм.
SeL4-ийг шалгахдаа тоног төхөөрөмж нь заасан ёсоор ажилладаг бөгөөд техникийн үзүүлэлтүүд нь системийн үйл ажиллагааг бүрэн дүрсэлсэн гэж үздэг боловч бодит байдал дээр төхөөрөмж нь алдаанаас ангид байдаггүй нь таамаглалыг хэрэгжүүлэх механизмд байнга гарч ирдэг асуудлуудаар тодорхой харагдаж байна. зааварчилгаа. Нээлттэй техник хангамжийн платформууд нь аюулгүй байдалтай холбоотой өөрчлөлтүүдийг нэгтгэхэд хялбар болгодог - жишээлбэл, хажуугийн сувгийн алдагдлыг хааж, програм хангамжаас тойрон гарах арга зам хайхаас илүү техник хангамжийн асуудлаас ангижрах нь илүү үр дүнтэй байдаг.
seL4 архитектур гэдгийг санаарай Хэрэглэгчийн орон зайд цөмийн нөөцийг удирдах хэсгүүдийг хөдөлгөж, хэрэглэгчийн нөөцтэй ижил хандалтын хяналтын хэрэгслийг ашиглах. Микро цөм нь файлууд, процессууд, сүлжээний холболтууд болон бусад зүйлсийг удирдахад бэлэн өндөр түвшний хийсвэрлэлүүдийг өгдөггүй, харин физик хаягийн зай, тасалдал, процессорын нөөцөд хандах хандалтыг хянах хамгийн бага механизмаар хангадаг. Техник хангамжтай харилцах өндөр түвшний хийсвэрлэлүүд болон драйверуудыг хэрэглэгчийн түвшний даалгавар хэлбэрээр микро цөмийн дээд талд тусад нь хэрэгжүүлдэг. Ийм даалгаврыг бичил цөмд байгаа нөөцөд хандах хандалтыг дүрмийн тодорхойлолтоор дамжуулан зохион байгуулдаг.
RISC-V нь нээлттэй, уян хатан машин зааврын системээр хангадаг бөгөөд микропроцессоруудыг ашигт малтмалын нөөц ашигласны төлбөр, ашиглахад хавсаргах шаардлагагүйгээр дур зоргоороо ашиглах боломжийг олгодог. RISC-V нь танд бүрэн нээлттэй SoC болон процессор үүсгэх боломжийг олгодог. Одоогийн байдлаар янз бүрийн үнэ төлбөргүй лицензийн дагуу (BSD, MIT, Apache 2.0) өөр өөр компани, нийгэмлэгүүдийн RISC-V техникийн үзүүлэлтэд үндэслэсэн. микропроцессорын цөм, SoC болон аль хэдийн үйлдвэрлэсэн чипүүдийн хэдэн арван хувилбарууд. Glibc 2.27, binutils 2.30, gcc 7, Linux цөм 4.15 хувилбаруудыг гаргаснаас хойш RISC-V дэмжлэг үзүүлж байна.
Эх сурвалж: opennet.ru