專訪哈工大朱曉蕊教授：系統安全會成為無人機未來的重要問題

雷鋒網 AI 科技評論按：日前，哈工大朱曉蕊教授等人在中國工程院院刊《信息與電子工程前沿》（英文）（Frontiers of Information Technology & Electronic Engineering，FITEE）上發表了一篇題為《針對無人機系統安全的新型層級式軟體架構》（A new hierarchical software architecture towards safety-critical aspects of a drone system）的論文，提出一種覆蓋底層源代碼到上層用戶任務代碼的新型層級式軟體架構，能夠有效地提高無人機系統安全性與可靠性。

目前，對於基礎技術日趨成熟的無人機領域來說，無人機系統的安全性還是一個欠缺關注的研究方向，然而，這一研究方向對於無人機未來發展而言至關重要。因而，朱曉蕊教授等人在這一方向上的研究頗具前瞻性，其工作成果也獨具開創性意義。雷鋒網 AI 科技評論藉此機會拜訪了朱曉蕊教授，深入探討了其開啟這項工作的背景、研究歷程以及對於無人機領域的一些思考。

實際上，在無人機系統安全這個項目之前，朱曉蕊教授的研究方向主要是無人機控制和導航，而之所以轉到無人機系統安全的研究則源自於她與耶魯大學邵中教授一次對話中受到的啟發：系統安全會成為無人機等小型智能系統未來的一個重要問題。

2014 年底，朱曉蕊教授在與來自耶魯大學的邵中教授進行學術交流的過程中，了解到邵中教授一直在進行安全操作系統方面的研究，並在這個領域處於國際最前沿。而當時還在專註於無人機控制、導航研究的朱曉蕊教授，意識到她此前所做的這些研究工作實際上都已經趨向成熟，正在思考無人機未來的研究方向，邵中教授的這一研究方向則帶給了她一個新的研究思路。朱曉蕊教授在採訪中「他正在做這項工作就提醒了我，無人機這類小型智能系統的安全問題，會成為未來一個比較重要的問題 」。

然而，當時甚至是現在，無人機領域對於安全性問題的關注度都比較少。對此，朱曉蕊教授指出：「需要注意的一點是我們研究的基本上是小型飛行器，而小型飛行器和大型飛行器的區別是非常大的。光就安全性而言，大型飛行器很早就按照 Safety Critical System 啟用了標準度很高的 系統安全驗證，雖然在安全驗證方面的人力、物力的耗費量都非常巨大，但是它們的一個小小的安全問題就可能帶來非常嚴重的後果，因而即便投入巨大，大家也不得不關注這一問題。然而對於小型飛行器的安全驗證問題，目前領域內國際上只有極少數研究者開始嘗試去做這些事情，因為這是一個全新的東西，一切都從新開始。」

正是基於上面的兩點考量，朱曉蕊教授決心要成為「第一批吃螃蟹的人」，與邵中教授開啟了無人機系統安全的研究項目。

「當無人機這類智能系統進入到民用領域後，就不可避免地走向小型化，就會在片上資源方面犧牲掉很多的性能，因此直接將大型飛行器的安全驗證系統移植到小型飛行器上是不可行的，所以我們就需要設計一個新的軟體架構，既保證小型飛行器理論驗證消耗不會那麼高，又能夠保障系統的安全性。傳統而言，新系統研發是通過反覆地模擬和實際測試來確保系統可靠性和安全性的。但是這種方式從嚴格意義上是無法完全保證安全性的，會出現看似隨機的一些故障，甚至引起飛機墜毀現象。」

同時，為了促成雙方正式將無人機系統安全項目提上重要日程，朱曉蕊教授和邵中教授也特地正式申請了國際合作項目。

按照朱曉蕊教授的說法，研究上層系統的人通常並不關注底層系統的細節，只在需要的時候直接使用底層系統，而反過來，研究操作系統的人往往也很少考慮上層系統的情況。因此，無人機等智能系統的上層系統和底層操作系統之間相當於存在一塊「隔板」，二者間往往只存在最基本的互動。

「這樣的話，這兩個方向的研究者在進行安全測試時，往往只測試各自系統內的交互情況，然而這樣僅僅只能確保系統內的安全性，而不能保證上層系統在跟底層操作系統做交互的時候不會出現問題。因此，我們合作這個項目的思路就是要將這兩個系統中間的這塊隔板打開，將二者作為一個整體來設計軟體架構，從而完全保證無人機系統的安全性。」

