王一華,周 晴,胡婉如,杜家昊

(1.中國科學(xué)院 國家空間科學(xué)中心,北京 100190;2.中國科學(xué)院大學(xué),北京 100049)

0 引 言

控制器局域網(wǎng)絡(luò)(Controller Area Network,CAN)是一種具有高性能的高速串行現(xiàn)場總線,航天、航空、軌道交通等領(lǐng)域常用其作為通信總線。該安全關(guān)鍵領(lǐng)域涉及人員、空間飛行器安全,需對路徑死鎖、時(shí)序沖突、攻擊者入侵等重大風(fēng)險(xiǎn)進(jìn)行嚴(yán)謹(jǐn)?shù)姆抡媾c驗(yàn)證[1],并給出風(fēng)險(xiǎn)評估和改進(jìn)方案以減少軟件失效帶來的慘痛損失。在軟件需求分析階段[2]開展建模分析,可盡早發(fā)現(xiàn)軟件系統(tǒng)設(shè)計(jì)缺陷,大幅提升系統(tǒng)的安全性、可靠性與高效性[3]。形式化方法[4]采用嚴(yán)格的數(shù)學(xué)描述,可對狀態(tài)跳轉(zhuǎn)與時(shí)序約束進(jìn)行嚴(yán)謹(jǐn)有效、可解釋性強(qiáng)的驗(yàn)證,已廣泛用于通信協(xié)議與總線的建模與驗(yàn)證。

目前,已有很多關(guān)于CAN總線形式化建模相關(guān)的優(yōu)秀工作。Krakora等人[5]提出了一種用時(shí)間自動(dòng)機(jī)建立CAN總線模型,采用UPPAAL對其時(shí)態(tài)邏輯描述的屬性進(jìn)行形式化驗(yàn)證。隨后,Rodriguez-Navas等人[6]更加細(xì)致地驗(yàn)證了CAN總線模型的容錯(cuò)時(shí)鐘同步機(jī)制,證明了其在單點(diǎn)故障的情況下仍舊可以保證2 μs量級的通信精度。但在上述研究中,前者只針對協(xié)議的數(shù)據(jù)鏈層進(jìn)行建模,后者同樣只分析了故障對通信時(shí)鐘的影響,并未將CAN總線協(xié)議的潛在不穩(wěn)定性因素同時(shí)考慮在內(nèi)。Pan等人[7]對CAN應(yīng)用層進(jìn)行了建模與驗(yàn)證,主要驗(yàn)證了消息調(diào)度算法與節(jié)點(diǎn)恢復(fù)機(jī)制。孟瑤等人[8]對CAN總線控制的機(jī)器人關(guān)節(jié)通信這一應(yīng)用場景進(jìn)行了建模和驗(yàn)證。Wang等人[9]建立了CAN總線在CPS系統(tǒng)中的時(shí)間自動(dòng)機(jī)模型。但上述研究的驗(yàn)證部分只對CAN總線的安全性、節(jié)點(diǎn)可達(dá)性等基本性質(zhì)進(jìn)行驗(yàn)證,沒有涉及時(shí)序相關(guān)的應(yīng)用場景。

此外,在CAN總線風(fēng)險(xiǎn)分析領(lǐng)域,2021年Hnaini等人[10]提出了一種將定性風(fēng)險(xiǎn)分析與形式化方法相結(jié)合的方法,用來對具有大量攻擊者的汽車預(yù)訂系統(tǒng)的安全屬性進(jìn)行驗(yàn)證。Batista等人[11]介紹了關(guān)于通信總線上故障仿真器的設(shè)計(jì)與實(shí)現(xiàn),其中故障仿真器支持互操作性和穩(wěn)健性的驗(yàn)證。Kim等人[12]針對Mauth-CAN協(xié)議進(jìn)行了形式化的建模驗(yàn)證,驗(yàn)證了該協(xié)議對CAN總線上的消息泛洪攻擊具有健壯性,但該工作沒有針對CAN總線模型自身的抗攻擊性進(jìn)行研究?？傮w而言,采用形式化方法分析CAN總線健壯性的研究仍然存在不足。

