基于MAVLink 協(xié)議的無人機(jī)系統(tǒng)安全通信方案

張凌浩，王 勝，周 輝，陳一凡，桂盛霖*

（1. 國(guó)網(wǎng)四川省電力公司電力科學(xué)研究院，成都610000； 2. 國(guó)網(wǎng)四川省電力公司檢修公司，成都610041；3. 電子科技大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院，成都611731）

0 引言

隨著科學(xué)技術(shù)的發(fā)展，無人機(jī)（Unmanned Aerial Vehicle,UAV)已經(jīng)成為一項(xiàng)新興技術(shù)，在多個(gè)行業(yè)獲得了廣泛應(yīng)用，如智能城市、邊境監(jiān)視、自然災(zāi)害監(jiān)控［1］、實(shí)時(shí)物體跟蹤［2］和貨物運(yùn)輸［3-4］等。UAV［5］在飛行時(shí)可以被地面控制站（Ground Control Station，GCS）進(jìn)行遠(yuǎn)程控制，也可以通過預(yù)先編程的任務(wù)進(jìn)行自動(dòng)控制。當(dāng)受到遠(yuǎn)程控制時(shí)，UAV 和GCS 之間需通過通信協(xié)議進(jìn)行通信。微型飛行器鏈路（Micro Air Vehicle Link，MAVLink）協(xié)議［6］是一種靈活、輕量級(jí)的開源通信協(xié)議，被Ardupilot、PX4 等多個(gè)無人機(jī)系統(tǒng)作為無人機(jī)與地面站之間的通信協(xié)議，實(shí)現(xiàn)無人機(jī)和地面站之間的雙向數(shù)據(jù)交換。

但是，MAVLink協(xié)議沒有引入足夠的安全機(jī)制，且未使用任何加密算法，因此容易受到包括竊聽、消息偽造和中間人攻擊等多種惡意攻擊［7-8］。為了保證MAVLink協(xié)議的通信安全，研究者們提出了一些通信安全方案，如使用凱撒密碼［9］對(duì)無人機(jī)與地面站的之間的通信數(shù)據(jù)進(jìn)行加密，但是，已有文獻(xiàn)較多關(guān)注通信內(nèi)容加密，缺乏系統(tǒng)性安全增強(qiáng)機(jī)制，具有較大的局限性。因此，本文基于MAVLink 協(xié)議，提出了一種無人機(jī)系統(tǒng)安全通信方案，不僅解決了MAVLink 協(xié)議的安全性以防止竊聽攔截之類的攻擊，同時(shí)增加了無人機(jī)和地面站的身份認(rèn)證機(jī)制防止中間人的惡意攻擊。本文的方案模型在形式化驗(yàn)證工具UPPAAL 平臺(tái)上經(jīng)過形式化驗(yàn)證，證明它具有活性、可連接性及連接唯一性，并且在PX4 1.6.0 與地面站QgroundControl 3.5.0平臺(tái)上進(jìn)行了開發(fā)和實(shí)現(xiàn)。

1 相關(guān)工作

無人機(jī)的現(xiàn)有安全防護(hù)措施主要包括傳感器安全、軟件安全、通信安全三個(gè)方面［10］。

