Shangfute's Blog
Cyber-Physical Systems & Formal Methods

春节回家想把Mac mini留在家里，当做一台远程主机使用。但是家里没有公网IP，只能通过ssh远程连接出来。

在 Mac 上执行

建立远程ssh隧道，将本机的22端口转发到远程主机45.32.126.157的 2222 端口上，这样就可以在VPS上管理我的Mac了。

AUTOMATED DETECTION OF VULNERABILITIES IN BLACK-BOX ROUTERS (AND OTHER NETWORK DEVICES)

动机

网络协议一般是基于公开的标准，但是互联网运行在大量的闭源网络设备上，如路由器和交换机。设备制造商如果对标准协议的实现进行细微的修改，就会导致协议的安全性问题，如产生攻击者可以利用的逻辑漏洞。这样的漏洞可能会影响该制造商的很多设备。找到路由器协议实现的漏洞需要大量精力对设备进行逆向工程。

研究目标

一种方法是利用自动化形式化黑盒方法（基于模型的测试）发现协议实现中的变化，而不需要获得设备的源代码。 黑盒：不需要获得设备的源代码或二进制代码。 形式化：基于严谨证明的基础的系统化方法 自动化：手动配置好之后，不需要人工辅助

基本思想

将路由器的行为与标准协议（部分）功能模型进行对比 简单的途径：根据预定的启发式方法，手动选择测试 我们的途径：利用符号执行自动生成测试，覆盖所有功能模型

劫持栈指针（Stack pivot）就是改写rsp(esp)，使其指向其他位置。这样栈也就被劫持到攻击者控制的内存上去，然后在该位置做ROP。

为什么要劫持栈指针？

1. 可以控制的栈溢出的字节比较少，难以构造较长的ROP链，无法直接利用溢出字节进行ROP
2. 开启了PIE保护，栈地址未知，并且无法泄露，但是利用某些技术（如ret2dl-resolve）时，必须知道栈地址，可以通过stack pivot将栈劫持到相应的区域
3. 其它漏洞难以利用，stack pivot 能够将一些非栈溢出的漏洞，变成栈溢出的漏洞，例如，将程序劫持到堆空间中。

利用条件

如果在尝试了直接Rop发现比较难实现，并且程序中有可以利用进行读写的函数，就可以考虑stack pivot stack pivot

1. 可以控制程序执行流

2. 存在地址已知，内容可控的Buffer

   • BSS，由于进程按页分配内存，分配给bss段的内存大小至少一个页(4k,0x1000)大小。然而一般bss段的内容用不了这么多的空间，并且bss段分配的内存页拥有读写权限
   • 堆，但是需要我们能够泄露堆地址。

3. 可以控制sp指针。一般来说 …

正如这个技巧名字所说的那样，这个技巧就是构造一个虚假的栈帧来控制程序的执行流。

原理

概括地讲，我们在之前讲的栈溢出不外乎两种方式

• 控制程序EIP
• 控制程序EBP

其最终都是控制程序的执行流。在frame faking中，我们所利用的技巧便是同时控制EBP与EIP，这样我们在控制程序执行流的同时，也改变程序栈帧的位置。一般来说其payload如下

buffer padding|fake ebp|leave ret addr|

即我们利用栈溢出将栈上构造为如上格式。这里我们主要接下后面两个部分

• 函数的返回地址被我们覆盖为执行leave ret的地址，这就表明了函数在正常执行完自己的leave ret后，还会再次执行一次leave ret。
• 其中fake ebp为我们构造的栈帧的基地址，需要注意的是这里是一个地址。一般来说我们构造的假的栈帧如下

fake ebp
|
v
ebp2|target function addr|leave ret addr|arg1|arg2

这里我们的fake ebp指向ebp2 …

首先，精确定义UAV系统安全。针对通用UAV系统，识别出一组相对完全的安全属性，并且提供统一的格式。安全属性有两部分组成：攻击行为和想要的安全属性。 然后，分析UAV系统是否安全。根据一组安全属性自动生成攻击行为，使用可达性和LTL属性对安全属性建模。

收集UAV系统潜在的攻击方式。通过分析攻击的关联，识别原子攻击行为，使得所有攻击都是原子攻击的组合。利用攻击树形式化表示原子攻击的所有组合，构成全部可能的攻击。

