计算机应用已经渗透到了社会生活的各个方面，利用计算机对信息进行收集、加工、存储、分析以及交换等各种处理，越来越成为必不可少的手段。而对于任何一个完善的信息系统，最重要的需求之一就是安全。在传统的访问控制方面，研究人员已经提出了多种访问控制的策略和模型，如自主存取控制、强制存取控制、Bell-LaPadula策略和基于角色的访问控制等，但是它们还是各有局限。目前，访问控制模型的发展方向体现在：新的多变的应用环境和复杂的对象类型，使得访问控制需求不再是单一访问控制策略可以满足的，访问控制模型应该必须能够描述多种访问控制策略。本文根据国内外已有的研究成果及应用情况，系统地研究了多种经典的安全策略与模型。在此基础上，我们提出了一个可扩展的安全控制模型。该模型采用面向过程的安全控制定义方式，支持授权规则、权限转移规则以及义务规则的定义。用户可以基于安全控制规则和安全控制过程的定义来进一步描述多种安全控制策略。而整个模型及安全策略的形式化定义则是基于一种扩充的时态逻辑系统。本文所做的工作内容及贡献在于： 第一，提出了一种可扩展的安全控制模型，在此框架下，基于授权、权限转移和义务三种安全规则，安全控制过程的定义以及可变对象属性的概念，我们可以灵活地描述不同的安全策略。 第二，在经典的动作时态逻辑TLA的基础上，通过对系统状态序列语义和动作语义进行扩展，并引入更丰富的时态操作符，将其扩展为TLSecA。并在TLSecA的框架下对安全控制规则和安全控制过程进行了较为精确的形式化定义。 第三，在TLSecA的框架下，对安全属性进行了较为系统的分类。并进一步以TLSecA作为描述信息流安全属性的基本手段，定义了确定和非确定系统以及传递和非传递非干扰安全属性。 第四，对系统模型、安全模型以及安全属性采取统一的形式化定义方法，对具体的访问控制模型和应用模型及其各自特定的安全属性进行了形式化定义，并使用定理证明和模型检查两种技术，对不同的安全属性进行了验证。 第五，在Schneider安全自动机理论的基础上提出了可扩展的安全自动机，用以描述基于执行监控器的安全控制执行机制。同时给出了各种安全自动机执行能力的定义，进一步分析了基于类似事务处理方式的安全控制执行机制的执行能力。 最后，在TLSecA的框架下，对一个实际的安全系统——SELinux的安全策略配置语义和安全控制执行机制进行了基本的建模和分析。