面向安全屬性的機器人運行時驗證

楚 敏 邵振洲 王 瑞 李曉娟 張 芮

(首都師范大學信息工程學院 北京 100048)(輕型工業(yè)機器人與安全驗證北京市重點實驗室(首都師范大學) 北京 100048)

0 引 言

ROS是一個用于機器人軟件開發(fā)的開源操作系統(tǒng)[1]。ROS為機器人應(yīng)用提供了統(tǒng)一的接口標準，容易與其他的機器人軟件平臺集成。ROS中執(zhí)行某一任務(wù)的進程稱為節(jié)點，機器人控制系統(tǒng)通常由多個節(jié)點組成。節(jié)點之間傳遞消息的主要方式是主題。主題通信方式通過發(fā)布者發(fā)布主題，訂閱者訂閱主題來進行。但是，在ROS的通信過程中，存在一些安全隱患。例如，節(jié)點的活動不受限制，任何節(jié)點都可以進行注冊和主題發(fā)布。攻擊者可以很容易地偽造節(jié)點來發(fā)布假消息，并竊聽重要主題的消息。另一方面，通信數(shù)據(jù)缺乏實時監(jiān)控，異常消息無法被捕獲。因此，需要建立合理的安全監(jiān)控機制保護節(jié)點通信過程的安全。這對于提高機器人系統(tǒng)的安全性和可靠性具有重要意義。

運行時驗證[2]是一種輕量級的驗證方法，采用形式化的方式對系統(tǒng)行為規(guī)范進行描述。它實時監(jiān)控系統(tǒng)程序的運行軌跡，判斷系統(tǒng)行為是否違反安全規(guī)范。該方法與模型檢測[3]和定理證明方法[4]相比，復(fù)雜度更低。與傳統(tǒng)的測試方法相比，運行時驗證在對屬性的描述以及對程序的監(jiān)控方面具有靈活性和擴展性。運行時驗證已經(jīng)應(yīng)用在ROS系統(tǒng)安全性保障中，Huang[5]提出了一個ROSRV框架，該框架可以監(jiān)控消息數(shù)據(jù)，并可選地修改消息內(nèi)容，但是并未對程序進行邏輯驗證。Balsa-Comerón等[6]認為ROS中的主要安全問題是明文通信，提出對通信數(shù)據(jù)使用對稱加密算法。但是，密鑰的管理和泄露會帶來隱患。其他學者針對ROS通信安全提出了其他策略，如White等[7]通過TLS(傳輸層安全加密協(xié)議)對兩個通信應(yīng)用程序之間的隱私和數(shù)據(jù)完整性進行了保護，Breiling等[8]提出建立一個安全的傳輸信道，使ROS節(jié)點能夠更加安全的通信。

本文基于運行時驗證技術(shù)，針對ROS操作系統(tǒng)在主題通信和節(jié)點活動方面存在的安全問題，提出了一個ROS-Monitor監(jiān)控框架。該框架支持時序邏輯描述系統(tǒng)安全屬性，根據(jù)自定義場景生成監(jiān)控器來監(jiān)控系統(tǒng)行為。若系統(tǒng)行為違背安全屬性，則打印相關(guān)告警信息。

1 背景知識

1.1 ROS[1,9]的通信方式

主題通信是ROS節(jié)點進行消息通信的主要方式，圖1展示了ROS主題通信的機制與過程[10]。它通過一系列XML/RPC(一種用于遠程過程調(diào)用協(xié)議)請求來啟動，具體步驟為：1) 發(fā)布者通過RPC請求向節(jié)點管理器注冊發(fā)布者信息，包括主題名topic1和RPC地址addr1，并將這些信息存儲到注冊列表中。2) 訂閱者向節(jié)點管理器訂閱主題topic1。3) 節(jié)點管理器根據(jù)訂閱者所需的主題topic1，在注冊列表中進行查找。若匹配成功，節(jié)點管理器向訂閱者傳遞發(fā)布者的RPC地址addr1。4) 訂閱者聯(lián)系發(fā)布者獲取主題連接請求。5) 在收到訂閱者的連接請求后，發(fā)布者繼續(xù)通過RPC請求向訂閱者確認連接信息，包括發(fā)布主題的TCP地址addr2。6) 訂閱者接收到確認消息后，通過TCP請求連接到發(fā)布者地址addr2。7) 二者成功建立TCP連接，訂閱者開始接收發(fā)布者發(fā)出的消息數(shù)據(jù)。

