摘要
本期播客讨论了计算机安全领域的核心挑战，特别是系统漏洞的普遍性、攻击手段的多样性，以及形式化验证技术在构建安全系统中的应用前景。黎晓燕教授分享了从传统内存安全漏洞到侧信道攻击等多种威胁模型，以及学术界在形式化验证系统开发方面的最新进展。
核心要点
-
系统安全的根本困境：完全无漏洞的代码极其难以编写，安全漏洞具有普遍性和必然性，攻击手段随之不断演变。
-
多维度的安全威胁：
- 内存安全漏洞（如缓冲区溢出）：攻击者通过恶意输入导致程序状态被篡改，进而劫持控制流
- 远程攻击向量：攻击者可通过发送恶意数据包远程入侵系统
- 侧信道攻击：通过观察程序的输出行为和运行特征推断系统机密信息
-
漏洞的定义与本质：安全漏洞本质上是任何形式的代码缺陷，可被攻击者利用，而攻击类型的范围极其广泛。
-
安全保证的追求：安全研究的目标是为程序的安全属性提供尽可能强的保证，包括可证明的安全性（provable guarantees）。
-
形式化验证的可行性：
- 通过程序分析和形式验证技术可以证明代码不存在内存安全漏洞
- 学术界已在该领域投入数十年研究
-
形式化验证系统的现状：已有多个形式化验证系统成功应用于实际场景，包括微内核、编译器、文件系统和密码库等。
-
规模化验证的挑战：虽然形式化验证在小规模案例中已证实可行，但将其应用于大型实际系统仍存在挑战。
-
专业团队投入：学术界有专门团队投入数年甚至数十年的工作来开发验证工具和技术。
-
安全与机器学习的交叉：对抗性机器学习成为新兴安全研究方向，研究如何防御针对ML模型的攻击。
-
攻击多样性：攻击类型跨越内存安全、侧信道、应用层等多个维度，需要多管齐下的防御策略。
可执行建议
- 开发者层面：采用形式化验证工具对关键代码路径进行验证，特别是处理外部输入的模块
- 系统设计：考虑将系统分解为可形式化验证的微内核架构和可信基础组件
- 学习路径：关注机器学习安全领域的研究进展，理解对抗性样本和模型鲁棒性问题
- 防御策略：对内存安全、侧信道和应用层漏洞实施分层防御