Formal Methods for Software Certification

9708915本研究的重点是将形式化方法应用于进口软件的认证问题。集合约束、Kleene代数、Kleene代数和带测试的Kleene代数以及模态模微积分等形式系统已被证明为实际程序分析和验证提供了有力的工具。建议进一步发展这些系统，特别关注有效的实用算法，并研究它们作为软件认证工具的用途。目标是(i)使软件供应商能够轻松地构建一个证书，并与确保满足某些安全条件的编译对象一起下载；（ii）使客户端更容易检查证书，以验证外国代码在本地运行是安全的。希望这项工作将有助于消除不可信的软件。＊＊＊

9708915 This research focuses on applying formal methods to the problem of certification of imported software. Formal systems such as set constraints, Kleene algebra and Kleene algebra with tests, and the modal mu-calculus have been shown to provide potent tools for practical program analysis and verification. It is proposed to develop these systems further with special focus on efficient practical algorithms and to investigate their use as tools for software certification. The goals are (i) to make it easy for a software vendor to construct a certificate to be downloaded along with a compiled object that ensures that certain safety conditions are met; and (ii) to make it easy for a client to check the certificate to verify that the foreign code is safe to run locally. It is hoped that this work will contribute to the elimination of untrustworthy software. ***