首页> 外文期刊>Programming and Computer Software >Integrating RBAC, MIC, and MLS in Verified Hierarchical Security Model for Operating System
【24h】

Integrating RBAC, MIC, and MLS in Verified Hierarchical Security Model for Operating System

机译:将RBAC,MIC和MLS集成在验证的操作系统中的分层安全模型中

获取原文
获取原文并翻译 | 示例

摘要

Designing a trusted access control mechanism of an operating system (OS) is a complex task if the goal is to achieve high level of security assurance and guarantees of unwanted information flows absence. Even more complex it becomes when the integration of several heterogeneous mechanisms, like role-based access control (RBAC), mandatory integrity control (MIC), and multi-level security (MLS) is considered. This paper presents results of development of a hierarchical integrated model of access control and information flows (HIMACF), which provides a holistic integration of RBAC, MIC, and MLS preserving key security properties of all those mechanisms. Previous version of this model is called MROSL DP-model. Now the model is formalized using Event-B formal method and its correctness is formally verified. In the hierarchical representation of the model, each hierarchy level (module) corresponds to a separate security control mechanism, so the model can be verified with less effort reusing the results of verification of lower level modules. The model is implemented in a Linux-based operating system using the Linux Security Modules infrastructure.
机译:设计操作系统(OS)的可信访问控制机制是一个复杂的任务,如果目标是实现高水平的安全保证和保证不需要的信息流量的保证。甚至更复杂,当考虑若干异构机制的集成时,它被认为是基于角色的访问控制(RBAC),强制性完整性控制(MIC)和多级安全性(MLS)。本文提出了开发的访问控制和信息流量(HIMACF)的分层集成模型的结果,它提供了RBAC,MIC和MLS保留所有这些机制的密钥安全性的整体集成。此模型的先前版本称为MROSL DP模型。现在模型是使用事件-B正式方法正式的,其正确性正式验证。在模型的分层表示中,每个层次结构级别(模块)对应于单独的安全控制机制,因此可以通过重用较低级别模块的验证结果的努力来验证模型。该模型是在基于Linux的操作系统中实现的,使用Linux安全模块基础架构。

著录项

  • 来源
    《Programming and Computer Software》 |2020年第7期|443-453|共11页
  • 作者单位

    Rusbitech Moscow Russia;

    Russian Acad Sci Ivannikov Inst Syst Programming Moscow Russia|Lomonosov Moscow State Univ Moscow Russia|Moscow Inst Phys & Technol Dolgoprudnyi Moscow Region Russia|NRU Higher Sch Econ Moscow Russia;

    Russian Acad Sci Ivannikov Inst Syst Programming Moscow Russia|Lomonosov Moscow State Univ Moscow Russia|NRU Higher Sch Econ Moscow Russia;

    Russian Acad Sci Ivannikov Inst Syst Programming Moscow Russia|Lomonosov Moscow State Univ Moscow Russia|NRU Higher Sch Econ Moscow Russia;

    Russian Acad Sci Ivannikov Inst Syst Programming Moscow Russia;

  • 收录信息
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号