论文部分内容阅读
信息流安全的形式化以无干扰性为标准属性.针对目前字节码级的信息流安全分析均未基于对程序无干扰性的语义表示,提出了一种基于语义的无干扰性自动验证方法.为适应语言特性和应用环境的限制,将基本自合成扩展为低安全级记录自合成,以支持对标错状态的可达性分析,保证标错状态不可达时对应字节码程序满足无干扰性.在此基础上为提高实际验证效率提出了3种模型优化方法.实验说明方法的可用性、效率、可扩展性及模型优化的实际效果.