對於這項工作成果在保障無人機整體安全性上的具體工作原理，朱曉蕊教授介紹道：「我們將所有演算法形成的代碼設計成分層結構，同時設計好層與層之間的交互架構，然後使用形式化驗證的方法去檢測層與層之間交互的正確性。」

形式化驗證是採用邏輯來驗證程序可靠性的一種方法，即用邏輯的方法將一段程序證明一遍，證明它能得到預期的結果並且沒有出現錯誤，例如，歐美國家就將這種驗證方法廣泛地應用於一些大型飛行器中，由於這些設備的系統一旦出現出現錯誤，導致的後果會非常嚴重，同時研究者又無法對其進行一遍一遍的測試，因而形式化驗證是可以選擇的非常不錯的方法。

因此，朱曉蕊教授項目組的這項研究成果不僅以實現上層系統和底層操作系統的層級式互動的方式來保障系統整體的安全性，更從邏輯層面避免了人為測試中所存在的偶然性，保障了安全性和可靠性。而同時從這兩個方面著手展開（小型）無人機系統安全測試工作的，朱曉蕊教授等人是首創者。

實際上，無人機系統安全這個合作項目在 2014 年底就啟動了，然而一直到現在才出成果，朱曉蕊教授表示背後的原因主要有兩點：

• 一是合作項目的人員投入以及相關人員的時間投入都非常緊缺。一般而言，朱曉蕊和邵中兩位教授每年大概各自投入 1 到 2 名研究生，再加上學生推進相關研究工作的時間有限，因而整個研究的推進節奏是比較慢的。

• 二是交叉學科之間對於彼此學科的理解難度以及研究理念上的差異。「這也是我們在合作研究中遇到的一個比較大的挑戰，我和邵中老師以及我們各自的學生，研究方向其實是不同的，我們是典型的交叉研究領域，因此我這邊的學生需要去了解很多操作系統方面的東西，邵中老師的學生同樣也需要重新理解上層系統的相關知識，所以他們彼此都要花很多時間去學習這些知識，這中間其實也耗費了非常多的時間。」

此外，朱曉蕊教授還提到了她這邊存在的一個比較嚴峻的問題，就是在現行的培養體制下，一方面是由於研究生培養年限比較短，另一方面則是因為學生對於新事物的熱情和好奇心也不夠，畏難心理比較明顯，因此她這邊參與項目的學生更替很快，這樣的話，輪到下一批加入的學生，他們又要去學習操作系統方面的知識，這就又需要耗費一個周期的時間了。

談及至此，朱曉蕊教授也就目前國內高校學生存在的一些問題提出了兩點自己的期望：

• 第一是增強自身對學術科研的熱愛和好奇心，減少學術功利性。「實際上現在很多學生不是因為熱愛才去做科研，所以他們往往會以企業需要求職者擁有怎樣的技能為衡量標準來做項目，功利性比較強。這樣的心態一方面讓他們在遇到困難時就會產生畏難心理，另一方面他們一旦拿到比較好的 offer 就傾向於選擇去就業，這些因素都會導致他們無法進行深度科研。」

• 第二是要有自己的獨立思考和判斷能力，不要盲目跟風追熱點。「現在很多學生都在跟熱點做研究，我覺得最關鍵的原因是他們沒有判斷力，無法獨立思考目前領域發展中重要的方向，同時也缺乏對自己的判斷和思考，因此跟熱點是一種相對來說比較安全的方式。但是現在以及未來，整個社會的變化都非常快，因此現在即便是熱點，過段時間說不定就冷掉了，而一些冷門的方向說不定到某個時間就發展起來了。」

也正是基於這種期望，朱曉蕊教授在日常教學中也始終堅持引導學生樹立正確的研究思路：「所以我也一再地跟我的學生強調，我要教給他們的是一套系統的做科學研究的方法論，是怎樣從零或一個 idea 開始做出一套有說服力的成果的方法，讓他們最終在畢業答辯的時候能夠自信地將自己做出來的這些成果講給別人聽，而不是說一定局限在課題所涉及的特定研究領域。」

對於無人機系統安全研究的這一版研究成果，朱曉蕊教授表示，目前還沒有達到最理想的狀態，因此下一步的規劃還是希望參與研究的學生能夠再花半年到一年左右的時間，實現該方案的最佳效果。

