AArch64 зааврын багц архитектуртай системүүд дээрх seL4 микрокернелийн найдвартай байдал, аюулгүй байдлын албан ёсны математикийн баталгаажуулалтын ажил дууссан. Баталгаажуулалт нь албан ёсны хэл дээр тодорхойлсон техникийн үзүүлэлтүүдтэй бүрэн нийцэж байгааг харуулсан seL4 үйлдлийн зөв байдлын математикийн баталгаанаас бүрдэнэ. Энэхүү найдвартай байдлын нотолгоо нь өндөр түвшний аюулгүй байдал шаарддаг, алдаа гарахгүй байхыг баталгаажуулдаг ARM64 процессорууд дээр суурилсан чухал системүүдэд seL4-ийг ашиглах боломжийг олгодог.
seL4 микрокернелийг анх 32 битийн ARM процессоруудад, дараа нь 64 битийн x86 болон RISC-V процессоруудад баталгаажуулсан. Баталгаажуулалт нь системийн нэг хэсэгт алдаа гарсан тохиолдолд системийн үлдсэн хэсэг болон түүний чухал бүрэлдэхүүн хэсгүүдэд тархахгүй байхыг баталгаажуулдаг. Аюулгүй байдлын үүднээс баталгаажуулалт нь цөм нь програмын тусгаарлалтын зохих түвшинг хангаж, зөвшөөрөлгүйгээр мэдээлэлд хандахаас сэргийлж, хоёрдогч програмууд эвдэрсэн тохиолдолд халдлага чухал програмуудад тархахгүй байхыг баталгаажуулдаг.
seL4 бичил цөмийн архитектур нь цөмийн нөөцийн удирдлагыг хэрэглэгчийн орон зайд шилжүүлж, хэрэглэгчийн нөөцтэй адил эдгээр нөөцөд хандах хяналтын механизмыг ашигладгаараа онцлог юм. Микро цөм нь файлууд, процессууд, сүлжээний холболтууд болон бусад зүйлсийг удирдахад бэлэн өндөр түвшний хийсвэрлэлүүдийг өгдөггүй; үүний оронд энэ нь физик хаягийн орон зай, тасалдал, процессорын нөөцөд хандах хандалтыг удирдах хамгийн бага механизмаар хангадаг. Техник хангамжтай харьцах өндөр түвшний хийсвэрлэлүүд болон драйверууд нь хэрэглэгчийн түвшинд ажиллаж байгаа ажлуудын хувьд микро цөмийн дээд талд тусад нь хэрэгждэг. Эдгээр даалгавруудаар микро цөмийн нөөцөд хандах хандалтыг дүрмийн тодорхойлолтоор дамжуулан зохион байгуулдаг.
Эх сурвалж: opennet.ru
