如需转载请注明出处，侵权必究。
论文题目：From Control Model to Program: Investigating Robotic Aerial Vehicle Accidents with MayDay
发表会议：Security 2020
本文第一作者是Taegyu Kim教授，研究方向是网络物理安全（例如无人机），系统安全和软件安全。作者目前在宾夕法尼亚州立大学信息科学与技术学院担任助理教授。本文是其在普渡大学担任博士后研究员时发表的。
概述
随着无人机（Robotic Aerial Vehicles）的广泛应用，相关的飞行事故频繁发生，有必要对此类事故深入调查。然而，现有的方法无法深入到RAV控制程序中以调查事故的根本原因，主要的原因是（1）RAV的飞行日志仅记录上层的无人机控制状态和事件，而没有记录控制程序的执行情况；（2）目前缺乏从控制器异常到程序变量损坏再到程序bug的追踪定位能力。
为了解决上述问题，作者开发了一个跨域事故后调查框架MAYDAY，通过将控制模型映射到控制程序，实现（1）无人机飞行过程中控制程序执行日志记录，以及 (2) 基于控制级和程序级日志，追溯导致事故发生的控制语义bug。
作者将MAYDAY应用于ArduPilot（流行的开源RAV控制程序），对10起由ArduPilot bug引发的RAV事故进行调查，发现MAYDAY能以高精度、最小的运行时间和存储开销查明事故的根本原因。另外，作者还发现其中有4个近期打过补丁的bug仍然容易受到攻击，作者向ArduPilot报告了相关问题。
背景
RAV控制模型
RAV 控制模型包括：（1）车辆动力学、（2）控制器和（3）控制算法。
对于车辆动力学，RAV可以沿六个自由角度稳定运动，包括x、y、z轴以及围绕轴的旋转。每一个6DoF由级联控制器控制，最终控制RAV的位置、速度和加速度。三个元控制器级联工作，上一个元控制器的输出会成为下一个元控制器的输入（因为位置、速度、加速度之间存在物理上的微分/依赖关系）。同时控制器还接收例如飞行任务和控制参数等其他的输入。整个级联控制器的输出可以是电机的油门值，或者另一个 6DoF 的输入。
图1 RAV控制模型
RAV控制程序
RAV控制程序实现了上述RAV控制模型。RAV控制程序接收两种输入：（1）无人机的传感器数据。（2）地面控制的操作命令。控制程序周期性运行来调整多个控制器，并且在每次循环中记录控制器状态（无人机状态和参考状态）和事件（传感器和地面控制输入），存储在板载持久存储中。
挑战
无人机（RAV）事故原因
RAV事故发生的原因多种多样，包括（但不限于）：（1）物理原因，例如物理组件故障、环境干扰和传感器的硬件缺陷。（2）控制程序中的一般程序错误，例如缓冲区溢出等。（3）特定领域的程序控制语义错误，即实现底层RAV控制模型时的控制程序编程错误。前两种分别涉及RAV的硬件和软件层面，而第三类涉及RAV的信息物理（cyber-physical）层面。
控制语义事故难以调查的原因
作者给出如下图所示的动机案例。一辆无人机首先以匀速正常飞行，直到任务设定的转弯点时，收到指令，无人机减速，正常转弯，再加速，然后继续保持匀速向东飞行。但是在加速之后的飞行过程中，无人机突然变得不稳定，随后坠毁。调查证明，事故的根本原因是控制语义错误——控制程序未能检查控制参数（由地面操作员或攻击者通过远程指令设定）的有效性。
此类事故难以调查的原因是：（1）对无人机的物理影响并不是在触发事件（即指令下发或控制参数变化时）立即产生，在跨越一定时间后就很难建立两者的因果关系。（2）RAV飞行日志记录的状态和事件数量多，定位触发事件具有挑战性。（3）定位触发事件后，再深入定位到控制程序中的bug具有挑战性。
图2 控制语义bug导致的事故案例
解决思路
为了解决以上的问题与挑战，作者开发了跨域事故后调查框架MAYDAY，通过将控制模型映射到控制程序，实现（1）无人机飞行过程中控制程序执行日志记录，以及 (2) 基于控制级和程序级日志，追溯导致事故发生的控制语义错误。
具体来说，为了丰富调查证据（日志），MAYDAY在控制变量依赖模型（CVDG）的指导下，首先分析控制程序并插桩以获取控制程序的执行日志。此步骤实现了控制模型到控制程序的映射。
为了调查事故，MAYDAY执行两步调查：（1）在控制级调查中，MAYDAY 分析控制级日志以识别：（i）最先出错的控制器，以及（ii）导致该控制器故障的控制变量损坏的顺序。（2）在程序级调查中，MAYDAY使用上一步的模型—程序映射来缩小要分析的程序级日志的范围，并输出非常小的一部分控制程序基本块，这些基本块包含事故发生的根本原因。
具体实现
MAYDAY的整体框架如下所示，主要包括两个阶段（1）控制程序分析和插桩。（2）事故后调查。其中事故后调查包括控制级和程序级两个方面。
图3 MAYDAY框架
控制变量依赖图（CVDG）
MAYDAY以RAV控制模型为指导。其中，控制器和控制变量之间具有依赖性，为了表示此类依赖，作者定义了控制变量依赖性图（CVDG）。CVDG表示6DoF控制器之间的一般依赖关系，而无需假设具体的实现算法。CVDG中的每个节点代表一个控制变量或控制器输入，每个有向边表示其两个节点之间的依赖关系。
图5 控制变量依赖图
CVDG映射到控制程序
此步骤首先将CVDG节点映射到程序变量。对于大多数的 CVDG 节点，控制程序现有的日志功能可以直接访问和记录相应的程序变量。对于特定的CVDG节点，例如xyz轴的速度是通过函数调用取回的。为了解决这个问题，作者对LLVM IR进行回溯：从函数中被日志记录的变量开始，回溯传递到该变量的其他变量，直到找到第一个不是日志记录的变量（例如类成员变量）作为对应的程序变量。
其次将CVDG边映射到程序代码。MAYDAY保守地识别source节点到 sink节点数据流的所有可能的程序路径。首先，执行路径不敏感和流敏感的指针分析以识别控制变量的所有别名。然后，对于识别出的每个别名，算法执行后向切片以识别可能影响控制变量值的程序代码。
最后，MAYDAY插桩LLVM Bitcode，在每个基本块的入口处插入程序级别的Logging方法，并将控制循环的迭代次数添加到Logging方法中。
控制级别调查
经过控制引导的程序分析和检测后，RAV将重新投入使用，并在执行任务期间开始生成控制级和程序级日志。如果发生事故，MAYDAY将通过两阶段（控制级别与程序级别）调查恢复和分析日志，以揭示事故的根本原因。
事故发生后，在控制级别调查中，MAYDAY首先（1）确定CVDG所有控制器中最先出错的控制器。然后（2）推断控制变量的损坏顺序，即CVDG中导致控制器故障的损坏路径。
由于控制器之间相互依赖，当事故发生时一定存在一个最先发生故障的控制器，其他控制器受此控制器的影响，在相互依赖和控制反馈循环之后出错。为了找到事故的根本原因，有必要确定最先发生故障的控制器以及故障开始的时间。
识别初始偏离控制器和一对上层偏离变量（例如状态和参考或参考和任务输入）后，MAYDAY将推断导致初始偏离的相关控制变量的损坏顺序。作者总结了四种可能的损坏路径，如下图所示。
图6 四种变量损坏路径示意图
根据最先偏离的变量对、XI与XC的状态一致性以及最先损坏的变量可以确定具体是哪种类型的损坏路径，如下图所示。
表1 四种变量损坏路径表
程序级别调查
程序级别调查利用上一步控制级别调查的输出，来实现缩小控制程序执行日志的范围。此步骤的最终结果是控制程序代码中的一小部分基本块（子集），其中包含导致事故发生的bug产生的根本原因。
具体来说，MAYDAY首先从控制级别分析过渡到程序级别。（1）根据离线分析时建立控制模型—程序的映射，将CVDG的损坏路径上的控制变量映射到程序变量。（2）定位初始偏离迭代时的程序踪迹（trace）。（3）从日志中恢复LLVM指令踪迹，来进行LLVM Bitcode级别的数据流分析。
MAYDAY采用如下算法，利用以上输入，执行后向污点分析找到所有程序级别变量损坏路径相关的数据流，并且可以识别每个损坏数据流的对应基本块。
算法 1 程序级别损坏路径基本块分析
实验评估
工具有效性
作者选择10起相关的无人机事故进行调查测试，基于的原则是（1）事故的根本原因确实是控制语义错误；（2）bug的性质应该具有代表性（例如无效的控制/任务参数值、整数溢出和被零除等）；（3）选择的事故中的初始偏离控制器应覆盖6DoF的所有六个维度；（4）事故中的CVDG损坏路径应该表现出多样性。
实验表明MAYDAY成功识别出所有事故的初始偏离控制器、损坏路径、控制程序中的漏洞基本块等内容，并且确认漏洞的根本原因确实存在于MAYDAY识别出的代码中，精确定位了bug的位置。
图7 事故调查数据
Bug检测能力比较
作者选择现成的bug查找工具Cppcheck 1.9、Coverity和RVFuzzer进行比较，其中Cppcheck和Coverity没有报告10起事故中的任何bug。对于Case 1-6，由于缺少控制模型的知识，Cppcheck和Coverity完全无法检查控制/任务参数输入的有效性，或者确定RAV控制器状态在语义上是否有效。另外，由于静态分析工具的缺陷，包括检测除零错误时容易出现较高的误报/误报以及不了解控制语义，导致静态分析无法检测语义错误（例如错误的变量名），使得两者都无法确认某些除零错误的存在。同时两者也都没能检测到Case 7的整数溢出错误。
RVFuzzer自动改变可通过GCS命令动态调整的控制参数值，以识别控制参数的无效值范围，即输入验证错误。与RVFuzzer的比较发现，RVFuzzer能够触发由GCS输入验证错误引起的8个案例。对于案例6，作者发现需要更改RVFuzzer的默认配置，延长模拟运行时间才能触发。对于案例10，作者发现错误不是GCS输入验证错误，而是根据风速传感器输入概率性触发。
图8 Bug检测能力比较
漏洞定位范围缩减效果
作者发现MAYDAY可以显著缩小待调查的控制程序代码范围，以便人工检查定位漏洞的根本原因。作者认为范围缩减效果主要归功于（1）控制模型 （CVDG）指导的损坏推理和（2）程序执行日志记录补充。
图9 基本块缩减比例
运行、存储及能耗额外开销
对于运行时开销，作者发现在400 Hz控制环路频率下，MAYDAY插桩的Log在一次循环中占用7.6%的时间—总计190.72 µs。作者认为，由于信息物理系统相对于其控制器CPU的控制频率本质上较低，因此细粒度的程序跟踪是可行的。
对于存储开销，作者发现其30分钟（许多商用RAV的最大飞行时间）总日志量大小不超过1.3 GB。轻型商用存储设备（例如64 GB SD卡）可以轻松容纳此类容量开销。
对于电池消耗，作者发现与RAV发动机相比，MAYDAY消耗的电池电量相当少。对于配备四个电机的四旋翼飞行器，作者发现其主处理器板功耗最大为5.0瓦（不到总功耗的3.69%），而MAYDAY的功耗由主处理器板承担，因此占总功耗的比例甚至更小。
总结
本文揭示并集成无人机飞行控制模块控制程序的插装、跟踪和调试知识，为有效地调查无人机控制程序语义错误提供专门且通用的程序分析能力。具体包括：
在控制程序插桩方面，将控制程序模型形式化为控制变量依赖图（CVDG），并通过建立控制模型和控制程序之间的映射，弥合控制级和程序级的变量之间以及数据流之间的语义差距。
在控制程序跟踪方面，能够以较低的频率记录控制程序执行日志，带来的开销较小，使得运行时控制程序执行日志记录成为可能。
对于（事故后）控制程序debug，开发一个两阶段的事故调查流程。
控制级调查识别第一个故障控制器并推断控制变量损坏路径；
程序级调查在模型—程序映射的指导下，沿着控制变量损坏路径回溯程序以进行 bug 定位。
对10起RAV事故的调查表明，MAYDAY能够在合理的时间和存储开销下准确定位所有的bug，并且发现其中4个bug在打补丁后依然存在漏洞。
供稿：魏宏涛
审稿：黄宗安、邬梦莹、洪赓
排版：边顾
戳“阅读原文”即可查看论文原文哦~
复旦白泽战队
一个有情怀的安全团队
还没有关注复旦白泽战队？
公众号、知乎、微博搜索：复旦白泽战队也能找到我们哦~
如有侵权请联系:admin#unsafe.sh