基于组件的软件体系结构是软件工程研究领域中的一个新的而且重要的课题。基于组件及其装配连接设计出的体系结构可以提供更丰富的设计信息,它除了可以描述设计模块之间的交互作用关系之外,还可以描述设计模块之间的约束关系、利用某些预先定义好的计算模型分析每个计算模块应具有的特性,并进一步分析体系结构的整体特性。软件体系结构反映了在一定构形下软件系统所要得到的重要性质(如安全性),它为软件设计和构造提供早期决策。近年来许多基于软件体系结构描述语言和体系结构风格的支持工具和属性模型纷纷涌现。为一个复杂系统提供形式化的体系结构描述,为所有参与系统设计、实现、维护的人员提供精确的系统结构描述文本,能在系统结构层经济省时地提供分析系统性质的可能性,进行早期错误检查。软件安全性研究同样是目前比较热和新的研究领域,研究在软件体系结构中对安全性这种非功能属性如何给予描述、分析并验证是一项十分有意义的工作。软件的安全性是软件产品的质量属性之一,软件安全性保证是指在安全临界系统(safety critical system)的软件开发生命周期中进行的一系列质量保证活动,目的在于消除隐患。对于软件体系结构的安全属性,我们可以在形式化描述的基础上给出精确的形式化证明或给出其反例。软件体系结构的形式化模型有基于操作的模型、基于进程代数的模型、基于逻辑的模型、基于网络的模型。逻辑推理的方法有其自身的不足,模型检测的方法遇到的最大问题是状态空间的爆炸。目前的软件工具大多仅限于原型系统,有其应用的局限性。从数据结构和行为两方面来刻画软件体系结构模型的本质,这种方法更全面,用进程的行为来证明安全性更合理。目前软件体系结构在学术界的理论研究尤其是形式化方面的工作还相对缺乏,将安全性和软件体系结构结合起来的工作更稀少。在一个形式化的框架内对软件体系结构的安全性进行描述、分析和验证可以保证和维持基于构件的一类软件体系结构开发的一致性和完整性。因此使用形式化方法研究安全组件以及其交互形成的软件体系结构的安全特性具有重要意义和实用价值。针对软件体系结构的安全性问题,本文对描述模型和分析验证的方法进行了系统的研究和探讨,发展和完善了基于组件的软件体系结构模型性质的有关理论和方法,并将其应用到实际问题中。文中首先分析和总结、比较了现有的安全软件体系结构的形式化研究方法和技术,然后给出了安全软件体系结构的形式化框架。并在此过程中逐步明确:使用基于组件的软件体系结构来构造软件系统,需要建立软件体系结构模型,其本质是利用形式化方法建立形式化模型来描述和验证复杂系统,形式化方法严格的数学基础使得系统具有较高的可信度和正确性,需要用它来详细分析组件的行为、研究其同步和通信的关系。系统描述基于组件的软件体系结构模型和组件的构成语法和结构、操作、行为语义。其次,本文针对如何在安全软件体系结构中建立行为模型和静态结构模型、功能模型、过程模型的方法展开讨论。详细介绍如何使用状态转换系统描述安全软件体系结构的行为模型,包括建模方法的符号表达、建模步骤等。定义了稳定状态、稳定的状态转换、转换可达、直至形成系统的行为树,并建立系统的Kripke结构;通过证明状态转换系统的谓词转换器上不动点的存在来实现体系结构模型的安全性。由于进程代数的描述语言具有描述组件并发行为的能力,加上其严格的代数性质和强大的可借鉴的标准等价技术工具,文中重点使用它来进行基于组件的软件体系结构的安全性研究。使用进程代数的语言描述结构和过程模型(包括语法和操作语义),并在此模型基础上给出安全软件体系结构的描述规约,规约有文本表示和图形表示两种形式。进程代数语言描述的软件体系结构模型依靠构件类型、体系结构类型和构件实例的限制语义定义得到对静态操作符引起的交互行为语义;作为补充,主要从语法的角度建立静态结构模型来定义软件体系结构,它借鉴几种类型的文法对构件、连接方式、配置方式进行规则制定、形成软件体系结构的构成语法;功能模型是操作逻辑及其与其他形式化方法的结合,它使用时序逻辑描述系统安全性;为了更有说服力,文中还对常用的体系结构描述语言UML和Wright(另一种基于进程代数的语言)的系统软件体系结构建模能力进行分析,并将它们和其他基于进程代数的体系结构描述语言进行比较,并认为UML擅长于描述体系结构的静态结构如对组件、连接件的描述、对动作特定顺序的描述,不同视图可以从不同层次对体系结构进行描述,还能够通过版型(stereotype)的扩展机制实现进程代数语言描述的体系结构的静态建模,但是其描述动态结构能力差,最终不适合用它全面构造软件体系结构模型。本文中间部分重点介绍如何使用基于进程代数的软件体系结构描述语言和其标准观察等价技术对体系结构进行相容性检查和互操作性检查,并且通过扩展体系结构描述语言将体系结构的相容性和互操作性检查扩展到不同风格的体系结构上。它们的正确性评估分别基于一个压缩代理系统和一个导航控制系统。该方法有行为和代数的本质,其中一个体系结构的描述仅仅由有固定行为的组件和连接件的类型以及拓扑结构的约束组成。这为组合、分层、图形化的体系结构描述语言(为了基于组件的软件系统族的规约和分析所开发的)提供了一个统一的框架,它可以保证在一个与一个给定的安全的组件交互的软件组件集合之内保持安全性,并扩展这两种检查到整个体系结构中。该方法建立了软件体系结构模型并通过相容性和互操作性检查保证了模型的安全性,其中所有检查都依赖于弱互模拟等价的性质,由于效率与/或诊断相关的原因,它比直接证明软件组件集合更方便,这一点已经得到证实。作为对基于进程代数的描述语言的补充,本文还针对简单的两组件安全通信的情况引入基于组件的软件体系结构的另一种安全模型。该模型以信任逻辑为基础进行安全性分析,给出安全构件的正常交互协议(包括协议的描述、分析、验证),以及当非法入侵构件存在时构件异常交互的协议,以组件通过连接件进行安全信息交流的情况为例建立软件体系结构的安全模型,并且验证了在该安全协议基础上建立的安全软件体系结构模型中,每一次模型实现都可以得到良好的安全性保证。本文应用部分是按照在安全控制计算机系统的实例上层次式地建立系统软件体系结构的安全模型的过程逐步展开的。模型分为整个系统的软件体系结构模型、安全控制操作系统的模型、基于安全软件模型的访问控制部分软件体系结构的模型共三层。基于给定的安全标准,分析访问控制的安全模型包括自主访问控制、强制访问控制、基于角色的访问控制和信息流等安全模型。对这些基本模型的数学性质的详细研究为新的安全模型的建立提供了坚实基础。安全操作系统软件体系结构模型的建立是分几步走的:首先建立访问控制系统的体系结构缩减流图,详细分析原模型的局限性后通过举例说明来明确模型安全改造的方向;然后进行原体系结构模型的相容性检查,发现危险状态后分析引发危险的交互,反复重定义安全组件(判定组件和实施组件)的行为,指出引发危险的原因实际上是不合理的组件划分和细分后可能出现的违反组件互操作性的交互所造成的;最后详细论述经过改造后得到的新模型的安全性。安全操作系统的实现以原Linux操作系统为基础,其强制访问控制机制和信息完整性保护、增加安全标签的保护等方法都属于操作系统功能增强改进的方法,该方法在整个安全操作系统上的实现依赖于安全调用基于增强模型的访问控制机制。增强后的安全操作系统的全局体系结构图说明系统完全符合Flask结构。此外还以登录过程为例详细描述安全系统策略和技术的有效实现。本文的最后介绍该安全方法的应用和外延。将安全软件体系结构模型和方法和软件复用技术相结合,具体有组件的安全复用技术和软件体系结构的安全复用技术,并给出安全复用方法的定义和描述以及方法的具体实施;在文中还对安全方法的应用进行扩充,将之应用于安全组件的互操作性、交互隐私性、原子性等安全相关的非功能属性的分析。文末对论文的主要贡献进行了总结并提出了未来将开展的研究。