圖1 ROS通信過程

1.2 JavaMOP[11]

運行時驗證系統(tǒng)的結(jié)構(gòu)[12-13]如圖2所示，它由運行的程序和監(jiān)控器組成。監(jiān)控器通過分析程序的多個執(zhí)行路徑，將它們轉(zhuǎn)換為相應(yīng)事件，并結(jié)合給定的屬性，驗證系統(tǒng)行為是否滿足屬性，對運行結(jié)果作出判定。

圖2 運行時驗證結(jié)構(gòu)

運行時驗證的目的是實時監(jiān)控系統(tǒng)行為,驗證系統(tǒng)的正確性[2]。通常使用面向監(jiān)控的編程(Monitoring-oriented Programming，MOP)[14]技術(shù)，這是一種擴展了運行時驗證技術(shù)的輕量級形式化方法。MOP將屬性編織到原始系統(tǒng)中，并根據(jù)指定的屬性自動生成監(jiān)控器。監(jiān)控器監(jiān)視程序在運行期間的行為，當違反規(guī)范時將觸發(fā)用戶定義的操作。JavaMOP[10，15-16]是一個針對Java的監(jiān)控編程開發(fā)工具，具有可插拔性和靈活性。JavaMOP規(guī)范主要包括變量(var)、事件(event)、屬性(property)和處理程序(handler)。

1) 變量。變量指的是待監(jiān)控的程序變量。

2) 事件。事件是目標程序執(zhí)行期間發(fā)生的操作。它對應(yīng)于監(jiān)控程序中被監(jiān)控變量的更新，或者被監(jiān)控方法的調(diào)用。事件的聲明遵循AspectJ語義，事件被編織到Java程序中,被用來檢查是否符合屬性規(guī)約。

3) 屬性。屬性包括邏輯類型和邏輯語義，JavaMOP插件支持多種邏輯類型，如FSM(有限狀態(tài)機)、LTL(線性速度邏輯)、ERE(擴展正則表達式)、CFG(上下文無關(guān)文法)等。系統(tǒng)安全屬性可以用時態(tài)邏輯表示，本文主要以LTL邏輯[17-18]語句進行介紹。LTL語法由原子命題和運算符組成，運算符包括[]，[*]，<>，<*>，o，(*)，！，not，U，S，And，Xor，Or，=>(蘊含)[19]。T=t1,t2，…，ti,…，tn是一組原子命題，LTL語法及時態(tài)運算符解釋如下：

· []μ:μ在所有的時間內(nèi)都是成立的。

· [*]μ:μ在過去的時間內(nèi)都是成立的。

· (*)μ:μ在之前的時間是成立的。

· <>μ:μ在將來的某個時間點成立。

· <*>μ:μ在過去的某個時間點成立

· oμ:μ在下一個時間點成立。

· μSv：自從μ成立的時間點起，v在過去的某個時刻已經(jīng)成立了。

· μUv：v在未來的某個時間點成立，μ在v成立之前已經(jīng)成立了。

4) 處理程序：處理程序由任意的Java代碼組成，用戶可以自定義操作，該操作可以是記錄異?；蛐畔⒏娜魏未a。以@fail、@violation或@validation開頭,分別代表自動機的不確定、違背和驗證三種狀態(tài)。

2 ROS-Monitor運行時驗證框架