傳感器是無人機(jī)系統(tǒng)探測(cè)自身及周圍環(huán)境數(shù)據(jù)的重要組成部分。目前，針對(duì)無人機(jī)傳感器的攻擊形式主要是全球定位系統(tǒng)（Global Positioning System，GPS）欺騙。文獻(xiàn)［11-13］中通過使用一種GPS 信號(hào)自動(dòng)增益控制來檢測(cè)是否接收到GPS 欺騙信號(hào)；而文獻(xiàn)［14］中則通過判斷信號(hào)強(qiáng)度和噪聲值來檢測(cè)GPS 欺騙。針對(duì)飛控軟件是否受到了惡意代碼的入侵，文獻(xiàn)［15-16］中采用機(jī)器學(xué)習(xí)技術(shù)通過處理軟件的特征碼以及軟件行為的數(shù)據(jù)，依據(jù)該信息得出該軟件是否為惡意軟件的結(jié)論。在通信安全方面，無人機(jī)和地面站之間的通信存在中間人攻擊、竊聽、偽造等安全威脅，而現(xiàn)有文獻(xiàn)的工作大多集中在對(duì)通信內(nèi)容進(jìn)行加密，如文獻(xiàn)［17］中介紹了一種無人機(jī)與傳感器等智能實(shí)體通信的協(xié)議，使用了證書簽名機(jī)制對(duì)通信內(nèi)容進(jìn)行加密；文獻(xiàn)［18］中使用加密機(jī)制RC5 來保護(hù)MAVLink 通信協(xié)議；文獻(xiàn)［19］中對(duì)MAVLink 協(xié)議進(jìn)行了漏洞分析，使用了多種加密算法來保護(hù)MAVLink 身份協(xié)議的通信內(nèi)容。而對(duì)于無人機(jī)與地面站的認(rèn)證機(jī)制僅有少量論文進(jìn)行研究，如文獻(xiàn)［20］中使用DH（Diffie-Hellman）密鑰交換/協(xié)議對(duì)無人機(jī)與地面站進(jìn)行身份認(rèn)證，但是并未對(duì)其進(jìn)行形式化證明。本文對(duì)該方案使用UPPAAL 進(jìn)行形式化建模和驗(yàn)證，發(fā)現(xiàn)存在認(rèn)證漏洞的可達(dá)性路徑（見第4章）。

基于上述分析，目前缺乏對(duì)MAVLink 協(xié)議的系統(tǒng)性安全機(jī)制的研究，如文獻(xiàn)［17-18］中沒有對(duì)與無人機(jī)交互的實(shí)體作身份認(rèn)證；文獻(xiàn)［19］中僅提供協(xié)議的描述，沒有給出測(cè)試和實(shí)現(xiàn)的特定細(xì)節(jié)。因此，本文基于MAVLink 2.0 通信協(xié)議設(shè)計(jì)了無人機(jī)系統(tǒng)的一種安全通信方案，其中在建立連接階段取消了MAVLink 2.0 中無人機(jī)無安全保證的確認(rèn)連接操作，并新增了密鑰協(xié)商機(jī)制生成共享密鑰，雙方使用加密的MAVLink 2.0 消息包進(jìn)行通信并完成身份認(rèn)證。為了防止系統(tǒng)固件被惡意篡改，還對(duì)無人機(jī)系統(tǒng)固件進(jìn)行了引導(dǎo)時(shí)自校驗(yàn)。最后經(jīng)過形式化建模，證明了本文改進(jìn)后的無人機(jī)系統(tǒng)安全通信方案能夠保證無人機(jī)系統(tǒng)的活性、可連接性以及認(rèn)證唯一性。

2 基于DH算法的MAVLink協(xié)議

2.1 MAVLink協(xié)議

MAVLink是一種開源、輕量級(jí)且僅包含標(biāo)頭的協(xié)議，常用于 GCS 和 UAV 之間的雙向 通 信 。MAVLink 1.0 于 2009 年 初由Lorenz Meier 以寬通用公共許可證（Lesser General Public License，LGPL）首次發(fā)布［21］。MAVLink 2.0 協(xié)議［22］于 2017 年初發(fā)布，是當(dāng)前最新的版本，它與MAVLink 1.0 版本向后兼容，并在MAVLink 1.0版本的基礎(chǔ)上進(jìn)行了多項(xiàng)改進(jìn)。

