《软件定义网络元素与机器代码的形式化验证》

软件、可编程性与连接性已成为社会日益普及的特征。在人的一生时间跨度内，从车辆到电话等一切设备都已从固定功能设备演变为始终在线的通用可编程设备。其结果是，设备功能完全由软件决定，而这些软件可能随版本更新或安装应用的不同而改变。软件本身日益由外包顾问甚至人工智能编写，漏洞每日出现并被修复。

人们该从何处着手保护现代数字设备？最高级别的保障认证要求形式化验证——即基于硬件或编程语言语义模型、通过数学证明排除漏洞的方法。这项工作成本高昂且耗时，因此主要应用于小型关键组件。实现可扩展性的途径是将保障声明建立在高度自动化的验证工具基础上，这些工具的正确性仅依赖于最小化、可审计的可信代码库。

本文工作聚焦于机器代码与网络领域的形式化验证工具开发。其共同点在于使用交互式定理证明器来确保结果的可信度。具体而言，本文提出：（i）非结构化程序（尤其针对机器代码）的验证任务分解方法；（ii）P4领域专用网络语言的形式化模型，并附带（iii）可生成证明的符号执行工具，以及（iv）将经过验证的P4程序可验证地编译至软件交换机的完整工具链。

本汇编型论文的第一部分对第二部分进行概述并提供背景语境，第二部分由四篇论文组成（以首次发表或最新校对前版本的原貌呈现）。第一章为技术与非技术背景读者提供引言并阐述研究动机；第二章包含理解论文所需的理论与历史背景；第三章对相关及可比工作进行全面评述；第四章总结本论文工作对科学的贡献；第五章提出主要结论并展望未来工作方向。