ROS-Monitor是一個針對機器人操作系統(tǒng)的運行時驗證框架。如圖3所示，我們設(shè)計了一個能夠監(jiān)控所有節(jié)點活動和節(jié)點消息的監(jiān)控中心節(jié)點，并將所有的待監(jiān)控信息存放到事件消息中樞。同時設(shè)計了一個代碼生成器，可以根據(jù)自定義場景描述自動生成特定的監(jiān)控器。最后通過運行監(jiān)控器，驗證系統(tǒng)的安全屬性，若系統(tǒng)行為違反安全屬性邏輯，則發(fā)出違背警告。

圖3 ROS-Monitor框架

2.1 監(jiān)控中心節(jié)點

ROS主題通信機制詳見1.1節(jié)，節(jié)點管理器默認啟動在11311端口，系統(tǒng)各節(jié)點連接到該端口進行主題發(fā)布等相關(guān)操作，節(jié)點管理器記錄各節(jié)點發(fā)布和訂閱的信息。為了獲取節(jié)點的所有信息，我們根據(jù)ROS的XML/RPC的通信協(xié)議，設(shè)計了一個支持節(jié)點注冊、主題發(fā)布訂閱等功能的監(jiān)控中心節(jié)點，可將其理解為節(jié)點管理器的代理。本框架將節(jié)點管理器啟動在11111端口，監(jiān)控中心節(jié)點啟動在11311端口。監(jiān)控中心節(jié)點一方面與節(jié)點管理器進行通信，另一方面與系統(tǒng)各功能節(jié)點進行通信，因此可以獲取ROS系統(tǒng)中所有待監(jiān)控的信息。

監(jiān)控中心節(jié)點需要監(jiān)控節(jié)點活動和節(jié)點消息兩種事件類型，并把所有的數(shù)據(jù)存放到事件消息中樞。其中節(jié)點活動類型是指在ROS系統(tǒng)中所有節(jié)點的活動數(shù)據(jù)，包括節(jié)點的啟動、發(fā)布主題、訂閱主題等事件。節(jié)點消息類型是指系統(tǒng)中各個節(jié)點之間傳遞的主題消息。

2.2 事件消息中樞

ROS程序主要由C++編寫，而JavaMOP是監(jiān)控Java程序的一種運行時驗證技術(shù)。為了能夠更好地利用JavaMOP技術(shù)，本系統(tǒng)設(shè)計了一個用于信息傳輸?shù)闹虚g件——事件消息中樞，它包括C++服務(wù)端和Java客戶端兩個部分?？蛻舳撕头?wù)端采用請求和應(yīng)答的方式進行通信，服務(wù)端將待監(jiān)控的信息存放到一個緩沖消息隊列，客戶端主動發(fā)起請求獲取服務(wù)端隊列中的數(shù)據(jù)。為了方便數(shù)據(jù)傳輸和解析，我們使用json字符串的方法將數(shù)據(jù)轉(zhuǎn)換成字節(jié)流。json是一種輕量級的數(shù)據(jù)交換格式，方法簡單靈活，又具有表達多層次復(fù)雜內(nèi)容的能力。

針對節(jié)點消息類型，主題消息的內(nèi)容是一個結(jié)構(gòu)體數(shù)據(jù)。例如控制小車運動的“/cmd_vel”消息對應(yīng)的結(jié)構(gòu)數(shù)據(jù)是“geometry_msgs/Twist”，該結(jié)構(gòu)體“Twist.msg”包含3維浮點數(shù):“Vector3 linear(x,y,z)”和“Vector3 angular(x,y,z)”。其中線速度表示為“msg.linear.x”，角速度表示為“msg.angular.z”。為了方便使用，將其轉(zhuǎn)化成json字符串，如一個具體的消息數(shù)據(jù)為“[1,0,0][0,0,2]”則轉(zhuǎn)化后的json字符串為:“message”:{“cmd_vel”:{“x”:1,”y”:0,”z”:0},”angular”:{“x”:0,”y”:0,”z”:2}}}

針對節(jié)點活動類型，包括節(jié)點注冊與注銷、主題發(fā)布與訂閱、消息發(fā)送與接收，具體字段和含義如表1所示。該類型數(shù)據(jù)同樣通過json字符串的方法進行傳輸，如下所示：

