មីក្រូខឺណែល seL4 ត្រូវបានផ្ទៀងផ្ទាត់តាមគណិតវិទ្យាសម្រាប់ស្ថាបត្យកម្ម RISC-V

មូលនិធិ RISC-V រាយការណ៍ អំពីការផ្ទៀងផ្ទាត់ប្រតិបត្តិការរបស់ microkernel seL4 នៅលើប្រព័ន្ធដែលមានស្ថាបត្យកម្មសំណុំការណែនាំ RISC-V ។ ការផ្ទៀងផ្ទាត់ចុះមក ភស្តុតាងគណិតវិទ្យា ភាពជឿជាក់នៃប្រតិបត្តិការ seL4 ដែលបង្ហាញពីការអនុលោមពេញលេញជាមួយនឹងលក្ខណៈជាក់លាក់ដែលបានបញ្ជាក់នៅក្នុងភាសាផ្លូវការ។ ភស្តុតាងនៃភាពជឿជាក់ អនុញ្ញាតឱ្យអ្នកប្រើ seL4 នៅក្នុងប្រព័ន្ធសំខាន់នៃបេសកកម្មដោយផ្អែកលើប្រព័ន្ធដំណើរការ RISC-V RV64 ដែលតម្រូវឱ្យមានការកើនឡើងនូវកម្រិតនៃភាពជឿជាក់ និងធានាអវត្តមាននៃការបរាជ័យ។ អ្នកបង្កើតកម្មវិធីដែលដំណើរការលើខឺណែល seL4 អាចមានទំនុកចិត្តទាំងស្រុងថាប្រសិនបើមានការបរាជ័យនៅក្នុងផ្នែកមួយនៃប្រព័ន្ធ នោះការបរាជ័យនេះនឹងមិនរាលដាលដល់ប្រព័ន្ធដែលនៅសល់ឡើយ ហើយជាពិសេសផ្នែកសំខាន់ៗរបស់វា។

មីក្រូខឺណែល seL4 ត្រូវបានផ្ទៀងផ្ទាត់ដំបូងសម្រាប់ប្រព័ន្ធដំណើរការ ARM 32 ប៊ីត ហើយក្រោយមកសម្រាប់ដំណើរការ 64 ប៊ីត x86 ។ វាត្រូវបានកត់សម្គាល់ថាការរួមបញ្ចូលគ្នានៃស្ថាបត្យកម្មផ្នែករឹង RISC-V បើកចំហជាមួយមីក្រូខឺណែល seL4 បើកចំហនឹងសម្រេចបាននូវកម្រិតសុវត្ថិភាពថ្មីមួយ ដោយសារសមាសធាតុផ្នែករឹងក៏អាចត្រូវបានផ្ទៀងផ្ទាត់យ៉ាងពេញលេញនាពេលអនាគត ដែលវាមិនអាចទៅរួចទេសម្រាប់ស្ថាបត្យកម្មផ្នែករឹងដែលមានកម្មសិទ្ធិ។

នៅពេលផ្ទៀងផ្ទាត់ seL4 វាត្រូវបានសន្មត់ថាឧបករណ៍ដំណើរការដូចដែលបានបញ្ជាក់ហើយការបញ្ជាក់ពិពណ៌នាយ៉ាងពេញលេញអំពីឥរិយាបទនៃប្រព័ន្ធ ប៉ុន្តែតាមពិតឧបករណ៍នេះមិនមានកំហុសទេ ដែលត្រូវបានបង្ហាញយ៉ាងច្បាស់ដោយបញ្ហាដែលកើតឡើងជាទៀងទាត់នៅក្នុងយន្តការនៃការអនុវត្តការប៉ាន់ស្មាន។ ការណែនាំ។ វេទិកាផ្នែករឹងបើកចំហធ្វើឱ្យវាកាន់តែងាយស្រួលក្នុងការរួមបញ្ចូលការផ្លាស់ប្តូរដែលទាក់ទងនឹងសុវត្ថិភាព - ឧទាហរណ៍ ដើម្បីទប់ស្កាត់ការលេចធ្លាយឆានែលដែលអាចកើតមានទាំងអស់ ដែលជាកន្លែងដែលវាមានប្រសិទ្ធភាពជាងក្នុងការកម្ចាត់បញ្ហានៅក្នុងផ្នែករឹងជាជាងការព្យាយាមស្វែងរកដំណោះស្រាយនៅក្នុងកម្មវិធី។

សូមចាំថាស្ថាបត្យកម្ម seL4 គួរឱ្យកត់សម្គាល់ ផ្លាស់ទីផ្នែកសម្រាប់គ្រប់គ្រងធនធានខឺណែលទៅក្នុងលំហអ្នកប្រើប្រាស់ និងអនុវត្តមធ្យោបាយគ្រប់គ្រងការចូលប្រើដូចគ្នាសម្រាប់ធនធានដូចជាធនធានអ្នកប្រើប្រាស់។ មីក្រូខឺណែលមិនផ្តល់អរូបីកម្រិតខ្ពស់ដែលត្រៀមរួចជាស្រេចសម្រាប់ការគ្រប់គ្រងឯកសារ ដំណើរការ ការតភ្ជាប់បណ្តាញ និងអ្វីផ្សេងទៀតទេ ផ្ទុយទៅវិញ វាផ្តល់តែយន្តការតិចតួចប៉ុណ្ណោះសម្រាប់ការគ្រប់គ្រងការចូលទៅកាន់លំហអាសយដ្ឋានជាក់ស្តែង ការរំខាន និងធនធានដំណើរការ។ abstractions និងកម្មវិធីបញ្ជាកម្រិតខ្ពស់សម្រាប់អន្តរកម្មជាមួយ hardware ត្រូវបានអនុវត្តដោយឡែកពីគ្នានៅលើកំពូលនៃ microkernel ក្នុងទម្រង់នៃភារកិច្ចកម្រិតអ្នកប្រើប្រាស់។ ការចូលប្រើប្រាស់ភារកិច្ចបែបនេះចំពោះធនធានដែលមានសម្រាប់មីក្រូខឺណែលត្រូវបានរៀបចំតាមរយៈនិយមន័យនៃច្បាប់។

RISC-V ផ្តល់នូវប្រព័ន្ធណែនាំម៉ាស៊ីនបើកចំហ និងអាចបត់បែនបានដែលអនុញ្ញាតឱ្យ microprocessors ត្រូវបានបង្កើតឡើងសម្រាប់កម្មវិធីដែលបំពានដោយមិនចាំបាច់ទាមទារថ្លៃសួយសារអាករ ឬខ្សែភ្ជាប់សម្រាប់ប្រើប្រាស់។ RISC-V អនុញ្ញាតឱ្យអ្នកបង្កើត SoCs និង processors ដែលបើកចំហទាំងស្រុង។ បច្ចុប្បន្នផ្អែកលើការបញ្ជាក់ RISC-V ដោយក្រុមហ៊ុន និងសហគមន៍ផ្សេងៗគ្នាក្រោមអាជ្ញាប័ណ្ណឥតគិតថ្លៃផ្សេងៗ (BSD, MIT, Apache 2.0) កំពុងអភិវឌ្ឍ វ៉ារ្យ៉ង់រាប់សិបនៃ microprocessor cores, SoCs និងបន្ទះឈីបដែលបានផលិតរួចហើយ។ ការគាំទ្រ RISC-V មានវត្តមានចាប់តាំងពីការចេញផ្សាយរបស់ Glibc 2.27, binutils 2.30, gcc 7 និងខឺណែលលីនុច 4.15។

ប្រភព: opennet.ru