RISC-V એ તેમના આરવી 4 પ્રોસેસરો પર SEL64 માઇક્રોકર્નલની ચકાસણી કરી

આરઆઈએસસી-વી ફાઉન્ડેશને જાહેરાત કરી કે તેની ચકાસણી થઈ છે માઇક્રોકર્નલ કેવી રીતે કાર્ય કરે છે સાથે સિસ્ટમોમાં seL4 સૂચના સેટ આર્કિટેક્ચર આરઆઈએસસી-વી. જેમાં ચકાસણી પ્રક્રિયાને SEL4 ની વિશ્વસનીયતાના ગાણિતિક પુરાવા માટે ઘટાડવામાં આવે છે, જે formalપચારિક ભાષામાં ઉલ્લેખિત સ્પષ્ટીકરણોનું સંપૂર્ણ પાલન સૂચવે છે.

વિશ્વસનીયતા પરીક્ષણ, આરઆઈએસસી-વી પ્રોસેસરો પર આધારીત મિશન ક્રિટિકલ સિસ્ટમોમાં સેલ 4 નો ઉપયોગ કરવા માટે સક્ષમ બનાવે છે RV64, જેને ઉચ્ચ સ્તરની વિશ્વસનીયતાની જરૂર હોય છે અને તે નિષ્ફળતાની બાંયધરી આપતું નથી.

સીએલ 4 કર્નલની ટોચ પર ચાલતા સ Softwareફ્ટવેર ડેવલપર્સ સંપૂર્ણપણે ખાતરી કરી શકે છે કે સિસ્ટમના એક ભાગમાં નિષ્ફળતાની સ્થિતિમાં, આ નિષ્ફળતા સિસ્ટમના બાકીના ભાગોમાં અને ખાસ કરીને, તેના નિર્ણાયક ભાગોમાં ફેલાશે નહીં.

વિશે SEL4

આ સીએલ 4 આર્કિટેક્ચર વપરાશકર્તા જગ્યામાં કર્નલ સંસાધનોના સંચાલન માટે ભાગોને દૂર કરવા માટે નોંધપાત્ર છે અને આવા સંસાધનો માટે વપરાશકર્તા સ્રોતો માટે સમાન accessક્સેસ નિયંત્રણ પદ્ધતિઓનો ઉપયોગ કરો.

માઇક્રોકર્નલ ઉચ્ચ-સ્તરના એબ્સ્ટ્રેક્શન્સ પ્રદાન કરતું નથી ફાઇલો, પ્રક્રિયાઓ, નેટવર્ક જોડાણો, વગેરેનું સંચાલન કરવા માટે પહેલાથી જ તૈયાર છે, પરંતુ તેના બદલે ભૌતિક સરનામાં સ્થાનની toક્સેસને નિયંત્રિત કરવા માટે ફક્ત ન્યૂનતમ પદ્ધતિઓ પ્રદાન કરે છે, વિક્ષેપો અને પ્રોસેસર સંસાધનો.

કમ્પ્યુટર સાથે ક્રિયાપ્રતિક્રિયા માટે ઉચ્ચ-સ્તરના એબ્સ્ટ્રેક્શન્સ અને ડ્રાઇવરો, વપરાશકર્તા સ્તર પર કરવામાં આવેલા કાર્યોના રૂપમાં માઇક્રોકર્નલની ટોચ પર અલગથી લાગુ કરવામાં આવે છે.

માઇક્રોકર્નલમાં ઉપલબ્ધ સંસાધનોમાં આવા કાર્યોની પહોંચ નિયમોની વ્યાખ્યા દ્વારા ગોઠવવામાં આવે છે.

આરઆઈએસસી-વી એક ખુલ્લી અને લવચીક સિસ્ટમ પ્રદાન કરે છે મશીન સૂચનો કે કપાતની જરૂરિયાત વિના, મનસ્વી કાર્યક્રમો માટે માઇક્રોપ્રોસેસર બનાવવાની મંજૂરી આપે છે અને ઉપયોગની શરતો લાદ્યા વિના.

