可信软件代码中程序标注的使用及类型验证
Employment of Program Annotations in Trusted Code and Their Type Verification
-
摘要: 程序标注技术能够勾勒程序代码中的各种数据属性和软件行为,提出了使用许可类型系统作为沟通程序标注和程序代码的桥梁,从程序代码的角度分析和验证了程序的安全性,进而提升了整个软件系统的可靠性和可维护性。Abstract: We propose to use the permission system to act as a bridge connecting program annotations and program code.Within the permissions,we could verify the credibilities and safety properties of the program from the level of source code.Thus the reliability and maintainability of software systems could be improved.