RISC-V ફાઉન્ડેશન માઇક્રોકર્નલની કામગીરીની ચકાસણી વિશે RISC-V સૂચના સેટ આર્કિટેક્ચર સાથે સિસ્ટમો પર. ચકાસણી નીચે આવે છે seL4 ઓપરેશનની વિશ્વસનીયતા, જે ઔપચારિક ભાષામાં ઉલ્લેખિત સ્પષ્ટીકરણો સાથે સંપૂર્ણ પાલન સૂચવે છે. વિશ્વસનીયતાનો પુરાવો RISC-V RV4 પ્રોસેસર્સ પર આધારિત મિશન-ક્રિટીકલ સિસ્ટમ્સમાં seL64 કે જેને વિશ્વસનીયતાના વધેલા સ્તરની જરૂર છે અને નિષ્ફળતાઓની ગેરહાજરીની ખાતરી આપે છે. seL4 કર્નલની ટોચ પર ચાલતા સોફ્ટવેરના વિકાસકર્તાઓ સંપૂર્ણ વિશ્વાસ રાખી શકે છે કે જો સિસ્ટમના એક ભાગમાં નિષ્ફળતા હોય, તો આ નિષ્ફળતા બાકીની સિસ્ટમમાં અને ખાસ કરીને, તેના નિર્ણાયક ભાગોમાં ફેલાશે નહીં.
seL4 માઇક્રોકર્નલ શરૂઆતમાં 32-બીટ એઆરએમ પ્રોસેસર માટે અને પછીથી 64-બીટ x86 પ્રોસેસર માટે ચકાસવામાં આવ્યું હતું. એ નોંધ્યું છે કે ઓપન seL4 માઇક્રોકર્નલ સાથે ઓપન RISC-V હાર્ડવેર આર્કિટેક્ચરનું સંયોજન સુરક્ષાના નવા સ્તરને હાંસલ કરશે, કારણ કે ભવિષ્યમાં હાર્ડવેર ઘટકોને પણ સંપૂર્ણ રીતે ચકાસી શકાય છે, જે માલિકીના હાર્ડવેર આર્કિટેક્ચર્સ માટે પ્રાપ્ત કરવું અશક્ય છે.
seL4 ની ચકાસણી કરતી વખતે, એવું માનવામાં આવે છે કે સાધન જણાવ્યા મુજબ કાર્ય કરે છે અને સ્પષ્ટીકરણ સિસ્ટમની વર્તણૂકનું સંપૂર્ણ વર્ણન કરે છે, પરંતુ વાસ્તવમાં સાધન ભૂલોથી મુક્ત નથી, જે સટ્ટાકીય અમલીકરણની પદ્ધતિમાં નિયમિતપણે ઉભરતી સમસ્યાઓ દ્વારા સ્પષ્ટપણે દર્શાવવામાં આવે છે. સૂચનાઓ ઓપન હાર્ડવેર પ્લેટફોર્મ સુરક્ષા-સંબંધિત ફેરફારોને એકીકૃત કરવાનું સરળ બનાવે છે - ઉદાહરણ તરીકે, તમામ સંભવિત સાઇડ-ચેનલ લીક્સને અવરોધિત કરવા, જ્યાં સોફ્ટવેરમાં ઉકેલ શોધવાનો પ્રયાસ કરવા કરતાં હાર્ડવેરમાં સમસ્યાથી છુટકારો મેળવવો વધુ કાર્યક્ષમ છે.
યાદ કરો કે seL4 આર્કિટેક્ચર કર્નલ સંસાધનોને વપરાશકર્તા જગ્યામાં મેનેજ કરવા માટે ભાગોને ખસેડવા અને વપરાશકર્તા સંસાધનોની જેમ સ્રોતો માટે સમાન વપરાશ નિયંત્રણનો અર્થ લાગુ કરવો. માઇક્રોકર્નલ ફાઇલો, પ્રક્રિયાઓ, નેટવર્ક કનેક્શન્સ અને તેના જેવા મેનેજ કરવા માટે તૈયાર ઉચ્ચ-સ્તરનાં એબ્સ્ટ્રેક્શન્સ પ્રદાન કરતું નથી; તેના બદલે, તે ભૌતિક સરનામાં સ્થાન, વિક્ષેપો અને પ્રોસેસર સંસાધનોની ઍક્સેસને નિયંત્રિત કરવા માટે માત્ર ન્યૂનતમ પદ્ધતિઓ પ્રદાન કરે છે. હાર્ડવેર સાથે ક્રિયાપ્રતિક્રિયા કરવા માટે ઉચ્ચ-સ્તરના એબ્સ્ટ્રેક્શન્સ અને ડ્રાઇવરો વપરાશકર્તા-સ્તરના કાર્યોના સ્વરૂપમાં માઇક્રોકર્નલની ટોચ પર અલગથી લાગુ કરવામાં આવે છે. માઇક્રોકર્નલને ઉપલબ્ધ સંસાધનોમાં આવા કાર્યોની ઍક્સેસ નિયમોની વ્યાખ્યા દ્વારા ગોઠવવામાં આવે છે.
RISC-V એક ખુલ્લી અને લવચીક મશીન સૂચના પ્રણાલી પ્રદાન કરે છે જે માઇક્રોપ્રોસેસરોને ઉપયોગ માટે જોડાયેલ રોયલ્ટી અથવા સ્ટ્રિંગ્સની જરૂર વગર મનસ્વી એપ્લિકેશનો માટે બનાવવાની મંજૂરી આપે છે. RISC-V તમને સંપૂર્ણપણે ઓપન SoCs અને પ્રોસેસર્સ બનાવવાની પરવાનગી આપે છે. હાલમાં વિવિધ કંપનીઓ અને સમુદાયો દ્વારા વિવિધ મફત લાઇસન્સ (BSD, MIT, Apache 2.0) હેઠળ RISC-V સ્પષ્ટીકરણ પર આધારિત છે. માઇક્રોપ્રોસેસર કોરો, SoCs અને પહેલેથી જ ઉત્પાદિત ચિપ્સના કેટલાક ડઝન પ્રકારો. RISC-V આધાર Glibc 2.27, binutils 2.30, gcc 7, અને Linux કર્નલ 4.15 ના પ્રકાશન પછી હાજર છે.
સોર્સ: opennet.ru