圖1 給出了MAVLink 2.0 消息包的結(jié)構(gòu)，每個(gè)MAVLink 2.0 消息包都包含頭部信息、內(nèi)容信息和校驗(yàn)信息，具體字段包括：數(shù)據(jù)包開始標(biāo)記字段（packet Start Sign，STX）、有效負(fù)載長(zhǎng)度字段（payload LENgth，LEN）、不兼容標(biāo)志字段（INCompat FLAGS，INC FLAGS）、兼容標(biāo)志字段（CoMPat FLAGS，CMP FLAGS）、數(shù)據(jù)包序列號(hào)字段（packet SEQuence，SEQ）、系統(tǒng) ID 字段（SYStem ID，SYS ID）、組件 ID 字段（COMPonent ID，COMP ID）、消息ID 字段（MeSsaGe ID，MSG ID）、校驗(yàn)和字段（CHECKSUM）、簽名（SIGNATURE）和有效負(fù)載字段（PAYLOAD）。其中PAYLOAD 大小是可變的，其長(zhǎng)度取決于在通信期間發(fā)送或接收的參數(shù)，最大長(zhǎng)度為255 B。MAVLink 2.0 消息類型由消息包上的MSG ID 字段標(biāo)識(shí)，并且PAYLOAD 字段依據(jù)MSG ID 產(chǎn)生不同的內(nèi)容。其中，MSG ID字段為0X00 的消息包為心跳包（Heartbeat）。請(qǐng)求連接時(shí)，無人機(jī)會(huì)首先向地面站發(fā)送心跳包請(qǐng)求連接，若地面站收到該請(qǐng)求，則發(fā)送對(duì)應(yīng)的控制命令確認(rèn)連接。此后，無人機(jī)定期（通常每秒）向地面站發(fā)送心跳包，以提供其狀態(tài)的反饋（指示無人機(jī)處于活動(dòng)狀態(tài)且仍處于連接狀態(tài)）。圖2 給出了MAVLink 2.0中無人機(jī)和地面站的連接過程。

圖1 MAVLink 2.0的消息包結(jié)構(gòu)Fig. 1 Message package structure of MAVLink 2.0

圖2 MAVLink 2.0中無人機(jī)和地面站的連接過程Fig.2 Connection process between UAV and GCS in MAVLink 2.0

事實(shí)上，由于MAVLink 2.0 協(xié)議并沒有提供足夠的安全機(jī)制來保護(hù)通信數(shù)據(jù)，也沒有身份認(rèn)證機(jī)制，因此只要使用匹配的無線數(shù)傳硬件，任何第三方地面站都可以與無人機(jī)通信并將命令注入到現(xiàn)有會(huì)話中，無人機(jī)系統(tǒng)很容易被黑客入侵和控制，存在較大的安全風(fēng)險(xiǎn)。

2.2 基于MAVLink的無人機(jī)系統(tǒng)安全通信方案

針對(duì)基本的MAVLink 2.0 中的安全問題，本文方案至少要達(dá)到以下三個(gè)目標(biāo)：

1）無人機(jī)以密文形式傳輸消息，防止惡意竊聽及篡改消息；

2）無人機(jī)和地面站進(jìn)行身份認(rèn)證，防止惡意中間人攻擊；

3）對(duì)協(xié)議的通信過程需建立形式化模型，證明其安全性質(zhì)。

在基本MAVLink 2.0協(xié)議的基礎(chǔ)上引入了高級(jí)加密標(biāo)準(zhǔn)（Advanced Encryption Standard，AES）算法和DH 算法，其中：AES 加密算法保證了無人機(jī)以密文形式傳輸消息，防止了惡意竊聽和篡改消息；DH算法則實(shí)現(xiàn)了無人機(jī)和地面站的密鑰協(xié)商和身份認(rèn)證。

本文設(shè)計(jì)的無人機(jī)系統(tǒng)安全通信方案可分為四個(gè)階段：

1）無人機(jī)請(qǐng)求連接；

2）無人機(jī)和地面站密鑰協(xié)商與身份認(rèn)證；

3）無人機(jī)與地面站加密通信；

4）無人機(jī)與地面站斷開連接。

圖3 給出了無人機(jī)和地面站的上述4 個(gè)交互階段。定義1 給出了描述無人機(jī)或地面站在交互過程中狀態(tài)變化的六元組的定義。