表1 節(jié)點活動類型

節(jié)點注冊：

{“node_event”:{“node”:“car”,“type”:“register”}}

發(fā)布主題：

{“node_event”:{“node”:“car”,“type”:“publish”,“topic”:“cmd_vel”}}

訂閱主題：

{“node_event”:{“node:car”,“type”:“subscribe”,“topic”:“cmd_vel”}}

2.3 自定義場景描述

一個正在運行的ROS系統(tǒng)會產(chǎn)生許多節(jié)點活動和節(jié)點消息數(shù)據(jù)，但是并非所有數(shù)據(jù)都需要監(jiān)控，僅需要關(guān)注與系統(tǒng)安全相關(guān)的部分。ROS中的待監(jiān)控數(shù)據(jù)本身具有結(jié)構(gòu)化，我們通過一種形式化描述的方法更加方便地表達要監(jiān)控的數(shù)據(jù)。因此，本系統(tǒng)設(shè)計了一個代碼生成工具，可以根據(jù)自定義場景描述文件自動生成特定的監(jiān)控器，包括Java代碼和Mop代碼。

表2是自定義場景描述字段和格式內(nèi)容說明。“Source”字段指定監(jiān)控內(nèi)容的來源，它包括節(jié)點活動或節(jié)點消息類型的數(shù)據(jù)，格式為“主題：主題名，或者節(jié)點：節(jié)點名”?！癡ar”表示要監(jiān)視消息中的變量，格式為“變量內(nèi)容：消息結(jié)構(gòu)體值”?！癊vent”字段是節(jié)點活動事件或節(jié)點消息變量監(jiān)控事件，格式為觸發(fā)函數(shù)的事件條件語句，它將與“Property”字段中的邏輯語句組合在一起形成屬性邏輯語義?！癙roperty”字段是一個屬性表達式，格式為“邏輯類型：邏輯語義”?！癡iolation”為違背字段，內(nèi)容為違背時的錯誤執(zhí)行代碼段，如果該屬性被違反，將根據(jù)“Violation”字段后面的代碼內(nèi)容進行打印警告。

表2 自定義場景描述說明

2.4 監(jiān)控代碼生成機制

監(jiān)控器的代碼生成機制如圖4所示。代碼生成器能依次解析自定義場景描述的“Source”、“Var”、“Event”和“Property”字段內(nèi)容，計算出這幾個字段的內(nèi)部依賴關(guān)系，生成若干個代碼段。并將生成的代碼填充到預(yù)先準備好的代碼模板中，最終生成完整的Java代碼和Mop代碼文件。其中生成的Java代碼包含一個TCP客戶端，該客戶端通過連接事件消息中樞獲取待監(jiān)控的數(shù)據(jù)。我們使用shell腳本在Ubuntu系統(tǒng)上編譯代碼，通過執(zhí)行javac等指令把Java代碼編譯成可執(zhí)行文件，通過javamop等指令把Mop文件編織成JavaMOP代理。

圖4 自動代碼生成的主要流程

下面展示了一個生成的簡單的“monitor.mop”文件，其中“RESET”是一個特殊表達式，可以將監(jiān)控器重置為初始狀態(tài)。

monitor()

event exceed_speed after():

call(**.exceed_speed())

ltl :[]!(exceed_speed)

@violation {System.out. println(“warning from mop”);RESET;}

2.5 界面設(shè)計

我們在Ubuntu14.04上成功地實現(xiàn)了ROS-Monitor框架。為了讓系統(tǒng)易操作和使用，提供了一個用戶界面，如圖5所示，用戶可以設(shè)置“Source”、“Var”、“Event”和“Property”字段內(nèi)容。當用戶點擊“Generator”按鈕時，工具將根據(jù)自定義場景描述，自動生成Java代碼和Mop代碼并編譯到JavaMOP代理中。當用戶單擊“Reset”按鈕時，輸入內(nèi)容將被清除，如果監(jiān)控器正在運行，它將被強制停止監(jiān)控。當用戶點擊“Monitor”按鈕后，系統(tǒng)會結(jié)合場景描述內(nèi)容，監(jiān)控正在運行ROS的系統(tǒng)。如果系統(tǒng)行為違背安全屬性，警告日志將被打印在“Monitor Result”文本框內(nèi)。

