(相關資料圖)

近日，谷歌宣布，推出為嵌入式設備準備的操作系統 KataOS。

據悉，KataOS 選擇了 seL4 作為微內核，其經過數學證明是安全的，具有保證的機密性、完整性和可用性。通過 seL4 CAmkES 框架，KataOS 還能夠提供靜態定義和可分析的系統組件。KataOS 提供了一個可驗證的安全平臺，保護用戶的隱私，因為應用程序在邏輯上不可能違反內核的硬件安全保護，并且系統組件是可驗證安全的。