圖3 無人機(jī)與地面站交互過程Fig. 3 Interaction process between UAV and GCS

定義1 通信實(shí)體狀態(tài)可由一個(gè)六元組L，L0，A，C，I，E表示。其中：L表示有窮位置集；L0表示初始位置，L0∈L；A表示有窮事件集，其中a？(a∈A)表示接收了一個(gè)來自其他實(shí)體的事件，a！(a∈A)表示向其他實(shí)體發(fā)出了一個(gè)事件；C表示時(shí)鐘變量集；I：L→B(C)表示一個(gè)映射，用于為L(zhǎng)中的每個(gè)元素指定一個(gè)時(shí)間約束，其中，時(shí)鐘約束集B(C) 是形如{c0～n或c1-c2～n，c0，c1，c2 ∈C，n∈N，～ ∈ { ＜ ，＜= ，= ，＞= ，＞ }的不等式集合；E?L×A×B(C) × 2C×L，表示邊集，邊(l，a，b，R，l′) ∈E表示滿足事件a和時(shí)鐘約束b時(shí)，從位置l遷移到位置l′，同時(shí)時(shí)鐘集合R中的時(shí)鐘變量被重置。

2.2.1 無人機(jī)請(qǐng)求連接階段

在連接請(qǐng)求階段，無人機(jī)持續(xù)交替廣播MAVLink 2.0 心跳包與公鑰包Xuav，請(qǐng)求與地面站連接，其中心跳包格式與MAVLink 2.0中定義的一致，公鑰包的MSG ID 為3，并將公鑰Xuav填充至其有效負(fù)載字段。圖4 給出了無人機(jī)與地面站在請(qǐng) 求 連 接 階 段 的 六 元 組Luav，L0，A，Cuav，Iuav，Euav和Lgcs，L0，A，Cgcs，Igcs，Egcs描述，其中兩個(gè)六元組共享同一事件集A。

在無人機(jī)端，無人機(jī)初始化后進(jìn)入idle 空閑位置（idle ∈Luav）并交替發(fā)送心跳包與公鑰包Xuav（將其記為原子事件“request！”(request∈A)），然后進(jìn)入 wait_public_key 位置（wait_public_key∈Luav）等待接收地面站的公鑰包Xgcs，同時(shí)將時(shí)鐘變量c1 清零。在該位置上，最多只能停留5 個(gè)時(shí)鐘單位（記為不變式“c1 ＜= 5”（c1 ∈Cuav））。若未在5 個(gè)時(shí)鐘單位內(nèi)收到地面站的公鑰包Xgcs則返回idle位置。在地面站端，若收到無人機(jī)發(fā)送的心跳包或公鑰包Xuav，則進(jìn)入parse_request位置（parse_request ∈Lgcs）。

圖4 無人機(jī)和地面站在請(qǐng)求連接階段的狀態(tài)變化關(guān)系Fig.4 State transition relationship between UAV and GCS in stage of requesting connection

2.2.2 無人機(jī)和地面站密鑰協(xié)商與身份認(rèn)證階段

本文設(shè)計(jì)的方案和基本的MAVLink 2.0 協(xié)議相比，還增加了密鑰協(xié)商與身份認(rèn)證過程。無人機(jī)發(fā)起請(qǐng)求連接后，若在5個(gè)時(shí)鐘單位內(nèi)收到地面站發(fā)送的公鑰Xgcs，則通過式（1）、（2）計(jì)算共享密鑰K。

式中：a、q為無人機(jī)和地面站預(yù)先協(xié)商的共同參數(shù)。在地面站端，收到無人機(jī)發(fā)送的公鑰Xuav后通過式（3）、（4）計(jì)算共享密鑰K。

通過密鑰協(xié)商，無人機(jī)和地面站生成了安全的共享密鑰K。在此后的一輪通信中，無人機(jī)和地面站使用AES 算法對(duì)MAVLink 2.0消息包中的PAYLOAD字段進(jìn)行加密。

若無人機(jī)收到地面站發(fā)送的加密MAVLink 2.0消息包對(duì)其PAYLOAD 字段解析錯(cuò)誤，則地面站未通過身份認(rèn)證，無人機(jī)與其斷開連接；若對(duì)加密的MAVLink 2.0消息包解析正確，則雙方身份認(rèn)證成功，可繼續(xù)通信。圖5 給出了無人機(jī)與地面站在密鑰協(xié)商與身份認(rèn)證階段的六元組描述。

圖5 無人機(jī)和地面站在密鑰協(xié)商和身份認(rèn)證階段的狀態(tài)變化關(guān)系Fig.5 State transition relationship between UAV and GCS during stage of key negotiation and identity authentication

本階段開始時(shí)，無人機(jī)處于wait_public_key 位置，若在5個(gè)時(shí)鐘單位內(nèi)收到地面站發(fā)送的公鑰包Xgcs（記為事件“Xgcs？”(Xgcs∈ A)）后進(jìn)入位置 success(success ∈ Luav)表示成功收到公鑰包Xgcs。該位置中，若收到地面站使用共享密鑰K加密的任何 MAVLink 2.0 消息包（記為事件“mav？”（mav ∈A））則表示身份認(rèn)證成功繼續(xù)保持通信，否則到達(dá)5個(gè)時(shí)鐘單位后斷開連接進(jìn)入idle 位置重新發(fā)起新的會(huì)話（記為事件“off！”（off ∈ A））。在地面站端，地面站在本階段開始前已經(jīng)處于parse_request 位置，向無人機(jī)發(fā)送公鑰包Xgcs（記為事件“Xgcs！”）進(jìn)入success位置表示密鑰協(xié)商成功。該位置中，地面站使用共享密鑰K 加密任何要發(fā)送的MAVLink 2.0消息包（記為事件“mav！”）。

2.2.3 無人機(jī)與地面站加密通信

無人機(jī)與地面站使用共享密鑰K對(duì)MAVLink消息包加密通信。若收到惡意攻擊者發(fā)來偽造的MAVlink 2.0 消息包導(dǎo)致解密失敗，則無人機(jī)斷開連接。在斷開連接之后，若無人機(jī)和地面站需要建立新的連接，則動(dòng)態(tài)更新Xuav和Xgcs重新生成新的共享密鑰K，進(jìn)一步保證了密鑰的安全性。此外，為了保持連接狀態(tài)，無人機(jī)定期向地面站發(fā)送心跳包，對(duì)其中的PAYLOAD字段進(jìn)行加密。

本文所提出的無人機(jī)系統(tǒng)安全通信方案繼續(xù)保留了MAVLink 2.0的以下安全機(jī)制：

1）時(shí)間戳機(jī)制：自2015 年1 月1 日格林威治標(biāo)準(zhǔn)時(shí)間以來，時(shí)間戳以10 μs 為單位。對(duì)于特定連接上的每個(gè)消息，時(shí)間戳必須單調(diào)增加。注意，這意味著如果數(shù)據(jù)包速率平均每秒超過100 000個(gè)數(shù)據(jù)包，則時(shí)間戳可能會(huì)超過實(shí)際時(shí)間。

2）重傳機(jī)制：MAVLink 2.0 協(xié)議在發(fā)送端啟動(dòng)一個(gè)定時(shí)器，如果在特定的時(shí)間內(nèi)沒有收到響應(yīng)，則請(qǐng)求的消息會(huì)被重新發(fā)送一次。該重傳過程會(huì)重復(fù)數(shù)次，如果在最后一次的重傳超時(shí)后仍然沒有收到響應(yīng)，則認(rèn)定該消息發(fā)送失敗。

3）丟包機(jī)制：在發(fā)送端，MAVLink 2.0 消息包中的 SEQ 字段在每次發(fā)送消息包后都會(huì)遞增，以此檢測(cè)是否丟包。

2.2.4 無人機(jī)和地面站斷開連接

無人機(jī)與地面站滿足以下條件之一時(shí)斷開連接：

1）在無人機(jī)和地面站進(jìn)行通信過程中，若對(duì)地面站發(fā)送的加密MAVLink 消息包解析錯(cuò)誤，則主動(dòng)斷開連接并進(jìn)入idle位置（記為事件“off！”）；

2）無人機(jī)或地面站主動(dòng)發(fā)送MSG ID 為5 的消息包，則斷開連接。

3 無人機(jī)自校驗(yàn)

為保證無人機(jī)系統(tǒng)不被篡改，本文還設(shè)計(jì)了引導(dǎo)時(shí)的自校驗(yàn)機(jī)制，并在PX4 1.6.0 系統(tǒng)進(jìn)行開發(fā)，實(shí)現(xiàn)PX4 系統(tǒng)在上電初始化后進(jìn)行Hash 校驗(yàn)，若校驗(yàn)成功，系統(tǒng)正常運(yùn)行；否則，系統(tǒng)停止加載并退出。該機(jī)制的實(shí)現(xiàn)過程如下：

1）原 px4src_1.6.0FirmwareToolspx_uploader.py 文件中的def __program（self，label，fw）函數(shù)中定義了變量size 記錄固件的大小，因此本文在此函數(shù)中新增根據(jù)PX4 系統(tǒng)固件的起始地址（BootLoader_v2 在配置文件BootLoader_v2/hw_config.h 中定義起始地址為0x08004004）計(jì)算終止地址為0x08004004+size-4。

2）在 Bootloader_v2 根目錄中新增 md5. c 與 md5. h 文件，實(shí)現(xiàn)了MD5（Message-Digest Algorithm 5）算法［23］用于計(jì)算PX4系統(tǒng)固件Hash 值。本文使用PX4 系統(tǒng)固件作為MD5 算法的輸入?yún)?shù)并計(jì)算出Hash 值，存儲(chǔ)在Bootloader_v2l.c 文件下hash_data［n］數(shù)組中。

