Noninterference 不干擾模型深度解析：Goguen-Meseguer 架構如何從根源封堵隱密通道資訊洩漏

Noninterference 不干擾模型深度解析：Goguen-Meseguer 架構如何從根源封堵隱密通道資訊洩漏

什麼是 Noninterference（不干擾模型）？

在多層級安全系統中，資訊洩漏的最大威脅往往不來自直接存取，而是隱密通道（Covert Channel）。Goguen 與 Meseguer 於 1982 年提出的不干擾模型，從數學層面定義了一條清晰的安全邊界。

不干擾模型的核心主張是：高安全級別（High）主體的所有動作，對低安全級別（Low）主體的可觀察輸出不產生任何影響。 換言之，無論 High 端執行了什麼操作，Low 端看到的系統狀態必須完全一致。這不只是存取控制，而是對資訊流動本身的根本性封堵。

形式化定義如下：設系統狀態轉移函數為 M，若將所有 High 動作從執行序列中移除後，Low 端的可觀察輸出 outputs_L 保持不變，則稱系統滿足 Noninterference。

如何從根源封堵隱密通道？

傳統存取控制（如 Bell-LaPadula）僅規範「誰能讀寫哪些資源」，卻無法防禦時序通道（Timing Channel）與儲存通道（Storage Channel）等隱性洩漏路徑。Noninterference 直接對系統的輸入輸出行為建立語意約束，不依賴具體的通道型態。

舉例而言，即使 High 端透過快取佔用、磁碟忙碌訊號等側通道間接傳遞訊息，只要 Low 端可觀察的輸出序列產生變化，系統即違反 Noninterference。此模型的強大之處在於它對「洩漏」的定義是行為語意，而非機制。

-- 虛擬碼：Noninterference 驗證邏輯
verify_noninterference(trace_full, trace_purged_high):
    obs_full   = observe_low(trace_full)
    obs_purged = observe_low(trace_purged_high)
    return obs_full == obs_purged  -- 必須完全相同

💡 重點整理

行為語意封堵：約束的是可觀察輸出，而非特定通道類型。
移除高端動作測試：將 High 動作清除後，Low 端輸出若改變即為違規。
優於存取控制：能防禦 Bell-LaPadula 無法處理的隱密通道。
形式驗證基礎：可與模型檢驗工具（如 Isabelle/HOL）整合進行嚴格證明。

Noninterference 並非萬能，其嚴格性在實務中可能過於保守，需搭配資訊流型別系統（Information Flow Type Systems）或安全標籤傳播機制落地應用。理解此模型，是設計真正抵禦隱密通道的系統架構的第一步。

📚 參考文獻

Goguen, J. A. & Meseguer, J. (1982). Security Policies and Security Models. IEEE Symposium on Security and Privacy — 不干擾模型的原始提出論文，定義核心語意框架。
McLean, J. (1994). A General Theory of Composition for Trace Sets. IEEE S&P — 擴展 Noninterference 至組合系統的權威延伸研究。
Sabelfeld, A. & Myers, A. C. (2003). Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications — 介紹如何將不干擾概念落實於程式語言層級。