Weaving Authentication and Authorization Requirements into the Functional Model of a System Using Z Promotion

Weaving Authentication and Authorization Requirements into the Functional Model of a System Using Z Promotion
复制标题

使用 Z 提升将身份验证和授权要求融入到系统的功能模型中

DOI:
--
复制
发表时间:
2008
期刊:
Leveraging Applications of Formal Methods
影响因子:
--
通讯作者:
A. Abdallah
A. Abdallah
中科院分区:
--
文献类型:
--
作者:
A. Haidar;A. Abdallah

文献摘要

被引文献

相似文献

Z在软件开发中的使用集中在指定系统的功能。然而,在开发安全系统时,重要的是要解决基本的安全方面,如身份验证、授权和审计。在本文中,我们提出了一种方法,从通用和模块化的安全组件,使用提升技术在Z。该方法利用Z.对于每个组件,使用Z符号来构造其基于状态的模型和相关操作。一旦引入了组件,定义的本地操作就被提升为对全局状态起作用。我们说明了这种方法的发展,一个“安全”的会议管理系统模型。通过这种方法,可以独立于安全机制来指定系统的核心功能。认证和授权被视为与功能系统仔细集成的组件。
The use of Z in software development has focused on specifying the functionality of a system. However, when developing secure system, it is important to address fundamental security aspects, such as authentication, authorization, and auditing. In this paper, we show an approach for building systems from generic and modular security components using promotion technique in Z. The approach focuses on weaving security component into the functionality of a system using promotion technique in Z. For each component, Z notation is used to construct its state-based model and the relevant operations. Once a component is introduced, the defined local operations are promoted to work on the global state. We illustrate this approach on the development of a “secure” model for a conference management system. With this approach, it is possible to specify the core functionalities of a system independently from the security mechanisms. Authentication and authorization are viewed as components which are carefully integrated with the functional system.