本文針對嵌入式系統(tǒng)CAN總線時(shí)序分析建模與風(fēng)險(xiǎn)量化存在的問題,提出了一種可開展CAN總線系統(tǒng)健壯性分析的建模驗(yàn)證方案。該方案基于航天嵌入式通信系統(tǒng)的軟件需求,構(gòu)建CAN總線系統(tǒng)形式化模型;基于CAN總線數(shù)據(jù)鏈路層與應(yīng)用層開通信協(xié)議抗攻擊性能分析;通過模型驗(yàn)證結(jié)果,改進(jìn)總線通信系統(tǒng)設(shè)計(jì)與優(yōu)化需求參數(shù),提高總線健壯性,有效提升節(jié)點(diǎn)傳輸準(zhǔn)確率與應(yīng)答正確率,為CAN總線嵌入式軟件需求改進(jìn)提供了理論指導(dǎo)。

1 設(shè)計(jì)方案

為了驗(yàn)證CAN總線系統(tǒng)在攻擊風(fēng)險(xiǎn)下的通信時(shí)序安全性能,通過對比有無攻擊兩種情況下應(yīng)用層的通信效率,衡量CAN總線系統(tǒng)的健壯性。通常,航天CAN總線應(yīng)用層通信的時(shí)序需求有三類。第一類是總線發(fā)送數(shù)據(jù)時(shí)間要求,如復(fù)合幀幀間間隔時(shí)間不超過0.5 ms,廣播時(shí)間碼周期為1±0.2 s,輪詢某從屬節(jié)點(diǎn)應(yīng)答數(shù)據(jù)包周期為0.5 ms;第二類為應(yīng)答時(shí)間要求,如應(yīng)答幀響應(yīng)時(shí)間不超過2 ms,否則視為超時(shí);第三類為總線故障恢復(fù)時(shí)間要求,當(dāng)CAN總線發(fā)送錯(cuò)誤寄存器或接收錯(cuò)誤寄存器任何一個(gè)寄存器的計(jì)數(shù)大于90時(shí),重新初始化該總線控制器,其中軟件初始化時(shí)間小于50 s。

以上時(shí)間約束設(shè)計(jì)能滿足常規(guī)通信性能要求,但軟件實(shí)際運(yùn)行中經(jīng)常面臨各種攻擊風(fēng)險(xiǎn)。如航天軟件傳輸數(shù)據(jù)時(shí),受宇宙空間效應(yīng)影響,可能出現(xiàn)單粒子翻轉(zhuǎn)、鎖定等現(xiàn)象,從而導(dǎo)致總線通信異常;或因載荷自身故障,導(dǎo)致載荷向總線持續(xù)發(fā)送異常報(bào)文。在地面CAN總線廣泛的應(yīng)用中,惡意攻擊的情況更是不在少數(shù)。故在上述可能存在的攻擊下,驗(yàn)證CAN總線是否仍能滿足應(yīng)用層時(shí)序需求非常有意義。

本文構(gòu)建了包含1個(gè)主節(jié)點(diǎn)、4個(gè)從節(jié)點(diǎn)的5節(jié)點(diǎn)CAN總線模型,其中,主節(jié)點(diǎn)具有最高優(yōu)先級,從而節(jié)點(diǎn)需滿足“不與其他從節(jié)點(diǎn)交流信息、不在非應(yīng)答的情況下主動(dòng)發(fā)送消息至總線其他節(jié)點(diǎn)”兩個(gè)規(guī)則。根據(jù)CAN總線應(yīng)用層故障恢復(fù)設(shè)計(jì),節(jié)點(diǎn)的收發(fā)控制器對總線節(jié)點(diǎn)通信時(shí)的錯(cuò)誤報(bào)文進(jìn)行鑒別并進(jìn)行錯(cuò)誤計(jì)數(shù);當(dāng)CAN總線上存在節(jié)點(diǎn)崩潰、泛洪攻擊等情況時(shí),發(fā)送錯(cuò)誤計(jì)數(shù)設(shè)置了一個(gè)閾值Transmit Error Counter(TEC),超過閾值則進(jìn)行總線復(fù)位,重啟并初始化總線。