圖5 用戶界面

3 安全策略和實驗

本節(jié)通過一個簡單示例和一個綜合實驗來介紹ROS-Monitor框架的使用。用戶可根據(jù)具體的需求，通過自定義場景描述生成特定的監(jiān)控器，即可方便地監(jiān)控系統(tǒng)行為。

3.1 簡單示例

攻擊者可以通過在TCP/IP層構(gòu)造虛假請求包來偽造ROS節(jié)點。例如在節(jié)點注冊之前進行發(fā)布或訂閱主題，該操作不符合主題發(fā)布的正常運行順序，會帶來潛在威脅。因此必須ROS系統(tǒng)中節(jié)點在發(fā)布主題之前，確保該節(jié)點已經(jīng)注冊。假設(shè)系統(tǒng)發(fā)布節(jié)點為“talker”，則自定義場景描述為：

Source:

node: talker

Var: None

Event:

node_start: talker.register

node_publish: talker.publish

Property:

ltl:[]node_publish=>(*)node_start

violation:

System.out.println(“Suspicious Nodes”);

此示例對“talker”節(jié)點的注冊和發(fā)布進行安全監(jiān)控。由于操作不涉及變量，“Var”字段為空。當觸發(fā)“talker”節(jié)點注冊活動時，激活“node_start”事件；觸發(fā)“talker”節(jié)點的發(fā)布主題時，激活“node_publish”事件。為了保證系統(tǒng)始終處于安全狀態(tài)，則必須保證在節(jié)點發(fā)布主題之前先注冊該節(jié)點，即在激活“node_pulish”事件之前先激活“node_start”事件，LTL語句為“[]node_publish=>(*)node_start”。若系統(tǒng)行為違背該安全屬性，則打印出“Suspicious Nodes”警告信息。

圖6顯示了節(jié)點發(fā)布的有限狀態(tài)機的轉(zhuǎn)化過程。其中“ST”指的是系統(tǒng)處于“start”狀態(tài)?！癝”指的是系統(tǒng)處于“safety”狀態(tài)，“US”指的是系統(tǒng)處于“unsafety”狀態(tài)。當“node_start”事件被激活時，系統(tǒng)從“ST”啟動狀態(tài)遷移到“S”安全狀態(tài)。若之前未先激活“node_start”事件，而直接進行“node_publish”事件操作，系統(tǒng)將遷移到“US”狀態(tài)并發(fā)出警告提示。

圖6 節(jié)點發(fā)布的有限狀態(tài)機

3.2 綜合實驗

本節(jié)我們以一個綜合的案例介紹ROS-Monitor框架。無人駕駛汽車又稱為輪式移動機器人，它通過車載傳感器感知周圍環(huán)境，獲取道路和障礙物信息來控制車輛的轉(zhuǎn)向和速度，從而使車輛能夠安全、可靠地在道路上行駛。

Gazebo[20]是ROS中的物理仿真環(huán)境，它是一款機器人的仿真軟件，基于ODE的物理引擎，可模擬機器人以及環(huán)境中很多物理特性。我們采用Gazebo建立無人駕駛小車模型，車身搭載激光雷達[21]。激光雷達數(shù)據(jù)量大、檢測距離遠、精度高，可以獲取很多的三維坐標信息。通過這些信息，我們可以檢測障礙物的方位，判斷它的大小、高度等。本實驗基于Gazebo環(huán)境構(gòu)建了一個虛擬的駕駛道路場景，模擬小車通過十字路口的過程。期間進行多次實驗，讓小車分別以直行和轉(zhuǎn)彎的方式通過該路口。我們設(shè)計了小車在行駛過程中，必須保證的4個重要的安全屬性：

