RISC-V基金會 關於驗證微核心的運行 在具有 RISC-V 指令集架構的系統上。 驗證歸結為 seL4 操作的可靠性，表示完全符合正式語言中指定的規範。 可靠性證明 基於 RISC-V RV4 處理器的關鍵任務系統中的 seL64，需要提高可靠性並確保不故障。 在 seL4 核心之上運行的軟體開發人員可以完全確信，如果系統的某個部分出現故障，這種故障不會蔓延到系統的其餘部分，特別是其關鍵部分。
seL4 微核心最初針對 32 位元 ARM 處理器進行驗證，後來針對 64 位元 x86 處理器進行驗證。 值得注意的是，開放RISC-V硬體架構與開放seL4微核心的結合將實現新的安全水平，因為未來硬體元件也可以充分驗證，這是專有硬體架構無法實現的。
在驗證 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