圖1為CAN總線主控制器模型的交互圖,模擬了主控制器識別并發(fā)送報(bào)文的行為,針對不同的報(bào)文類型分別發(fā)送對應(yīng)的同步信號或進(jìn)行相關(guān)的更新操作。除此之外,為便于總線抗攻擊性能的測試,對總線應(yīng)用層及多節(jié)點(diǎn)仲裁的數(shù)據(jù)鏈路層也進(jìn)行了形式化建模工作。CAN總線嵌入式軟件通信系統(tǒng)健壯性的衡量指標(biāo)為時(shí)間約束能否較好地在特定設(shè)計(jì)情況下被滿足,數(shù)據(jù)傳輸耗時(shí)由發(fā)送時(shí)間與仲裁時(shí)間組成,因此需在模型中合理對兩者進(jìn)行量化。發(fā)送時(shí)間通過設(shè)置狀態(tài)的時(shí)間速率進(jìn)行量化;為更精準(zhǔn)地量化仲裁時(shí)間和減少模型的狀態(tài)空間數(shù)量,將按位仲裁計(jì)算部分設(shè)置為原子操作,仲裁總耗時(shí)的衡量通過為關(guān)鍵節(jié)點(diǎn)增加時(shí)間不變量約束來實(shí)現(xiàn)。

圖1 CAN總線主控模型

2 CAN總線形式化模型

本節(jié)介紹CAN總線模型的構(gòu)建。模型對主從節(jié)點(diǎn)的數(shù)據(jù)收發(fā)、控制器故障處理、優(yōu)先級仲裁、應(yīng)用層需求進(jìn)行關(guān)鍵行為提取與抽象。CAN總線時(shí)間自動(dòng)機(jī)模型中的變量名及其含義見表1。

表1 模型中的變量定義與含義描述

2.1 主控制器建模

圖2所示為CAN總線主控制器時(shí)間自動(dòng)機(jī)模型Main_Controller,模型包含主控制器節(jié)點(diǎn)發(fā)送報(bào)文后CAN總線上的不同操作。使用Uppaal SMC的概率分支實(shí)現(xiàn)不同報(bào)文不同發(fā)送順序的隨機(jī)組合,將數(shù)量為msg_Num的報(bào)文分成4組隨機(jī)發(fā)送,覆蓋了正常發(fā)送和異常發(fā)送的各種情況。本文用4個(gè)數(shù)字標(biāo)識不同的報(bào)文類型,0代表錯(cuò)誤報(bào)文,1代表重置報(bào)文,2代表主節(jié)點(diǎn)發(fā)送廣播報(bào)文或無需應(yīng)答的點(diǎn)對點(diǎn)報(bào)文,3代表需要從節(jié)點(diǎn)應(yīng)答的報(bào)文。若總線檢測到錯(cuò)誤報(bào)文,進(jìn)行傳輸錯(cuò)誤計(jì)數(shù),txErr_Cnt到達(dá)閾值TEC時(shí),總線會(huì)發(fā)送重置報(bào)文進(jìn)行總線的初始化。此時(shí),狀態(tài)ResetType發(fā)送重置信號reset!與模板Node_Applicition進(jìn)行通信,直到CAN總線重新初始化結(jié)束,模板收到reset_Done?信號后完成本次傳輸。若為類型2,則發(fā)送send!同步信號與模板Node_Applicition進(jìn)行通信,直到完成應(yīng)用層數(shù)據(jù)傳輸。若類型為3,對報(bào)文ID繼續(xù)使用guard_Node()函數(shù)判斷哪個(gè)節(jié)點(diǎn)需要應(yīng)答,發(fā)送reply_Req[id]!通知相應(yīng)的從屬節(jié)點(diǎn)準(zhǔn)備數(shù)據(jù)回復(fù)應(yīng)答。

