RISC-V ፋውንዴሽን የማይክሮከርነሉን አሠራር ስለማረጋገጥ በ RISC-V መመሪያ ስብስብ አርክቴክቸር በስርዓቶች ላይ። ማረጋገጫው ወደ ላይ ይመጣል የ seL4 አሠራር አስተማማኝነት, ይህም በመደበኛ ቋንቋ ውስጥ ከተገለጹት መመዘኛዎች ጋር ሙሉ በሙሉ መሟላቱን ያሳያል. አስተማማኝነት ማረጋገጫ seL4 በ RISC-V RV64 ፕሮሰሰር ላይ የተመሰረተ በተልዕኮ-ወሳኝ ሲስተሞች ውስጥ አስተማማኝነት መጨመር የሚያስፈልጋቸው እና ውድቀቶች አለመኖራቸውን ያረጋግጣል። በሴኤል 4 ከርነል አናት ላይ የሚሰሩ የሶፍትዌር አዘጋጆች በአንድ የስርአቱ ክፍል ላይ ብልሽት ካለ ይህ ውድቀት ወደሌላው የስርአቱ ክፍል እና በተለይም ወሳኝ ክፍሎቹ እንደማይሰራጭ ሙሉ በሙሉ እርግጠኞች ሊሆኑ ይችላሉ።
የ seL4 ማይክሮከርነል መጀመሪያ የተረጋገጠው ለ 32-ቢት ARM ፕሮሰሰሮች፣ እና በኋላ ለ64-ቢት x86 ፕሮሰሰር ነው። የተከፈተው RISC-V ሃርድዌር አርክቴክቸር ከተከፈተው seL4 ማይክሮከርነል ጋር ሲጣመር አዲስ የደህንነት ደረጃ እንደሚያስገኝ ተጠቁሟል ምክንያቱም የሃርድዌር ክፍሎቹም ወደፊት ሙሉ በሙሉ ሊረጋገጡ ስለሚችሉ ለባለቤትነት ሃርድዌር አርክቴክቸር ሊደረስ የማይችል ነው።
ኤስኤል 4ን በሚያረጋግጥበት ጊዜ መሳሪያው እንደተገለፀው እንደሚሰራ ይታሰባል እና መግለጫው የስርዓቱን ባህሪ ሙሉ በሙሉ ይገልፃል ፣ ግን በእውነቱ መሣሪያዎቹ ከስህተቶች ነፃ አይደሉም ፣ ይህም በግምታዊ አፈፃፀም ዘዴ ውስጥ በየጊዜው በሚፈጠሩ ችግሮች በግልፅ ይታያል ። መመሪያዎች. ክፍት የሃርድዌር መድረኮች ከደህንነት ጋር የተገናኙ ለውጦችን ለማዋሃድ ቀላል ያደርጉታል - ለምሳሌ ፣ ሁሉንም ሊሆኑ የሚችሉ የጎን ቻናል ፍንጮችን ለመግታት ፣ በሶፍትዌር ውስጥ መፍትሄዎችን ለማግኘት ከመሞከር ይልቅ በሃርድዌር ውስጥ ያለውን ችግር ለማስወገድ በጣም ቀልጣፋ ነው።
የ seL4 አርክቴክቸር መሆኑን አስታውስ የከርነል ሀብቶችን ለማስተዳደር ክፍሎችን ወደ ተጠቃሚ ቦታ መውሰድ እና እንደ የተጠቃሚ ሀብቶች ተመሳሳይ የመዳረሻ መቆጣጠሪያ ዘዴዎችን መተግበር። ማይክሮከርነል ፋይሎችን ፣ ሂደቶችን ፣ የአውታረ መረብ ግንኙነቶችን እና መሰል ነገሮችን ለማስተዳደር ዝግጁ-የተሰሩ የከፍተኛ ደረጃ ማጠቃለያዎችን አይሰጥም ፣ ይልቁንም የአካላዊ አድራሻ ቦታን ፣ መቆራረጥን እና የአቀነባባሪ ሃብቶችን ለመቆጣጠር አነስተኛ ዘዴዎችን ብቻ ይሰጣል። ከሃርድዌር ጋር መስተጋብር ለመፍጠር የከፍተኛ ደረጃ ማጠቃለያዎች እና አሽከርካሪዎች በማይክሮከርነል አናት ላይ በተጠቃሚ ደረጃ ተግባራት ውስጥ ተለይተው ተፈጻሚ ይሆናሉ። እንደነዚህ ያሉ ሥራዎችን ለማይክሮከርነል የሚገኙትን ሀብቶች መድረስ በሕጎች ፍቺ በኩል ተደራጅቷል ።
RISC-V የማይክሮፕሮሰሰሮችን የዘፈቀደ አፕሊኬሽኖች እንዲገነቡ የሚያስችል ክፍት እና ተለዋዋጭ የማሽን መመሪያ ስርዓት ያቀርባል ከሮያሊቲዎች ወይም ከጥቅም ጋር የተያያዙ ገመዶችን ሳያስፈልግ። RISC-V ሙሉ ለሙሉ ክፍት የሆኑ ሶሲዎችን እና ፕሮሰሰሮችን እንዲፈጥሩ ይፈቅድልዎታል። በአሁኑ ጊዜ በተለያዩ ኩባንያዎች እና ማህበረሰቦች በተለያዩ ነጻ ፈቃዶች (BSD፣ MIT፣ Apache 2.0) በRISC-V ዝርዝር መግለጫ ላይ የተመሰረተ በርካታ ደርዘን ዓይነቶች የማይክሮፕሮሰሰር ኮሮች፣ SoCs እና ቀድሞ የተሰሩ ቺፖችን። የRISC-V ድጋፍ Glibc 2.27፣ binutils 2.30፣ gcc 7 እና Linux kernel 4.15 ከተለቀቀ በኋላ አለ።
ምንጭ: opennet.ru