| Security model, which aims at improving understanding of security requirement realization, precisely describe main aspects of security and its relationship with system action. Security policy plays an important role in confirming the content of security model. Therefore successfully developing a perfect security model needs clear and comprehensive policies. In particular, the composition of systems must consistently assure security policies that are supposed to enforce. However, there is currently no rigorous and systematic way to predict and assure such critical properties in security system design.This paper starts at information system and network security, and focuses on formal developing method of security system and security model. First, after analyzing deeply current security model, policy-based information security model is educed. In formal description, proper mathematics methods are usually needed to insure precise description and analysis. Second, a methodoly, which aims at modeling security architecture and verifying whether required security constraints are assured by the composition of the components, is introduced in this paper. Through the concept of security constraint patterns, the generic form of security policies are formally specified that the system architecture must enforce. Then, temporal logic and Petri net are applied to describe and verify access control in policy-based security model. TL, as a popular descriptive formalism, is best suited for describing rules and constraints. By contrast, Petri net is a well-known operational model well suited for modeling the control and composition of distributed system. Last, the resultant architectural model is verified against the systemwide security constraint patterns using Petri net's analysis techniques--reachabilityanalysis, which not only ensures the integrity of early design decisions, but also provides a framework to guide correct implementations of the security system design.
|
PDF Full Text Request