本次系统安全暑期学校涵盖的内容非常广泛，有深有浅地包括了模糊测试技术，AI 系统安全，硬件辅助系统安全，传统二进制安全，嵌入式系统安全以及固件分析，形式化方法等各种内容。既有对于前沿科研成果的介绍，也有技术分享的干货。

接下来将对几个较为感兴趣的报告作一些总结，分别是刘洋老师的有关模糊测试技术的分享，夏虞斌老师的有关硬件扩展的分享，以及陈立前和赵勇望老师的有关形式化技术的分享。

模糊测试技术

对于模糊测试技术，之前的了解较为浅显。刘洋老师从五个方面介绍了他们小组在模糊测试方面进行的安全方面的工作。

第一部分介绍了模糊测试中如何更合理地生成种子，可以通过将上下文加入考虑，建立执行路径的概率模型。第二部分则更细粒度地介绍了如何理解种子的意义，衡量种子之间的距离，以及基于优先的排序等，对之前提到的模糊测试框架的闭环有了更好的阐释。

第三部分介绍了模糊测试如何和其他的想法进行结合。比较有启发的一个例子是和符号执行进行结合。对于一些条件表达式（ 例如 x == 1 && y == 2） 来说，更适合使用符号执行（很快可以得到该路径的输入）而不是随机 mutation ；对于另一些条件（非线性的表达式）来说，符号执行则会引入相当大的复杂度，使用随机的算法则更加合适。

第四部分介绍了对于特定类型的缺陷和漏洞如何进行模糊测试。用 UAF 举例，触发一个 UAF 必须经历一些复杂的操作序列，因此在传统的模糊测试中很难被触发到。而刘洋老师的团队将触发 UAF 这个小目标转化为一个有效状态机，根据这个 FSM 的需求进行插装，然后再在测试框架中根据这个状态机的输出反馈指导种子的选择，mutation 等等，就能够很好地对这一类型的缺陷和漏洞进行挖掘。同时，这个工作流程其实是非常通用的，能应用到很多别的目标上。

最后一个方面是模糊测试在其他领域内的使用。如何将各种概念（错误，mutate 等）进行领域间的迁移，也是很有趣的工作。

总体理解下来，发现刘洋老师做科研的思路非常清晰：简单而有效的 idea ，许多研究工作给人一种「就该这样做」的感觉，从直观理解上和从实验结果上看都容易被人接受。

硬件扩展

夏虞斌老师来自于有名的上海交通大学 IPADS 实验室。对于硬件扩展方面的介绍非常的全面以及清晰，听讲座之后受益匪浅，我对于这一领域的技术发展，漏洞的基本防护思路都有了一定的了解。讲座的结构也很清楚，首先对于用于安全增强的硬件扩展进行了介绍，之后是用于隔离执行环境的硬件扩展，最后介绍了原先并不是专用于安全增强的一些硬件扩展。

Intel SMEP 对数据在用户态和内核态的执行权限进行了限制，使得特权程序并不能直接执行用户态可控的一些数据，因此可以减轻 Return-to-user attack 带来的影响。类似的另一个还有 SMAP，使得特权程序不能够直接读写用户态的数据，从而内核不会解引用恶意指针。在 ARM 架构下，同样也有类似的 PAN，PXN，UAO 等扩展来进行对数据在特权模式和用户模式下访存的限制。Intel MPX 能够在硬件级别进行边界检查，但是大量的边界检查仍会占用相当多的内存，并降低性能。Intel MPK 将内存进行分为 16 个域，通过用户态的特殊指令设置 pkru 寄存器来控制域内页的读写权限。

其他一些有意思的硬件扩展或者概念包括：

• Intel CET，用来做 CFI，想法有两个
  • Shadow stack
  • Indirect branch tracking
• SGX 中
  • 用来保证内存完整性的 Merkel Tree 的应用挺有意思。但是大量的计算哈希却带来了对于内存大小的限制。
  • 用着 （我最喜欢的） CTR 工作模式
• 以 Huawei 手机为例的四层 Trust Level 的解释
  • Secure Domain (身份认证，eID)
  • Trusted Domain (TrustZone and TEE)
  • Protected Domain （Hypervisor）
  • Rich Domain (Linux or Android)
• Intel MKTME( Multi-Key Total Memory Encryption)
• Intel CAT
  • The 「Noisy Neighbor」 Problem，太形象了

夏老师还提到了给内存加 tag 的相关工作还有 PUMP（Programmable Unit for Metadata Processing），基于 Micro-Policy 从而做到更细粒度的 CFI ，Memory Protection 等。

比较有意思的点还在于，硬件扩展在设计之初的目的会非常单纯，但是在实现之后使用它的方法可以有很多创造性的想法，从而做到一些意料之外的事情。

形式化方法

本次暑期学校共有两个讲座是有关形式化方法的，陈立前老师着重介绍了形式化方法如何在数值分析领域应用的，并提供了许多易于理解的例子来辅助学习形式化方法的基本思想和能够做到的事情。赵勇望老师集中介绍了在安全软件中应用形式化方法的基本思路和步骤。

陈立前老师主要从数值分析的应用场景出发，介绍了抽象解释的基本概念，描述如何通过抽象域的演算过程来代表在具体域上面程序的运行，变量值的变化等。还介绍了最小不动点的意义和算法，使用加宽算子来使得计算过程快速终止的直观解释等等。

赵老师的讲座中，可以看到形式化方法可以被理解为一种建模的工具。对于自然语言描述的规范或者是要求，可能在理解上有很多歧义。而将规范实现为具体的实现，则可能引入更多的不确定性。形式化方法引入一种规范的无歧义而同时表达能力足够强的语言，来对各种规范进行描述。类似于数学中的描述和定义，形式化后的规范也具有了一系列性质，能够被推导和证明出来。对于任意的软件和实现应用形式化方法是非常不现实的，因此，现在的形式化方法只在关键性技术和容错要求极高的领域中有着广泛的应用。