3）原Bootloader_v2l.c文件中包含了初始化硬件的各類函數(shù)，本文在該文件中新增了函數(shù)GetFlashMD5（unsigned char decrypt［］，int n），用于在 PX4 上電初始化完成后調(diào)用md5. c 文件中實(shí)現(xiàn)的MD5 算法完成對(duì)PX4 系統(tǒng)固件的Hash值計(jì)算并與預(yù)先存儲(chǔ)的Hash 值hash_data［n］進(jìn)行比較，若檢驗(yàn)正確，系統(tǒng)正常運(yùn)行；否則，系統(tǒng)停止加載并退出。

4 形式化證明與測(cè)試

4.1 形式化證明

本文使用由瑞典Uppsala 大學(xué)和丹麥Aalborg 大學(xué)聯(lián)合開發(fā)的形式化工具UPPAAL 對(duì)無人機(jī)系統(tǒng)安全通信方案進(jìn)行了形式化證明。該工具由模型編輯器、模擬器和驗(yàn)證器三部分組成。其中：系統(tǒng)編輯器用于對(duì)待驗(yàn)證實(shí)體進(jìn)行建模；模擬器用于檢查所建立的模型是否存在錯(cuò)誤；驗(yàn)證器用于驗(yàn)證模型是否滿足計(jì)算樹邏輯（Computation Tree Logic，CTL）公式描述的性質(zhì)。另外，UPPAAL 使用位置集（L）、初始位置（L0）、事件集（A）、時(shí)鐘變量集（C）、不變式（I）、邊集（E）六元組來描述通信實(shí)體狀態(tài)，并為屬性描述提供了簡(jiǎn)化版的計(jì)算樹邏輯（CTL）公式，它由路徑公式和狀態(tài)公式兩部分組成，前者量化模型的路徑或軌跡，而后者則描述單獨(dú)的狀態(tài)。此外，UPPAAL還提供了“deadlock”關(guān)鍵詞用來描述死鎖狀態(tài)。