圖2 CAN總線主控制器時(shí)間自動(dòng)機(jī)模型

2.2 從屬節(jié)點(diǎn)建模

圖3為各個(gè)從屬節(jié)點(diǎn)進(jìn)行報(bào)文應(yīng)答的時(shí)間自動(dòng)機(jī)模型。當(dāng)從節(jié)點(diǎn)txNode(i)收到需要回復(fù)的reply[id]?信號時(shí),應(yīng)答時(shí)鐘rep_Time開始計(jì)時(shí)。節(jié)點(diǎn)的控制器進(jìn)行報(bào)文解析并按照接收報(bào)文的要求進(jìn)行準(zhǔn)備需要回復(fù)的內(nèi)容,函數(shù)judge()判斷報(bào)文是否符合要求,識別并過濾攻擊報(bào)文?？蔀槊總€(gè)節(jié)點(diǎn)設(shè)置不同的發(fā)送速率實(shí)現(xiàn)發(fā)送的“時(shí)序隨機(jī)性”,模擬真實(shí)的數(shù)據(jù)傳輸。在仲裁階段,當(dāng)偵測到總線空閑時(shí),從節(jié)點(diǎn)發(fā)送仲裁請求arb[i][e]!后進(jìn)入等待仲裁狀態(tài)。若仲裁成功,可占用總線進(jìn)行數(shù)據(jù)傳輸,此時(shí)將應(yīng)答時(shí)間rep_Time與需求文檔中規(guī)定的CAN總線應(yīng)答最低時(shí)間限制t_UppLim進(jìn)行比較,在規(guī)定時(shí)間內(nèi)完成傳輸視為應(yīng)答成功,到達(dá)RepSucc位置,否則視作應(yīng)答失敗。

圖3 CAN總線從屬節(jié)點(diǎn)時(shí)間自動(dòng)機(jī)模型

2.3 仲裁器建模

圖4為模板Arbitration,表示了報(bào)文發(fā)送前按位仲裁的完整過程。當(dāng)接收到arb[i][e]?信號時(shí),設(shè)置狀態(tài)機(jī)邊上的局部變量,i代表需要回復(fù)消息的節(jié)點(diǎn)標(biāo)識,e標(biāo)識應(yīng)答報(bào)文的ID值即表明回復(fù)的是哪一條消息。每條消息有11個(gè)有效比特位,二維數(shù)組rep[e][11]表示第e條應(yīng)答報(bào)文。按位仲裁過程為:首先設(shè)置一個(gè)全為1的數(shù)組signal[11],將每個(gè)報(bào)文的對應(yīng)位與之相乘,將乘積值signal[s]與報(bào)文對應(yīng)位比較,若相等則該報(bào)文可參與后續(xù)仲裁,不相等則該報(bào)文仲裁失敗,發(fā)送arb_Fail[id]!信號通知節(jié)點(diǎn)仲裁失敗;其次將11位的每一位都進(jìn)行如上循環(huán)判斷;最后決出勝利者發(fā)送arb_Succ[id]!信號結(jié)束仲裁。

圖4 逐位仲裁器時(shí)間自動(dòng)機(jī)模型

2.4 總線應(yīng)用層建模