આરઆઈએસસી-વી તમને સંપૂર્ણપણે ખુલ્લા પ્રોસેસર્સ અને એસઓસી બનાવવા માટે પરવાનગી આપે છે. હાલમાં, આરઆઈએસસી-વી સ્પષ્ટીકરણના આધારે, વિવિધ કંપનીઓ અને વિવિધ મફત લાઇસન્સ (બીએસડી, એમઆઈટી, અપાચે 2.0) હેઠળના સમુદાયો પહેલાથી ઉત્પાદિત માઇક્રોપ્રોસેસર કોરો, એસઓસી અને ચિપ્સના કેટલાક ડઝન વિવિધ પ્રકારો વિકસાવી રહ્યા છે.

ગિલીબીસી 2.27, બેન્યુટીલ્સ 2.30, જીસીસી 7, અને લિનક્સ 4.15 કર્નલના પ્રકાશન પછી આરઆઈએસસી-વી આધાર છે.

સીએલ 4 માઇક્રોકર્નલ પરીક્ષણ વિશે

શરૂઆતમાં, માઇક્રોકરનલ seL4 32-બીટ એઆરએમ પ્રોસેસરો માટે ચકાસાયેલ હતુંઅને પાછળથી x86 64-બીટ પ્રોસેસરો માટે.

તે જોવાયું છે કે આરઆઈએસસી-વી ખુલ્લા હાર્ડવેર આર્કિટેક્ચરનું સંયોજન ખુલ્લા માઇક્રોકેનલ સાથે છે SEL4 સલામતીનું એક નવું સ્તર પ્રાપ્ત કરશે, કારણ કે ભવિષ્યમાં હાર્ડવેર ઘટકો પણ સંપૂર્ણ રૂપે ચકાસી શકાય છે, જે માલિકીના હાર્ડવેર આર્કિટેક્ચરો માટે પ્રાપ્ત કરવાનું અશક્ય છે.

જ્યારે આપણે seL4 તપાસીએ છીએ, ત્યારે આપણે માની લેવું જોઈએ કે હાર્ડવેર યોગ્ય રીતે કાર્ય કરી રહ્યું છે (એટલે ​​કે, ઉલ્લેખિત છે). તે ધારે છે કે પ્રથમ સ્થાને એક અસ્પષ્ટ સ્પષ્ટીકરણ છે, જે બધા હાર્ડવેર માટે કેસ નથી. 

પરંતુ જ્યારે પણ આવી વિશિષ્ટતા અસ્તિત્વમાં છે, અને તે formalપચારિક છે (એટલે ​​કે તેના ગુણધર્મો વિશેના ગાણિતિક તર્કને ટેકો આપે છે તે ગાણિતિક formalપચારિકતામાં ધકેલી દેવામાં આવે છે), તો આપણે કેવી રીતે જાણી શકીએ કે તે ખરેખર હાર્ડવેરના વર્તનને પકડે છે? 

વાસ્તવિકતા એ છે કે આપણે ખાતરીપૂર્વક કહી શકીએ કે તે નથી. હાર્ડવેર એ સ softwareફ્ટવેરથી અલગ નથી જેમાં બંને બગડેલ છે.

પરંતુ ખુલ્લા આઇએસએ હોવાના ફાયદાઓ છે જે રોયલ્ટી મુક્ત હોવા કરતાં આગળ વધે છે. એક તે તે ઓપન સોર્સ હાર્ડવેર અમલીકરણોને મંજૂરી આપે છે.

