seL4 మైక్రోకెర్నల్ RISC-V ఆర్కిటెక్చర్ కోసం గణితశాస్త్రపరంగా ధృవీకరించబడింది

RISC-V ఫౌండేషన్ నివేదించబడింది మైక్రోకెర్నల్ యొక్క ఆపరేషన్‌ని ధృవీకరించడం గురించి seL4 RISC-V ఇన్‌స్ట్రక్షన్ సెట్ ఆర్కిటెక్చర్‌తో కూడిన సిస్టమ్‌లపై. ధృవీకరణ క్రిందికి వస్తుంది గణిత శాస్త్ర రుజువు seL4 ఆపరేషన్ యొక్క విశ్వసనీయత, ఇది అధికారిక భాషలో పేర్కొన్న స్పెసిఫికేషన్లతో పూర్తి సమ్మతిని సూచిస్తుంది. విశ్వసనీయతకు రుజువు మీరు ఉపయోగించడానికి అనుమతిస్తుంది RISC-V RV4 ప్రాసెసర్‌లపై ఆధారపడిన మిషన్-క్రిటికల్ సిస్టమ్‌లలో seL64 విశ్వసనీయత యొక్క అధిక స్థాయి అవసరం మరియు వైఫల్యాల లేమికి హామీ ఇస్తుంది. seL4 కెర్నల్ పైన నడుస్తున్న సాఫ్ట్‌వేర్ డెవలపర్‌లు సిస్టమ్‌లోని ఒక భాగంలో వైఫల్యం ఉన్నట్లయితే, ఈ వైఫల్యం మిగిలిన సిస్టమ్‌కు మరియు ముఖ్యంగా దాని కీలక భాగాలకు వ్యాపించదని పూర్తిగా నమ్మకంగా ఉంటారు.

seL4 మైక్రోకెర్నల్ మొదట్లో 32-బిట్ ARM ప్రాసెసర్‌ల కోసం మరియు తరువాత 64-బిట్ x86 ప్రాసెసర్‌ల కోసం ధృవీకరించబడింది. ఓపెన్ seL4 మైక్రోకెర్నల్‌తో ఓపెన్ RISC-V హార్డ్‌వేర్ ఆర్కిటెక్చర్ కలయిక కొత్త స్థాయి భద్రతను సాధిస్తుందని గుర్తించబడింది, ఎందుకంటే భవిష్యత్తులో హార్డ్‌వేర్ భాగాలను కూడా పూర్తిగా ధృవీకరించవచ్చు, ఇది యాజమాన్య హార్డ్‌వేర్ ఆర్కిటెక్చర్‌ల కోసం సాధించడం అసాధ్యం.

seL4ని ధృవీకరించేటప్పుడు, పరికరాలు పేర్కొన్న విధంగా పనిచేస్తాయని మరియు స్పెసిఫికేషన్ సిస్టమ్ యొక్క ప్రవర్తనను పూర్తిగా వివరిస్తుందని భావించబడుతుంది, అయితే వాస్తవానికి పరికరాలు లోపాల నుండి విముక్తి పొందలేదు, ఇది ఊహాజనిత అమలులో క్రమం తప్పకుండా తలెత్తే సమస్యల ద్వారా స్పష్టంగా ప్రదర్శించబడుతుంది. సూచనలు. ఓపెన్ హార్డ్‌వేర్ ప్లాట్‌ఫారమ్‌లు భద్రత-సంబంధిత మార్పులను ఏకీకృతం చేయడాన్ని సులభతరం చేస్తాయి - ఉదాహరణకు, సాధ్యమయ్యే అన్ని సైడ్-ఛానల్ లీక్‌లను నిరోధించడం, సాఫ్ట్‌వేర్‌లో పరిష్కారాలను కనుగొనడానికి ప్రయత్నించడం కంటే హార్డ్‌వేర్‌లోని సమస్యను వదిలించుకోవడం చాలా సమర్థవంతంగా ఉంటుంది.

seL4 ఆర్కిటెక్చర్ గుర్తుకు తెచ్చుకోండి విశేషమైనది వినియోగదారు స్థలంలోకి కెర్నల్ వనరులను నిర్వహించడం కోసం భాగాలను తరలించడం మరియు వినియోగదారు వనరుల వంటి వనరుల కోసం అదే యాక్సెస్ నియంత్రణను వర్తింపజేయడం. మైక్రోకెర్నల్ ఫైల్‌లు, ప్రాసెస్‌లు, నెట్‌వర్క్ కనెక్షన్‌లు మరియు ఇలాంటి వాటిని నిర్వహించడానికి సిద్ధంగా ఉన్న అధిక-స్థాయి సంగ్రహాలను అందించదు; బదులుగా, ఇది భౌతిక చిరునామా స్థలం, అంతరాయాలు మరియు ప్రాసెసర్ వనరులకు ప్రాప్యతను నియంత్రించడానికి కనీస మెకానిజమ్‌లను మాత్రమే అందిస్తుంది. హార్డ్‌వేర్‌తో పరస్పర చర్య చేయడానికి ఉన్నత-స్థాయి సంగ్రహణలు మరియు డ్రైవర్‌లు వినియోగదారు-స్థాయి పనుల రూపంలో మైక్రోకెర్నల్ పైన విడిగా అమలు చేయబడతాయి. మైక్రోకెర్నల్‌కు అందుబాటులో ఉన్న వనరులకు అటువంటి పనుల యాక్సెస్ నియమాల నిర్వచనం ద్వారా నిర్వహించబడుతుంది.

RISC-V ఒక ఓపెన్ మరియు ఫ్లెక్సిబుల్ మెషిన్ ఇన్‌స్ట్రక్షన్ సిస్టమ్‌ను అందిస్తుంది, ఇది మైక్రోప్రాసెసర్‌లను ఏకపక్ష అనువర్తనాల కోసం నిర్మించడానికి రాయల్టీలు లేదా స్ట్రింగ్‌లు అవసరం లేకుండా అనుమతిస్తుంది. RISC-V పూర్తిగా ఓపెన్ SoCలు మరియు ప్రాసెసర్‌లను సృష్టించడానికి మిమ్మల్ని అనుమతిస్తుంది. ప్రస్తుతం వివిధ ఉచిత లైసెన్స్‌ల (BSD, MIT, Apache 2.0) కింద వివిధ కంపెనీలు మరియు సంఘాల ద్వారా RISC-V స్పెసిఫికేషన్ ఆధారంగా అభివృద్ధి చెందుతుంది మైక్రోప్రాసెసర్ కోర్లు, SoCలు మరియు ఇప్పటికే ఉత్పత్తి చేయబడిన చిప్‌ల యొక్క అనేక డజన్ల రకాలు. Glibc 2.27, binutils 2.30, gcc 7 మరియు Linux కెర్నల్ 4.15 విడుదలల నుండి RISC-V మద్దతు ఉంది.

మూలం: opennet.ru

ఒక వ్యాఖ్యను జోడించండి