圖5為CAN總線嵌入式軟件系統(tǒng)應(yīng)用層數(shù)據(jù)傳輸?shù)臅r(shí)間自動(dòng)機(jī),模擬了總線數(shù)據(jù)發(fā)送與總線重置兩種情況下的行為。初始狀態(tài)Idle收到發(fā)送信號send時(shí),模型發(fā)送receive!信號與主節(jié)點(diǎn)通信表示收到指令,并開始數(shù)據(jù)發(fā)送。發(fā)送數(shù)據(jù)包計(jì)數(shù)應(yīng)不小于幀數(shù),以8幀數(shù)據(jù)為例模擬數(shù)據(jù)發(fā)送過程。當(dāng)數(shù)據(jù)完成發(fā)送時(shí)進(jìn)行發(fā)送時(shí)長的統(tǒng)計(jì),將其與最大發(fā)送時(shí)間限制t_Done_Time進(jìn)行比較,若發(fā)送時(shí)長t_DataSend大于t_Done_Time則判斷為超時(shí),小于t_Done_Time則判斷為正確發(fā)送。初始狀態(tài)Idle收到總線重置信號reset?時(shí),判斷當(dāng)前總線是否空閑以及是否處于仲裁狀態(tài),同時(shí)初始化時(shí)鐘reset_Time從零開始計(jì)時(shí),當(dāng)時(shí)間流逝到達(dá)規(guī)定的重置最低時(shí)限r(nóng)eset_Period,將canState重新設(shè)置為0,總線可以繼續(xù)發(fā)送消息。

3 模型仿真驗(yàn)證與結(jié)果分析

本節(jié)對上述模型進(jìn)行仿真與形式化驗(yàn)證,并給出相應(yīng)的結(jié)果分析。CAN總線的一個(gè)明顯缺點(diǎn)是無法準(zhǔn)確地限制給定消息的最壞情況響應(yīng)時(shí)間,即消息排隊(duì)和消息到達(dá)目標(biāo)處理器之間的最長時(shí)間。本文并非驗(yàn)證總線的底層機(jī)制,而是給出需求約束條件在報(bào)文攻擊下的可滿足性分析。

圖5 總線應(yīng)用層行為模式時(shí)間自動(dòng)機(jī)

3.1 模型基本功能屬性驗(yàn)證

為驗(yàn)證CAN總線模型能否正確實(shí)現(xiàn)基本功能,使用CTL公式分別針對系統(tǒng)無死鎖性質(zhì)與狀態(tài)可達(dá)性進(jìn)行描述,屬性驗(yàn)證公式與含義說明如表2所示。模型在驗(yàn)證器中的驗(yàn)證結(jié)果如圖6所示,模型滿足表2所示的所有屬性。

表2 CAN總線屬性驗(yàn)證公式及其說明

圖6 Uppaal驗(yàn)證器對模型基本屬性的驗(yàn)證結(jié)果

3.2 CAN總線健壯性分析

本節(jié)分別使用正常報(bào)文與攻擊報(bào)文作為輸入對CAN總線的抗攻擊性能進(jìn)行分析,攻擊報(bào)文使用Seo等人[13]研究中提供的數(shù)據(jù)。對總線節(jié)點(diǎn)在報(bào)文攻擊存在下規(guī)定時(shí)間內(nèi)的發(fā)送成功概率進(jìn)行分析:

Sim-Property-1:Pr[<=15000]

(<>NodeApplication.SendSucc)。

為t_Done_Time取不同的值進(jìn)行仿真,Sim-Property-1屬性驗(yàn)證結(jié)果如圖7所示。當(dāng)取值為2 000或2 500個(gè)時(shí)間單位(1個(gè)時(shí)間單位代表1 μs)時(shí),成功發(fā)送的概率低于60%;當(dāng)取值為3 000～3 500個(gè)時(shí)間單位之間時(shí),發(fā)送成功的累積分布概率在75%以上。更高的取值不會(huì)帶來概率的明顯提升,故建議發(fā)送時(shí)間約束設(shè)置為3 000～3 500個(gè)時(shí)間單位,可滿足CAN總線高效發(fā)送數(shù)據(jù)的需求。

對總線節(jié)點(diǎn)在報(bào)文攻擊的情況下成功應(yīng)答的概率進(jìn)行統(tǒng)計(jì)分析。Sim-Property-2描述了0號從節(jié)點(diǎn)在99 999個(gè)時(shí)間單位內(nèi)到達(dá)RepSucc狀態(tài)的概率:

