Formal Protection Modeling of Computer Security in Parallel and Distributed Systems

该项目包括继续研究分布式系统的安全性，并开发一种称为分布式模型（D-Model）的正式保护模型。d模型定义了并发条件，保证并发系统不能达到以不安全的方式配置特权的状态。这项工作将扩展d模型，使其包括可信主体的安全正确性标准。到目前为止，d模型条件已被用于构建Bell-LaPadula安全模型的分布式版本。d模型在本项目中的应用较多，如Clark-Wilson模型、Minsky的特权转移模型、Landwehr的军事信息系统模型（Military Message System Model， MMS）等。这个项目的正式建模部分的第二阶段将开发一个所谓的通用分布式安全模型（GPDSM）。这个模型的结果将是一组安全模型，可以用来描述所有处于最先进状态的计算机系统。GPDSM必须在第一步正式确定。在形式化之后，任何模型（如D-Model、MMS和非干扰模型）都可以在GPDSM中实现。由于同步是分布式和并行系统中约束并发性的一个重要问题，因此D-Model将被移植到非干扰模型框架（即GPDSM）中，以便找到非干扰同步问题的解决方案。D-Model目前没有相关的隐蔽通道分析工具。建议的GPDSM也将作为模型和隐蔽信道分析工具。

This project involves continued research in security of distributed systems and development of a formal protection model called the Distributed Model (D-Model). The D-Model defines concurrency conditions which guarantee that a concurrent system cannot reach a state in which privileges are configured in a non-secure manner. This work will extend the D-Model to include the security correctness criteria of trusted subjects. So far the D-Model conditions have been used to construct a distributed version of the Bell-LaPadula security model. There are more applications of the D-Model within this project, such as the Clark-Wilson Model, Minsky's transfer of privilege model, and the Military Message System Model (MMS) of Landwehr. The second phase of the formal modeling part of this project will develop a so-called General Purpose Distributed Security Model (GPDSM). The result of this model will be a set of security models that can be used to depict all computer systems within the state-of- the-art. The GPDSM must be formalized in the first step. After the formalization, any model (e.g. the D-Model, MMS and Non-interference models) can be implemented in GPDSM. Since synchronization is an important issue for constraining concurrency in distributed and parallel systems, the D-Model will be ported to a non-interference model framework (which is the GPDSM) in order to find a solution for non-interference synchronization problem. The D-Model has currently no associated covert channel analysis tool. The proposed GPDSM will also serve as both a model and a covert channel analysis tool.