為驗(yàn)證文獻(xiàn)［19］中所提出的安全通信協(xié)議存在認(rèn)證漏洞，本文基于UPPAAL 工具對(duì)文獻(xiàn)［19］中的技術(shù)方案在存在惡意中間人攻擊的場(chǎng)景中進(jìn)行了形式化建模，如圖6 所示，其中：圖（a）給出了無人機(jī)（UAV）的狀態(tài)變化模型，圖（b）和（c）分別給出了惡意中間人地面站（Malice Ground Control Station，GCS_M）和正常地面站（GCS）的狀態(tài)變化模型。注意，圖6（b）的惡意中間人地面站偽裝成一個(gè)正常地面站，因此具有與正常地面站相同的狀態(tài)變化模型。但是，在實(shí)際攻擊場(chǎng)景中，惡意攻擊地面站可能采用不同精心設(shè)計(jì)的攻擊策略。

攻擊場(chǎng)景：文獻(xiàn)［19］中身份認(rèn)證過程中存在某一時(shí)刻，GCS 與UAV 已經(jīng)建立連接并等待身份認(rèn)證時(shí)，GCS_M 搶先發(fā)送公鑰Xgcs_m與UAV 完成身份認(rèn)證并實(shí)現(xiàn)控制UAV，導(dǎo)致與UAV 已經(jīng)建立連接關(guān)系的GCS 失去對(duì)UAV 的控制權(quán)。該過程可由式（5）表示：

