开发安全的软件需要花费大量的人力物力，如何使开发安全的软件变得更容易是计算机学科的一个基本问题。通过容错、复用等技术手段以及谨慎的系统设计可提高软件的安全性，但是无法避免的各种程序漏洞始终影响着软件的安全性。近年来，软件规模不断扩大，复杂性不断提高，使得软件开发和维护变得越来越困难。Internet等网络技术的高速发展使得软件开发和维护过程中产生的漏洞给恶意代码的攻击和入侵提供了大量的机会。软件安全已经成为一个研究热点。本文重点研究程序行为安全约束和动态代码检查等技术： （1）阐述了代码检查的原因，从检查方法和检查时刻两个方面对代码检查方法进行了分类研究。分析比较了各种检查方法的优劣和在代码检查工具中的应用。 （2）分析了通过基于层次结构的安全规则分类方法和构造基本的安全规则样式的方法。通过这些基本的规则样式，可以比较方便高效地构造其他安全规则，从而提高形式化验证方法的使用效率和普及率。 （3）采用STL（Safe Temporal Logic）构造了时序安全特性的形式化描述。为了对时序安全特性进行描述和检查，我们用STL给出专门针对时序安全特性的形式化描述。 （4）实现了对时序安全特性的动态检查方法。根据时序安全特性的分类和形式化描述，使用模式识别的方法实现了在解释性语言中对时序安全特性的动态检查。 （5）分析了各种保护程序正常运行的方法，指出了存在问题。目前保护程序正常运行的方法主要分为四大类，这些技术被广泛地应用于对程序安全性进行保护。对消除软件漏洞，阻止攻击等方面确实起到了一定的作用，然而每种方法都存在一定的局限性。 （6）研究了基于程序行为控制的语义约束方法，提出了程序行为安全约束描述方法和系统框架。为了克服现有方法的局限性提出了程序行为安全约束描述方法。对安全约束进行了分类，给出了刻画安全约束的七个要素和安全约束形式化描述的具体示例。在安全约束的基础上给出了基于安全约束的程序行为控制框架。