软件安全性的验证和编译

在当今信息社会，关键软件的高可信成了保障国家安全、保持经济可持续发展和维护社会稳定的必要条件。其中安全性是关注的重点之一，软件满足安全策略的证明方法是研究的热点之一。.本项目采用逻辑方法和类型方法相结合的方式，研究串行高级语言程序安全性的描述、证明、从高级语言级的安全性证明到目标语言级安全性证明的编译和在目标语言级进行安全性证明的检验的方法，解决该方法中主要的理论和技术问题，包括源语言的类型系统和逻辑系统的研究及它们的可靠性证明方法的研究、目标语言基础逻辑的研究、安全性证明的编译技术研究等。本项目还将实现出具证明编译器的一个原型，并尝试将这种方式用于操作系统内核和嵌入式软件的设计。.这项研究对保证关键软件的安全性，对建设我国各种安全的信息系统有着重要作用。