DO-332幫助解決OOT的動態(tài)靈活性關鍵認證挑戰(zhàn)

DO-332是DO-178C標準對面向對象技術（OOT）和相關技術的補充，分析了安全關鍵軟件中面向對象引發(fā)的問題，并為處理OOT的漏洞提供了新的指導。DO-332的一個重要新目標是“本地類型一致性驗證”，它利用了稱為“Liskov替換原理”的類型理論結果，并幫助解決OOT的動態(tài)靈活性帶來的一些關鍵認證挑戰(zhàn)。

面向對象技術（OOT）被廣泛使用，并得到包括C++，Java和Ada在內(nèi)的一系列編程語言的支持，但由于各種原因，它的普及尚未擴展到機載和其他安全關鍵軟件。根本問題是驗證利用OOT三個基本元素的軟件的復雜性：繼承，多態(tài)性和動態(tài)綁定。（圖 1 說明了面向對象的基礎知識。一個簡單的例子說明了這些問題：

圖1：面向對象基礎知識

假設 Sensor 類是繼承層次結構的根，ref 是對此層次結構中任何類中的對象的多態(tài)引用，而 Reset 是為不同的 Sensor 類定義不同的操作。聲明參考。Reset（。..） 根據(jù) ref 表示的對象的類動態(tài)綁定到相應的版本。如何驗證此調(diào)用是否滿足重置操作的要求？

如果使用繼承來定義不是傳感器專用化的子類，則會出現(xiàn)一個問題。此子類的重置可能具有與重置傳感器無關的某些效果，或者可能會生成異常。ref 從這樣的子類引用對象將是一個錯誤，需要分析以表明錯誤不會發(fā)生。這使驗證過程復雜化。

另一個問題涉及結構覆蓋率分析。對于 DO-178 標準中三個最高級別（A、B 或 C）中的任何一個的系統(tǒng)，必須使用基于需求的測試來證明完整的語句覆蓋率。但是，編譯器可能會選擇幾種實現(xiàn)策略來處理動態(tài)綁定，這些策略對“語句覆蓋率”的含義有不同的含義。結構覆蓋范圍的范圍不應取決于編譯器使用的實現(xiàn)策略。

DO-332［1］是DO-178C［2］的OOT補充，通過局部類型一致性的新概念解決了這些問題，該概念利用了繼承只應用于類專用化的原則。

繼承和利斯科夫替代原則

在面向對象的設計中，系統(tǒng)的體系結構反映了類及其關系。一個特別重要的關系是專業(yè)化（“is a”），但還有很多其他關系。實現(xiàn)設計涉及選擇用于捕獲關系的語言機制。

在面向對象的語言中，繼承可用于實現(xiàn)兩個類之間的各種關系。但是，當繼承用于專用化以外的任何內(nèi)容時，可能會出現(xiàn)異常，因為為超類定義的操作可能對子類沒有意義。在類型論的背景下，已經(jīng)研究了將繼承限制為專業(yè)化關系，其中它被稱為Liskov替換原理（LSP）［3］。非正式地說，LSP 意味著無論在哪里可以使用超類的實例，都應該允許替換任何子類的實例。

使用繼承進行專業(yè)化與操作的前置條件和后置條件（其“協(xié)定”）具有重要的交互作用。前提條件是在調(diào)用操作時對程序狀態(tài)所做的假設。后置條件是保證操作在操作完成時對程序狀態(tài)進行的操作。前置和后置條件可以明確指定 - 可以在源文本中指定，如Ada 2012［4］或SPARK［5］，也可以單獨指定 - 或者它們可以隱含在操作邏輯中。

如果繼承符合 LSP，則操作的子類版本不應施加比超類版本更強（更具限制性）的前提條件。否則，調(diào)用可能在某些情況下（在超類實例上）成功，但在其他情況下（在子類實例上）失敗。類似地，子類的操作版本不應指定比超類版本更弱（更通用）的后置條件。

因此，符合 LSP 意味著滿足兩個屬性：

協(xié)定一致性：任何子類操作都不會加強它所覆蓋的超類操作的前置條件或削弱后置條件。

行為一致性：每個子類操作都滿足其超類的要求。

DO-332 在新目標“本地類型一致性驗證”中捕獲了這些概念。此目標不需要證明類層次結構符合 LSP，這將過于嚴格。相反，它反映了對于符合要求的類體系結構，驗證工作更簡單，并且分析只需要考慮本地上下文。

本地類型一致性

圖 2 顯示了與驗證本地類型一致性相關的活動，DO-332 需要 A、B 或 C 級別的軟件。“對于使用替換的每個子類型”的措辭是指發(fā)生動態(tài)綁定的上下文，例如 ref。Reset（。..），所討論的“子類型”是 ref 在這一點上可以引用的對象的類。潛在的類不一定是完整的層次結構，不同的類集可能適用于同一操作的不同調(diào)用。

圖2：與驗證本地類型一致性相關的活動，DO-332 要求級別為 A、B 或 C 級軟件

考慮引用的特定出現(xiàn)。Reset（。..），并讓 HeatSensor 成為 ref 可以在那里引用的對象可能的子類之一。引用的本地類型一致性。HeatSensor的重置（。..）可以“樂觀地”或“悲觀地”地證明。如果HeatSensor滿足LSP，則樂觀方法有效，可以通過兩種方式進行：

通過形式化方法，通過證明HeatSensor的復位版本滿足傳感器版本的要求，并且不會加強傳感器復位的前置條件或削弱后置條件。

通過測試，通過使用 HeatSensor 的實例對傳感器的重置版本運行基于要求的測試。

來自編程語言及其工具集（例如 Ada 2012 或 SPARK）的適當支持可以促進形式化方法。

樂觀的方法將證明超類和子類的操作版本之間的契約和行為一致性。通過對子類的基于需求的測試以及可能通過形式化方法獲得額外的驗證。

如果類不符合 LSP，或者動態(tài)綁定調(diào)用很少，或者層次結構很淺和/或很窄，那么測試可能出現(xiàn)的每種可能的情況可能是最簡單的。這是圖 2 中第三個項目符號項中指定的悲觀測試。需要基于需求的測試來對可能出現(xiàn)的每個子類執(zhí)行操作。

DO-332、本地類型一致性和 LSP 指南認證

本地類型一致性驗證只是安全使用 OOT 的一個方面;DO-332 包含有關其他 OOT 元素以及相關技術（如通用模板）的指南。DO-332 是“語言不可知論者”;有關如何使用 Ada 2012 作為編程語言在安全關鍵或高安全性系統(tǒng)中應用 OOT 的更多細節(jié)［6］。

DO-332 的本地類型一致性指南與 DO-178C 的一般驗證方法一致，確保所有測試都基于要求。它以一種新穎的方式調(diào)整驗證活動，以反映面向對象的語義和類結構對LSP的遵守程度。新指南應有助于促進面向對象編程（OOP）在航空電子設備和其他關鍵領域的安全使用。

審核編輯：郭婷