提出从安全属性，自动生成攻击树的算法。然后根据攻击树生成攻击模型，并将每种攻击模型关联到相应的安全属性中。

每种攻击使用形式化语言CSP＃建模，每种安全属性形式化为可达性或暂态属性。根据系统模型、攻击模型和需要的安全属性，可以通过模型检查工具PAT验证系统在某种攻击下，是否满足安全属性。

创新点

1. 识别出相对完整的UAV系统的安全属性集合，考虑到了各种UAV系统中的子系统。
2. 提出自动根据安全属性生成攻击树的算法，然后自动生成攻击模型。
3. 验证系统。

安全需求识别

首先，识别UAV组件。UAV、地面站、飞行员、通信信道

对每个组件，识别 1. 安全保证 2. 攻击行为。

攻击行为之间可能存在关联：两个攻击结果相同、一个攻击依赖于另一个攻击 …

研究对不确定性变量进行计算的程序。

研究目标

开发静态和动态分析技术，能够将概率程序看成随机过程进行推理。

应用领域

分析机器学习中使用的模型：当输入存在噪声时，分类器性能如何变化。

分析随机化计算：系统化建立随机算法的属性。

分析传感器数据融合算法：对融合算法进行推理。

主要关注的问题

随机化安全性：给定概率程序P和状态集合U，在N步内程序执行到U的概率是多少。

时序逻辑属性：研究以1的概率成立的时序逻辑属性，包括，几乎确定终止（程序以1的概率终止），几乎确定常返（程序无限次访问某个状态集合），几乎确定持续（程序执行到某个状态集合，并永远留在集合内），以及整改暂态属性体系。

研究途径

概率程序的符号化推理：通过符号化决策过程对概率程序的抽象语义进行推理。

使用符号化执行和解空间大小计算的方法根据有限的执行路径获得整个程序的属性。

假设控制算法和估计算法的设计者十分了解物理系统，并且假设物理系统是线性系统。

但是，现在的CPS越来越复杂，并且存在人的影响，其行为很难预测，这些假设不一定成立。

CPS的复杂性 人的复杂性建模 － 航管员 从数据中推理出能够区分想要的和不想要的行为的STL公式。 公式可以指示出每个行为集合可能的原因。 使用鲁棒度的概念在这个行为集合上进行有向搜索。

研究新的算法从数据中学习出STL规格，而STL规格可以使用自然语言解释。

唯理论：从逻辑假设出发，进行推理。形式化方法。知识表示，逻辑推理，符号主义。无法处理不确定性。

经验论：从经验数据中总结公式。机器学习，深度学习。概率，连接主义。黑盒，不知道根据那些规则进行推理的，无法验证。

但是机器学习得出的结论，不够理性，无法知道事件之间潜在因果关系。不知道我是否知道，也不知道我是否不知道。我们如何知道我知道，如何知道我们不知道什么。深度学习需要大量训练数据才能工作，但人类只需要少量的sample就可以学到大量知识。

对概率推理进行建模。因为现在的CPS模型和攻击者模型十分复杂，难以使用数学公式进行建模。特别是对人（控制员和攻击者）的认知模型进行建模。

混合自动机的可达性分析：已知系统模型和规格的验证问题

现在的CPS传感器和激励器一般没有加密，因而容易产生各种完整性攻击方式。而直接加密的话，对计算性能要求较高，有没有一种半加密的方式，满足两者的要求。

基于格理论的密码学与随机性有关，是否可以与实际物理系统关联起来，利用物理系统的随机性？

根据CPS的随机性分布，建立满足随机性的程序分析方法。

本文是对Cyber-Physical Systems Security: a Systematic Mapping Study的学习笔记。

0. 引言

Cyber-physical systems (CPS) 是完成计算、通信、控制的软硬件的无缝集成，与物理组件联合设计。由控制器、传感器、激励器三大组件构成。在2006年左右提出。

CPS的应用领域包括：可信医疗设备、生活助理、交通管控、能源保护、环境控制、航空、关键基础设施（电力、水资源、通信系统等）、制造业、智慧建筑等。可以预见CPS的发展将使20世纪的IT技术革命相形见绌。

CPS与传统IT系统的区别：CPS是资源受限的实时系统。

毫无疑问这些系统的安全性(security)是需要考虑的主要因素。环境的不确定性、安全攻击、物理设备的故障都可能导致安全问题。

给定CPS中使用的估计和控制算法，设计要满足的 …