Security-critical system requirements are increasingly enforced through mandatory access control systems. These systems are controlled by security policies, highly sensitive system components, which emphasizes the paramount importance of formally verified security properties regarding policy correctness. For the class of safety-properties, addressing potential dynamic right proliferation, a number of known and tested formal analysis methods and tools already exist. Unfortunately, these methods need to be redesigned from scratch for each particular policy from a broad range of different application domains. In this paper, we seek to mitigate this problem by proposing a uniform formal framework, tailorable to a safety analysis algorithm for a specific application domain. We present a practical workflow, guided by model-based knowledge, that is capable of producing a meaningful formal safety definition along with an algorithm to heuristically analyze that safety. Our method is demonstrated based on security policies for the SELinux operating system. Keywords: Security engineering, security policies, access control systems, access control models, safety, heuristic analysis, SELinux.
翻译:这些系统由安全政策、高度敏感的系统组成部分控制,这些部分强调在政策正确性方面正式核查安全特性的极端重要性。对于安全财产类别,处理潜在的动态权利扩散问题,已经存在一些已知和经过测试的正式分析方法和工具。不幸的是,这些方法需要从零开始,从各种不同的应用领域对每项特定政策进行重新设计。在本文件中,我们试图通过提出一个统一的正式框架来缓解这一问题,这个框架适合特定应用领域的安全分析算法。我们提出了一个实用的工作流程,它以基于模型的知识为指导,能够产生一个有意义的正式安全定义,同时进行超自然分析的算法。我们的方法以SELinux操作系统的安全政策为基础。关键词:安保工程、安保政策、出入控制系统、出入控制模型、安全、超自然分析、SELinux。