RISC-V ಆರ್ಕಿಟೆಕ್ಚರ್‌ಗಾಗಿ seL4 ಮೈಕ್ರೊಕರ್ನಲ್ ಅನ್ನು ಗಣಿತೀಯವಾಗಿ ಪರಿಶೀಲಿಸಲಾಗಿದೆ

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 ಗಳು ಮತ್ತು ಪ್ರೊಸೆಸರ್‌ಗಳನ್ನು ರಚಿಸಲು ನಿಮಗೆ ಅನುಮತಿಸುತ್ತದೆ. ಪ್ರಸ್ತುತ RISC-V ವಿವರಣೆಯನ್ನು ಆಧರಿಸಿ ವಿವಿಧ ಕಂಪನಿಗಳು ಮತ್ತು ಸಮುದಾಯಗಳು ವಿವಿಧ ಉಚಿತ ಪರವಾನಗಿಗಳ ಅಡಿಯಲ್ಲಿ (BSD, MIT, Apache 2.0) ಅಭಿವೃದ್ಧಿ ಹೊಂದುತ್ತಿದೆ ಮೈಕ್ರೊಪ್ರೊಸೆಸರ್ ಕೋರ್‌ಗಳ ಹಲವಾರು ಡಜನ್ ರೂಪಾಂತರಗಳು, SoC ಗಳು ಮತ್ತು ಈಗಾಗಲೇ ತಯಾರಿಸಿದ ಚಿಪ್‌ಗಳು. Glibc 2.27, binutils 2.30, gcc 7, ಮತ್ತು Linux ಕರ್ನಲ್ 4.15 ಬಿಡುಗಡೆಯಾದಾಗಿನಿಂದ RISC-V ಬೆಂಬಲವು ಪ್ರಸ್ತುತವಾಗಿದೆ.

ಮೂಲ: opennet.ru