對(duì)圖6 和式（5）進(jìn)行形式化驗(yàn)證，結(jié)果顯示該性質(zhì)成立，因此存在認(rèn)證漏洞的可達(dá)路徑。而本文設(shè)計(jì)的方案在UPPAAL中進(jìn)行形式化建模后如圖7所示，其中：圖（a）給出了無人機(jī)（UAV）的狀態(tài)變化模型，圖（b）和（c）給出了惡意中間人地面站（GC1S_M）和正常地面站（GCS）的狀態(tài)變化模型。

本文使用了三個(gè)關(guān)鍵安全屬性，使用計(jì)算樹邏輯（CTL）公式表示如下：

1）活性。

在本文方案中，若UAV 和GCS 在某個(gè)通信時(shí)刻進(jìn)入了死鎖狀態(tài)，則表示整個(gè)協(xié)議是無法正常運(yùn)行的。因此，系統(tǒng)的活性是基本性質(zhì)之一。在UPPAAL 中，式（6）描述了系統(tǒng)的活性。經(jīng)驗(yàn)證，本文方案滿足該性質(zhì)。

2）可連接性。

UAV 和GCS 身份認(rèn)證過程中，雙方必須能夠在一定時(shí)間周期內(nèi)成功連接。式（7）描述了可連接性。經(jīng)驗(yàn)證，本文方案滿足該性質(zhì)。

3）連接唯一性。

圖6 文獻(xiàn)［19］的狀態(tài)變化模型Fig.6 State transition model of literature［19］

在UAV 和GCS 連接到身份認(rèn)證成功期間，若存在某一時(shí)刻GCS_M 同時(shí)也能夠與UAV 連接或進(jìn)行身份認(rèn)證，式（8）給出了連接唯一性的表示。

式（8）在UPPAAL 中驗(yàn)證不滿足，因此本文的無人機(jī)系統(tǒng)安全通信方案不存在文獻(xiàn)［20］中認(rèn)證漏洞的可達(dá)性，防止了惡意中間人的攻擊。表1 給出了本文無人機(jī)系統(tǒng)安全通信方案的安全機(jī)制。

圖7 本文方案的狀態(tài)變化模型Fig.7 State transition model of the proposed scheme

4.2 抓包測(cè)試

