基于AST自合成的嵌入式程序数据流安全验证方法

摘要

本发明公开一种基于抽象语法树AST自合成的嵌入式程序数据流安全验证方法，具体步骤包括：1、生成抽象语法树AST，2、对函数定义结点进行return归一化，3、对归一化后的函数定义结点进行自合成，4、配置安全级别，5、再函数定义结点中插入赋值结点与断言结点，6、验证数据流安全，7、结束验证。本发明克服了已有技术主要考虑功能属性，而忽略非功能属性的缺陷，以及在验证过程中需要用户输入安全规则的缺陷。通过自合成技术以及断言的插入使得本发明能验证出机密性无干扰与完整性无干扰，能自动化插入需要验证的安全断言，减少验证开销。

关键词