Formal Protection Modeling of Computer Security in Parallel and Distributed Systems

该项目涉及分布式网络安全的持续研究。 系统和开发一个正式的保护模型，称为 分布式模型（D-Model）。 D-Model定义了并发性 保证并发系统不能达到 以非安全方式配置权限的状态。 这项工作将扩展D模型，包括安全正确性 信任主体的标准。 到目前为止，D模型的条件已经 用于构建Bell-LaPadula安全的分布式版本 模型 D模型在这方面的应用更多。 项目，如克拉克威尔逊模型，明斯基的转移， 特权模型和军事消息系统模型（MMS）， 国防军 该项目正式建模部分的第二阶段将 开发所谓的通用分布式安全模型 （GPDSM）。 该模型的结果将是一组安全模型 它可以用来描述所有计算机系统的状态， GPDSM必须在第一步正式化。 后 形式化，任何模型（例如D模型、MMS和非干扰 模型）可以在GPDSM中实现。 由于同步是 分布式环境中约束并发性重要问题， 并行系统，D-模型将被移植到一个非干扰 模型框架（即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.