સીએલ 4 તપાસ કરતી વખતે, એવું માનવામાં આવે છે કે ઉપકરણ સૂચવેલા પ્રમાણે કાર્ય કરે છે અને સ્પષ્ટીકરણ સિસ્ટમની વર્તણૂકનું સંપૂર્ણ વર્ણન કરે છે, પરંતુ હકીકતમાં સાધન ભૂલથી મુક્ત નથી, જે સટ્ટાકીય અમલ પદ્ધતિમાં નિયમિતપણે ઉદ્ભવતા સમસ્યાઓ દ્વારા સારી રીતે દર્શાવવામાં આવે છે.

ખુલ્લા હાર્ડવેર પ્લેટફોર્મ ફેરફારોનું એકીકરણ સરળ બનાવે છે સુરક્ષાથી સંબંધિત, ઉદાહરણ તરીકે, તૃતીય-પક્ષ ચેનલો દ્વારા બધી શક્ય લિક ચેનલોને અવરોધિત કરવા માટે, જ્યાં સ hardwareફ્ટવેર દ્વારા ઉકેલો શોધવાનો પ્રયાસ કરતાં હાર્ડવેર દ્વારા સમસ્યામાંથી છુટકારો મેળવવામાં તે વધુ કાર્યક્ષમ છે.

અંતે, જો તમે તેના વિશે વધુ જાણવા માંગતા હો, તો તમે નોટની સલાહ લઈ શકો છો નીચેની કડી


તમારી ટિપ્પણી મૂકો

તમારું ઇમેઇલ સરનામું પ્રકાશિત કરવામાં આવશે નહીં. આવશ્યક ક્ષેત્રો સાથે ચિહ્નિત થયેલ છે *

*

*

  1. ડેટા માટે જવાબદાર: મિગ્યુએલ gelંજેલ ગેટóન
  2. ડેટાનો હેતુ: નિયંત્રણ સ્પામ, ટિપ્પણી સંચાલન.
  3. કાયદો: તમારી સંમતિ
  4. ડેટાની વાતચીત: કાયદાકીય જવાબદારી સિવાય ડેટા તૃતીય પક્ષને આપવામાં આવશે નહીં.
  5. ડેટા સ્ટોરેજ: cસેન્ટસ નેટવર્ક્સ (ઇયુ) દ્વારા હોસ્ટ કરેલો ડેટાબેઝ
  6. અધિકાર: કોઈપણ સમયે તમે તમારી માહિતીને મર્યાદિત, પુન recoverપ્રાપ્ત અને કા deleteી શકો છો.

  1.   કેટલાક એક જણાવ્યું હતું કે

    મારા માટે, આ પ્રોસેસર કંઈક છે જે મને ઘણું કહે છે. તે ફક્ત કેટલાક ચરબીયુક્ત કમ્પ્યુટર કૂતરા માટે કમ્પ્યુટર બનાવવાનું બાકી છે જેને આપણે ખરીદી શકીએ.

    એઆરએમ ઇશ્યૂ કંઈક એવી છે જે મને છીનવી લે છે, તમે પહેલેથી જ જોયું હતું કે પ્રતિબંધો સાથે હ્યુઆવેઇ સાથે શું થયું છે. હું સ્પષ્ટ છું કે મારા આરઆઈએસસી-વી માટે તે તમામ સ્તરે એક વધુ સારો ઉકેલો છે. આ ક્ષણે હ્યુઆવેઇએ તેના પર પહેલેથી જ ધ્યાન રાખ્યું છે અને કદાચ ભવિષ્યમાં તેમની પાસે આ માઇક્રો સાથે સાધનો હશે. જો એમ હોય તો, ચોક્કસ ત્યાં વધુ કંપનીઓ હશે જે તેને અપનાવે છે અને મારા માટે તે આદર્શ હશે અને સૌથી ઉપર કે જે ડિસ્ટ્રોસ તેને સમર્થન આપે છે અને એટલું જ નહીં, જેમ કે મોટાભાગના લોકો સાથે થાય છે.

    1.    ગ્રેગરી રોઝ જણાવ્યું હતું કે

      + 10