这篇学位论文主要探讨了网络技术中的网络基础,特别是针对汇编指针程序的安全性验证。随着计算机科学的进步和软件应用的广泛性,软件安全性成为了至关重要的问题,特别是在关键领域。论文的作者旨在提高软件的安全性,确保所有程序错误在执行前被发现或在运行时能被温和地捕获,防止不可预测的系统行为。
近年来,程序性质证明方法得到了显著的发展,包括基于类型的和基于逻辑的方法。论文中提到的项目组选择了一种结合简单类型系统和自动逻辑推理系统的混合方法,以证明程序满足安全策略。这种方法在PointerC(一种具有动态存储分配的类C语言)上进行实验,开发了一个出具证明的编译器,该编译器能够将源程序和规范转化为汇编代码和等效规范,同时生成源程序满足规范的证明。汇编代码级别的验证有助于减少受信任计算基础(TCB)的大小,从而提高系统的安全性。
论文重点研究了汇编指针程序的安全性质验证,采用了Hoare逻辑、Proof-Carrying Code和Certified Assembly Programming等技术。作者设计了一种基于x86机器模型的汇编级指针逻辑,以解决别名处理的挑战,扩展了指针逻辑在汇编程序性质证明中的应用。通过这种方法,他们实现了一个原型系统,可以自动验证链表、二叉树等复杂的指针程序的安全性。
该工作的贡献在于提供了一种新的汇编指针程序验证方法,并开发了一个实用的原型系统,这不仅丰富了程序性质证明的研究,也为实际应用提供了可能。这项研究得到了中国国家自然科学基金和Intel中国研究中心的支持,进一步强调了软件安全、程序性质证明、形式验证框架等领域的重要性。
关键词:软件安全,程序性质证明,受信任计算基础,出具证明编译器,Hoare逻辑,指针逻辑,形式验证框架,携带证明的汇编程序。