seL4 微核心

四 15 十二月 2022 by ols3

Moda 其實有很多事可以做,而不是自詡為 Ministry of Dispatch Affairs。

以建立數位韌性而言,例如:先進安全的作業系統研究、安全程式語言的應用推廣、安全程式審計認證制度等等,這些都是紮馬步打基石的重要工程。

當然,這非短期即可見成效的,但至少應列出具體的短中長期目標讓人民了解,而不是憑一堆形容詞就來消化200多億預算。

建立數位韌性,應以 OpenBSD 為師,安全高標務實不躁進。

======

舊文引貼

這位退休榮譽教授建議數位發展部應該如何如何,其中開頭提到台灣沒有自己開發的作業系統。

https://udn.com/news/story/7339/5820540?from=udn-relatednews_ch2

其實,有沒有自己開發的作業系統,並非首要,反而是對先進作業系統的深入研究,使其能和產業整合,成為基礎設施、國防工業、航太、汽車、醫療等生態系的一部份,才更為重要。

例如:seL4 微核心,是世界上最先進、最可靠的操作系統核心,在數學上已被證明為最安全的(bug-free)高效率核心(美國軍方也已採用 seL4 )。

2020 年 Linux 基金會宣佈將擴大支持 seL4 微核心,新基金會旨在加速 seL4 及相關技術的發展;在 Linux 基金會的保證下,將提供一個全球性、獨立和中立的組織,用於資助和指導 seL4 的未來發展。

https://www.linuxfoundation.org/press/press-release/sel4-microkernel-optimized-for-security-gets-support-of-linux-foundation

未來台灣若真的成立數位發展部,應該要朝 seL4 大力發展才對(https://sel4.systems/),而不是還在自陷糾結於開發自有作業系統的啟蒙階段。

這位教授屢有建言,立意良好,但若沒有切中前瞻,走偏了方向,繞大了寃枉路就不好了。