Sim-Property-2:Pr[<=99999]

(<> txNode(0).RepSucc)。

以此類推,驗(yàn)證其余3個(gè)節(jié)點(diǎn)到達(dá)成功應(yīng)答狀態(tài)的概率。當(dāng)應(yīng)答時(shí)限t_UppLim設(shè)置為2 000個(gè)時(shí)間單位時(shí),Uppaal SMC驗(yàn)證器的結(jié)果如圖8所示,通過進(jìn)行多次報(bào)文分組測試可得如表3所示的概率情況。

圖7 不同時(shí)限內(nèi)CAN總線成功發(fā)送數(shù)據(jù)的概率累積分布

圖8 Uppaal SMC對屬性公式的部分驗(yàn)證結(jié)果

表3 不同節(jié)點(diǎn)對常規(guī)報(bào)文與攻擊報(bào)文應(yīng)答成功的概率對比

由概率驗(yàn)證結(jié)果可知,當(dāng)嵌入式系統(tǒng)上存在攻擊時(shí),即CAN總線上通信內(nèi)容含有攻擊報(bào)文時(shí),特定需求時(shí)間約束內(nèi)成功應(yīng)答的概率均有所減小,優(yōu)先級最低的節(jié)點(diǎn)應(yīng)答正確率在[0.400 152,0.500 098]之間,正確率較低,說明在大量攻擊存在時(shí),應(yīng)答時(shí)間上限設(shè)置為2 000個(gè)時(shí)間單位并不合理。

Sim-Property-3描述了各個(gè)從節(jié)點(diǎn)應(yīng)答用時(shí)的時(shí)鐘變量隨時(shí)間變化的關(guān)系:

Sim-Property-3:simulate 1[<=21000]

{ txNode(0).rep_Time,txNode(1).rep_Time,

txNode(2).rep_Time,txNode(3).rep_Time}。

仿真結(jié)果如圖9所示,節(jié)點(diǎn)的應(yīng)答時(shí)間最高超過3 600個(gè)時(shí)間單位,故本文建議在考慮到攻擊存在的情況下,將應(yīng)答時(shí)限t_UppLim調(diào)整為3 500～4 000個(gè)時(shí)間單位,以保證低優(yōu)先級的節(jié)點(diǎn)也能正常應(yīng)答,提高CAN總線上的傳輸效率。如表3所示,響應(yīng)時(shí)間參數(shù)調(diào)整后,在相同攻擊下,最低優(yōu)先級節(jié)點(diǎn)3的應(yīng)答成功率提高了23.51%,4個(gè)節(jié)點(diǎn)的平均應(yīng)答正確概率由0.749 63提升至0.873 661,相比之下提升了12.4%,可滿足CAN總線常規(guī)通信需求。

圖9 報(bào)文攻擊下從節(jié)點(diǎn)應(yīng)答時(shí)間變化

4 結(jié)束語

本文針對航天嵌入式軟件需求,提出了一種CAN總線健壯性驗(yàn)證分析方案。該方案基于Uppaal SMC概率模型,將CAN總線協(xié)議數(shù)據(jù)鏈路層與應(yīng)用層結(jié)合進(jìn)行形式化建模,開展時(shí)序關(guān)鍵屬性驗(yàn)證;將攻擊報(bào)文引入CAN總線模型,評估CAN總線抗攻擊者入侵風(fēng)險(xiǎn)影響;依據(jù)仿真驗(yàn)證結(jié)果改進(jìn)軟件需求參數(shù)指標(biāo),提升總線在報(bào)文攻擊情況下的傳輸準(zhǔn)確率與應(yīng)答正確率,為嵌入式通信軟件開發(fā)與設(shè)計(jì)安全提供了理論參考。目前本文研究僅限于特定需求場景下的建模分析,后續(xù)將對CAN總線風(fēng)險(xiǎn)影響分析模型的普適性進(jìn)行進(jìn)一步優(yōu)化。