1) 節(jié)點必須遵循主題的發(fā)布訂閱規(guī)則，主題被訂閱之前，該主題已經(jīng)被發(fā)布了。即在“car”節(jié)點訂閱“cmd_vel”主題之前，“car_control”節(jié)點已經(jīng)發(fā)布了該主題。

2) 當“car_control”節(jié)點發(fā)送消息時，該節(jié)點必須已發(fā)布主題，并且該節(jié)點處于未關(guān)閉狀態(tài)。

3) 當汽車行駛到十字路口，不能超過十字路口限定速度16 km/h，否則發(fā)出超速警告。

4) 不允許“car”節(jié)點高速急轉(zhuǎn)彎通過十字路口。角度和速度分別不能同時超過50°和13 km/h。

根據(jù)上述安全屬性描述，我們設(shè)定自定義場景描述如下：

Source:

topic: cmd_vel

node: car_control, car

Var:

speed: cmd_vel.linear.x

angle:cmd_vel.angular.z

Event:

crtl_publish: car_control.publish

car_subsribe: car.subsribe

crtl_close: car-control.unregister

crtl_send: car_control.send

turn_speed: speed>13

turn_angle: angle>50

exceed_speed: speed>16

Property:

ltl:[]car_subsribe=>(*)crtl_publish

@violation: System.out.println(“violate publish subscribe“);

ltl:[]crtl_send=>(not crtl_close S crtl_publish)

@violation:System.out.println(“Suspicious Nodes”);

ltl:[]!exceed_speed

@violation:System.out.println(“exceed speed”);

ltl:[]!(turn_speed and turn_angle)

@violation: System.out.println(“Sharp turn at high speed”);

本實驗運行了2個小時，監(jiān)控結(jié)果參見表3。此實驗共出現(xiàn)22條警告。其中，V1屬性違反次數(shù)為0，所有的節(jié)點都遵循發(fā)布/訂閱規(guī)則進行通信。對于V2屬性，正常情況下較難發(fā)生，我們模擬了5次不合理的節(jié)點啟動順序。關(guān)閉節(jié)點后，該節(jié)點發(fā)布主題消息，監(jiān)控器打印了5次違規(guī)警告。由于小車無法識別特殊路段的限速標志，導致通過十字路口時，超過了我們設(shè)定的最大速度限制。因此汽車在V3屬性上顯示13條超速警告。對于V4屬性，有4個急轉(zhuǎn)彎警告是由于遇到突然出現(xiàn)的其他汽車時沒有及時進行降速躲避。

表3 實驗結(jié)果

通過實驗分析，該框架可以全面監(jiān)視汽車每個節(jié)點的運行狀態(tài)，在系統(tǒng)沒有違背安全屬性的情況下沒有發(fā)出告警信息，在系統(tǒng)違背安全屬性的情況能夠準確打印告警，并且告警次數(shù)符合預(yù)期。以上實驗驗證了ROS-Monitor框架的可用性，保證了系統(tǒng)的正常安全通信。

4 結(jié) 語

針對ROS在節(jié)點活動和消息通信方面存在的安全問題，本文提出ROS-Monitor的運行時驗證框架。該工具可以將自定義描述場景生成特定的監(jiān)控器，包括自動生成的Java代碼和Mop代碼，并支持LTL等時序邏輯對ROS進行驗證。在系統(tǒng)行為違反安全屬性時，打印相關(guān)警告信息。該框架適用于主題方式通信的ROS模型(支持Indigo版本)，該工具從場景描述到監(jiān)控結(jié)果的產(chǎn)生，實現(xiàn)了高度的簡單化和自動化，并通過實際的案例驗證了該框架的實用性。ROS消息通信方式有主題和服務(wù)兩種類型，本框架僅對主題通信進行安全驗證，后續(xù)將在服務(wù)通信方面進行相關(guān)研究。