RISC-V在其RV4處理器上驗證了seL64微內核

RISC-V基金會宣布已驗證 微內核如何工作 seL4在具有 指令集架構 RISC-V。 其中，驗證過程簡化為seL4可靠性的數學證明，表明完全符合正式語言中指定的規格。

可靠性測試使seL4可在基於RISC-V處理器的關鍵任務系統中使用 RV64，這需要更高的可靠性，並且不能保證會出現故障。

運行在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的支持一直存在。

關於seL4微內核測試

最初，微內核 seL4已針對32位ARM處理器進行了驗證，而 x86 64位處理器的更高版本.

可以看出，RISC-V開放硬件體系結構與開放微內核的結合 seL4將達到新的安全水平，因為將來的硬件組件也可以得到完全驗證，而專有硬件體系結構則無法實現。

檢查seL4時，必須假定硬件運行正常（即，如指定的那樣）。 假設首先要有一個明確的規範，但並非所有硬件都如此。 

但是，即使存在這樣的規範並且是規範的（即以支持有關其屬性的數學推理的數學形式主義形式編寫的），我們如何知道它實際上捕獲了硬件的行為？ 

現實情況是，我們可以確定情況並非如此。 硬件與軟件沒有什麼不同，因為兩者都是錯誤的。

但是擁有一個開放的ISA不僅具有免版稅的優勢。 其一是它允許開源硬件實現。

檢查seL4時，假定設備按指示工作，並且規格充分描述了系統的行為，但實際上設備並非沒有錯誤，這在推測執行機制中經常出現的問題中得到了很好的說明。 。

開放的硬件平台簡化了變更的集成 例如，與安全相關的功能是通過第三方渠道阻止所有可能的洩漏渠道，在這種情況下，通過硬件解決問題比通過軟件尋求解決方案要有效得多。

最後，如果您想了解更多信息，可以查閱 以下鏈接。