本文所使用的開發(fā)與測(cè)試平臺(tái)為無人機(jī)PX4 1.6.0 與地面站QgroundControl 3.5.0，其中，QGroundControl 地面站是由Lorenz Meier開發(fā)并用C++編寫的開源地面控制站（GCS）軟件應(yīng)用程序。本文按照2.2 節(jié)中定義的4 個(gè)階段修改了MAVLink 2.0 的相關(guān)源代碼，并按第3 章的實(shí)現(xiàn)過程在BootLoader_v2中增加了無人機(jī)系統(tǒng)固件進(jìn)行引導(dǎo)時(shí)自校驗(yàn)功能，最后重新編譯了QgroundControl 3.5.0、PX4 1.6.0 以及BootLoader_v2 的源代碼，形成了qgroundcontrol-start. sh、px4fmuv2_bl.bin與px4fmuv2.px4可執(zhí)行文件。

本節(jié)使用Bus Hound 抓包工具在Ubuntu16.04 對(duì)PX4 1.6.0 和QgroundControl 3.5.0 通信時(shí)進(jìn)行了抓包分析，以說明開發(fā)的有效性。表2、3 給出了PX4 1.6.0 與QgroundControl 3.5.0 在各個(gè)階段抓取的部分MAVLink 消息包內(nèi)容，說明本文基于MAVLink 的無人機(jī)系統(tǒng)安全通信方案具有防篡改、防竊聽的安全性質(zhì)

表 2、3 分別給出了 PX4 1.6.0 與 QgroundControl 3.5.0 在MAVLink 協(xié)議改進(jìn)前后的消息包內(nèi)容。在加密通信階段，控制命令原始消息包PAYLOAD 為0f 38 97 c6 e3 d1 59 7f 75 b8 89 48 0b 8a 95 71，通過加密后得到的有效負(fù)載為6a 49 67 03 7f 73 a6 10 3a 91 8a 17 a5 89 e6 92，有效防止了惡意中間人的竊聽，并且和MAVLink 中的校驗(yàn)字段結(jié)合可有效防止惡意中間人的篡改。

表4 測(cè)試了改進(jìn)前后加密通信階段PX4 1.6.0 與QgroundControl 3.5.0 在相同時(shí)間內(nèi)傳輸消息包的數(shù)量，說明了改進(jìn)后無人機(jī)與地面站傳輸?shù)南猩倭繙p少，此方案 對(duì)無人機(jī)性能開銷影響較小。

表1 無人機(jī)系統(tǒng)安全通信方案的安全機(jī)制Tab. 1 Security mechanisms of UAV system secure communication scheme

表2 改進(jìn)前各階段MAVLink消息包內(nèi)容Tab. 2 Contents of original MAVLink message packages in different stages

表3 改進(jìn)后各階段MAVLink消息包內(nèi)容Tab. 3 Contents of improved MAVLink message packages in different stages

表4 加密通信階段消息包傳輸數(shù)量Tab. 4 Number of transmitted message packets in encrypted communication stage

5 結(jié)語(yǔ)

本文針對(duì)MAVLink 2.0 協(xié)議存在的安全漏洞，設(shè)計(jì)并實(shí)現(xiàn)了一種基于MAVLink 協(xié)議的無人機(jī)系統(tǒng)安全通信方案。無人機(jī)首先廣播連接請(qǐng)求，然后使用DH 算法與地面站進(jìn)行密鑰協(xié)商及身份認(rèn)證，并使用AES 算法對(duì)MAVLink 消息包進(jìn)行加密傳輸。此外，無人機(jī)與地面站斷開連接后會(huì)動(dòng)態(tài)更新公鑰。經(jīng)過形式化證明和抓包測(cè)試，結(jié)果表明本文提出的方案能夠防止無人機(jī)與地面站通信過程中潛在的惡意竊聽、消息篡改等攻擊，并且與文獻(xiàn)［20］中的技術(shù)方案相比，本文方案避免了MAVLink 協(xié)議存在中間人攻擊等安全漏洞，未來還會(huì)針對(duì)本文方案作進(jìn)一步完善。