基于形式化方法的软件安全性验证技术研究

摘要

随着软件系统复杂度的不断增长,特别是软件在航天等尖端领域的应用,使得软件的安全性保障成为迫切需要解决的问题.传统的软件工程方法由于技术手段和应用对象的不一致而难以解决软件安全性问题.针对高安全软件,技术手段必须从系统各类功能状态和相互作用关系来考虑其安全性问题,遍历各种可能的输入或状态跃迁关系,分析出安全关键性的软件成分和可能风险.本文调研总结了各类形式化验证方法,在技术方法上提出以轻量级形式化方法进行模型安全性验证的工程实施途径,进一步的,进行了典型安全关键性软件的形式化验证,结论有效验证了本文所设计方案的可行性.