「下一步，我們會利用虛擬化技術來完善無人機系統安全方案，具體來說就是用虛擬化技術來將智能系統中對安全重要和對安全沒那麼重要的部分隔開來，從而減少不必要的安全驗證消耗 。以無人機為例，它其中的某些模塊對於安全來說至關重要，一旦出現問題，可能會直接導致無人機停止運行（從空中掉下來）；而其中也有部分模塊對安全性而言不那麼重要的，例如一些第三方程序，對於飛機整體的安全性不會造成太大影響，就不需要付出代價去證明這部分模塊的安全性。因此，大概再花一年左右的時間，整個安全方案就比較完整了。」

同時，朱曉蕊教授希望，這一系統安全性驗證方案不要被局限於無人機。「它同樣可以給其他小型智能系統包括無人駕駛帶來很大的價值。實際上，這個方案如果應用到無人駕駛這些場景中，實現原理其實還是一樣的，只不過需要針對這一套系統進行修改和調整，因此說，我們實際上提出的是一套可以廣泛應用的方法論。」

而對於目前每年只能各自投入 1 到 2 名學生的耶魯合作項目來說，人手同樣是一個亟需解決的問題，因此擴充科研隊伍同樣也是下一步規劃中的重要內容。

「本次之所以希望通過媒體來報道這項成果，主要也是有兩個訴求：第一個就是希望更多對這項研究感興趣的人能夠加入到我們的研究隊伍中來，從而更快地推進項目進度；第二個就是希望我們在無人機系統安全方面的這項研究成果能給相關領域研究者帶來一些啟發，啟發他們去挖掘領域內目前還未受到較大關注但對未來而言至關重要的研究方向。」

學界和業界應該怎麼分工？

朱曉蕊教授認為，學界和業界由於各自的性質以及承擔的社會責任不同，分工也不盡相同，如果二者能夠各司其職，形成一個非常良性、平衡的合作狀態，對於無人機以及整個人工智慧領域的發展會大有裨益。

「對於學界而言，首先一定要做一些超前的事情，在一些業界乃至整個研究領域還沒有關注到的問題上，先要嘗試著去開展研究工作，所有的研究工作往往在獲得成功之前都要經歷一個漫長的過程，所以，學界應該充當這個引路者的角色；其次，我認為學界的價值是提出一些能夠對業界具有啟發性意義的新的 idea，正如我之前所提到的，我們的研究實際上更像是提出了某一套具有普遍適應性的新方法，業界可以借鑒，並在我們的新思路和新方法上進行完善，從而最終與真正的應用場景實現對接。

而對於業界來說，他們需要做的便是將學界提出的新方法、新成果落地到各個細分應用場景中，並利用其豐富的人力、物力資源來推進某項成果不斷完善和升華，最終對整個社會的實際發展負責。」

無人機領域的最終目標為何？

對於目前無人機領域的整個發展情況，朱曉蕊教授還是比較有信心的，她認為在技術層面，無人機的通用性已經做得相對來說比較成熟的，接下來要著重解決的就是產業化落地的問題。

「目前就我看來，無人機領域在基礎技術方面都不錯，就差在細分行業中有針對性地應用了。因為不同的細分行業對於這些基礎技術都有特殊且具體的要求，因此我認為這其中還有很多可以挖掘的東西。當技術和市場、成本達到一個平衡的狀態時，無人機領域差不多就是一個比較理想的狀態了。」

論文：《針對無人機系統安全的新型層級式軟體架構》

作者：朱曉蕊，梁辰，殷振國，邵中，劉孟啟，陳昊

中文摘要：本文提出了一種覆蓋從底層源代碼到上層用戶任務代碼的新型層級式軟體架構，用於提高無人機系統的安全性與可靠性。在這種軟體架構下，每一個軟體模塊採用形式化驗證的方法驗證其源代碼符合設計規範，而且這些軟體模塊基於經過形式化驗證的操作系統內核CertiKOS，因而從理論上保證無人機系統不存在軟體漏洞。考慮到無人機的機載感測器會對系統可靠性產生顯著影響，本文對驅動感測器的SPI匯流排與I2C匯流排進行形式化驗證，並針對匯流排異常的情況設計完成相關實驗。實驗結果表明此類軟體架構能有效提高無人機系統安全性與可靠性。

關鍵詞：安全關鍵系統；無人機；軟體架構；形式化驗證；

本文引用格式：

Xiao-rui Zhu, Chen Liang, Zhen-guo Yin, Zhong Shao, Meng-qi Liu, Hao Chen, 2019. A new hierarchical software architecture towards safety-critical aspects of a drone system. Frontiers of Information Technology & Electronic Engineering, 20(3): 353-362.

https://doi.org/10.1631/FITEE.1800636雷鋒網

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！