On the Decidability of the Safety Problem for Access Control Policies
Contents
1. ou c yl rF y z y 0 76 OVO OAG O gt Ax d Yx O where x y are drawn from some set of variables and a is an access right To save ourselves exploring cases we consider that x y is x y OAV is AdV ay and w is nao Vw We will sometime refer to formulas where variables have been instantiated with actual object names i e the formula might have atomic propositions of the form o o or 0 0 a for 0 o When there are no quantifiers and all variables have been instantiated with object names we call it a propositional formula Remember these are not formulas in SATL For a finite non empty sequence of states 7 O1 M1 On Mn we say 7 is a path of P if O1 M1 gt gt On Mn We write n where i 1 n for the suffix of 7 starting at position i i e m O M On Mn We write fo where o O1 for the longest prefix of m possibly all of 7 which has o O for every state Oj M4 in the prefix Satisfaction between a sequence of states m and a formula is defined in Fig 2 The notation denotes a formula with all free occurences of x replaced by o In this way when satisfaction is applied to closed formulas all variables will have been substituted with actual objects by the time they are evaluated hence satisfaction finds object names o o in atomic propositions rather than variables Note that quantifiers range over currently existing object2. Motivation An access control system is a mechanism which regulates the rights of a set of users to gain access e g to read or write to some resources e g secret files This is done according to an access control policy a set of rules which indicates in which circumstances a particular user may obtain a particular permission to a particular resource These policies can be large and dynamic for example they might be updated every time a user or resource is created or deleted For these reasons it is generally 1 Email eldar kleiner comlab ox ac uk 2 Email tom newcomb comlab ox ac uk 1571 0661 see front matter 2007 Elsevier B V All rights reserved doi 10 1016 j entcs 2007 05 032 108 E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 not clear exactly which behaviours a policy permits at any given time and whether the policy does in fact implement some desired security specification For example a system administrator would want to be sure that the policy rules do not interact in any way which allows unrestricted users to gain access to restricted resources There is therefore a need for automated tools that help an administrator assess the impact of an access control policy on the security of his system The Problem In the seminal paper by Harrison Ruzzo and Ullman 7 a formal model of access control was presented which has become known as HRU A state of an HRU system
3. the infinite set of objects to a finite set of objects the size of which depends on the maximum number of such objects that might be required for any single transition This idea suggests that we compute transitions on the abstract state space by computing concrete transitions on a reduced state space C UC x C U C x A Here C is a subset of X C of size m where m is the the greatest number of formal object parameters in any one command i e the most objects that can be involved in any one transition To make this more formal we define a translation from abstract states to con crete states Q 0 M O2DC OCCUC MCOxOxA Mn CxC x A Q We define a transition to exist between two abstract states Q and Q exactly when there is some concrete transition from any state in y Q to any state in 7 Q This is computable because it deals only with finite structures This allows us to talk about abstract traces Q1 gt gt Qn To relate the abstract and concrete systems we say that each path 01 M1 gt On Mn of PIC i e a path of P with O D C for all i 1 n implies a concrete trace a 01 M1 gt a O Mn We will show that the two systems have equivalent traces 4 Proposition 4 4 All concrete traces are abstract traces Proof We show this by proving O1 M O2 M2 implies a 01 M gt a O2 M2 and the result follows by induction Suppose the command c that ge
4. 1 Employee Information System The company s policy states that directors can give out bonuses This is ex pressed in Fig 1 by the command c x y where a director x signals that he s awarded a bonus to an employee y The command c2 z y shows that directors can also remove bonuses they have awarded Similarly c3 a y and c4 x y dictate that a manager may give or take bonuses to any employee who isn t a manager or a director Commands c5 x y and ce x y say that a director can demote from or promote to manager The original example in 22 included the ability for an employee x to appoint another employee y as his advocate We omit this for simplicity but could easily 112 E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 trH o 0 iff o 0 m H 0 0 a iff 0 0 a Mi t no iff not mE TE OVY iff rE gortTEYD t H Az d iff there exists some o O such that mlo z T H Vad iff for all o O we have rto H z t H oog iff for alli 1 n we have qt H Fig 2 Satisfaction model it by setting a permission x y Advocate A feature not permitted in 22 but allowed in our framework is the ability to let the set of existing objects grow and shrink Commands c7 x y and cg x y expresses that managers may hire and fire employees 3 Safety Access Temporal Logic The formulas of Safety Access Temporal Logic SATL are
5. a should ever be granted between two objects 4 Universal SATL We define Universal SATL as the fragment of SATL which only contains the quan tifier Y which may only occur at the outermost level i e formulas of the form Va1 y where is quantifier free After looking at an example we will prove some propositions about our framework with the eventual goal of showing that the model checking problem for Universal SATL is decidable Example 4 1 The manager conspiracy scenario problem considered in 22 was Can two managers conspire such that one of them gives a bonus to the other We can express that the scenario is not possible in Universal SATL with the formula Va y x x Manager A y y Manager A a y Bonus A 7 y x Bonus x y Bonus V y x Bonus Our semantics for access control systems exhibits data independence 20 or parametric polymorphism with respect to the type of objects X This is because the only operation we assume on this type is equality testing This induces a symmetry on objects which implies a bisimilarity on the transition system Proposition 4 2 For all states O M and O M and for all bijections o on we have O M O M iff o O M o O M where o is lifted to states in the obvious way 114 E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 Proof Straightforward from the
6. in CSP The CSP models we use are to some extent similar Both these works reason only about bounded systems They are therefore usable only for finding flaws and cannot provide general proofs of safety Our result shows that RW formulas with only existential quantification can be checked on unbounded systems Future Work In practice it is often not possible to prove security requirements like the ones we consider without also assuming that the system can never enter some inconsistent state In such cases one would like to strengthen the check by specifying that for example there is never more than one administrator or every file always has a unique owner Universal SATL is unable to express these E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 119 invariants but we are currently preparing decidability results about larger fragments of SATL containing formulas like Yri n A INV gt O A INV where INV expresses a desired global invariant of the system via restricted use of quantifiers The results presented in this paper were possible thanks to the fact that the model is data independent with respect to the type of objects This observation allowed us to use techniques developed for data independent systems with arrays 10 14 and apply them to access control matrices There are other results about array systems that we believe can be leveraged to
7. is denoted by a set of objects some of which are subjects and a protection matrix giving the current access rights between pairs of subjects and objects A policy is a set of commands each parameterised by objects and specifying some possible transformation on the access matrix Their language is able to express naturally the behaviour of real world access control systems e g UNIX They considered the following safety problem given a set of policy rules a generic access right a and an initial matrix is it possible to reach a state in which a is granted to any subject They then showed that this problem is undecidable using an encoding of a Turing machine tape into the matrix Attempted solutions Since then research has concentrated on finding re stricted models for which this problem is decidable with minimum diminution of expressive power For example insisting that each command is mono operational 7 may only perform one single action e g it may create an object or grant an access right but cannot do both in the same atomic step or mono conditional 6 the enabling condition for each command is a single cell of the access matrix In 18 Sandhu and Suri introduced the non monotonic transformations model which is subsumed by 13 s condition that allows object creation but forbids the creation of new subjects Koch et al 9 analysed a similar restriction of their graph based access control framework Our observation Alt
8. set of formal parameters z 1 n i e symbols which denote objects by which a command is parameterised An instance of a command replaces each formal parameter in the command with a distinct object from We now formally specify the transition relation induced by an access control policy P over states as follows O M O M iff there exists some instance c of a command in the policy such that all of the following hold i The command is applicable Con UGog COXO x A Conditional permissions fall within the scope of the current state Cereate N O RE Objects to be created do not already exist Garant U Ctake C O x O x A where O O U Cereate Permissions to be altered exist after Cereate has been applied Cdestroy e OF Objects to be destroyed exist after Cereate has been applied ii The guard of the command is met e Con C M e cp IM 3 The distinct restriction does not affect expressiveness If one wanted to allow that two parameters mentioned in a command could represent the same object one would add a similar command in which the two formal parameter names are identified E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 111 iii The next state predicates are satisfied O O U Coreate Cdestroy e M M U Cgrant Crake N O x O x A Observe that a newly created object has no permissions associated with i
9. 05 pp 474 514 Lipton R and L Snyder On synchronization and security in A J R DeMillo D Dobkin and R Lipton editors Foundations of Secure Computation Academic Press 1978 pp 367 385 Newcomb T Model Checking Data Independent Systems With Arrays Ph D thesis Oxford University Computing Laboratory 2003 Roscoe A The Theory and Practice of Concurrency Prentice Hall 1998 Roscoe A and R Lazi What can you decide about resetable arrays in Proceedings of the 2nd International Workshop on Verification and Computational Logic VCL 2001 Technical Report DSSE TR 2001 8 pages 5 23 2001 pp 5 23 Ryan P S Schneider M Goldsmith G Lowe and A Roscoe Modelling and analysis of security protocols 2001 Sandhu R and G Suri Non monotonic transformation of access rights in Proceedings of the IEEE Symposium on Security and Privacy 1992 pp 148 163 Vardi M and P Wolper An automata theoretic approach to automatic program verification preliminary report in Proc 1st Annual IEEE Symposium on Logic in Computer Science Washington DC 1986 pp 332 344 Wolper P and V Lovinfosse Verifying properties of large sets of processes with network invariants in Automatic Verification Methods for Finite State Systems Lecture Notes in Computer Science 407 1989 pp 68 80 Zhang N M Ryan and D Guelev Synthesising verified access control systems in XACML in FMSE 04 Pro
10. Available online at www sciencedirect com ScienceDirect ois Science Jeet A ELSEVIER Electronic Notes in Theoretical Computer Science 185 2007 107 120 www elsevier com locate entcs On the Decidability of the Safety Problem for Access Control Policies E Kleiner Oxford University Computing Laboratory Ozford OX1 83QD UK T Newcomb Ozford University Computing Laboratory Ozford OX1 83QD UK Abstract An access control system regulates the rights of users to gain access to resources in accordance with a specified policy The rules in this policy may interact in a way that is not obvious via human inspection there is therefore a need for automated verification techniques that can check whether a policy does indeed implement some desired security requirement Thirty years ago a formalisation of access control presented a model and a safety specification for which satisfaction is undecidable Subsequent research aimed at finding restricted versions that obtain the decid ability of this problem yielded models without satisfactory expressive power for practical systems Instead of restricting the model we reexamine the safety specification We develop a new logic that can express a wide variety of safety properties over access control systems and show that model checking is decidable for a useful fragment of this logic Keywords Access control model checking temporal logic CSP 1 Introduction
11. analyse access control policies in particular results about arrays with reset 16 11 Writing CSP scripts for analysing access control polices manually might be te dious and error prone We therefore intend to develop a compiler which will produce CSP scripts from a more abstract description We are also interested in RBAC role based access control which are Turing complete 3 We believe our decidability results can be extended to model some RBAC polices in which the system is limited to a fixed number of roles but unre stricted otherwise Lastly we hope that our results can shed more light on verification of Trust Management systems 1 The results we present here together with knowledge gained in the security protocols field 17 can be combined in order to reason about such systems and hopefully strengthen existing decidability results 12 References 1 Blaze M J Feigenbaum and J Lacy Decentralized trust management in Proceedings of the IEEE Symposium on Research in Security and Privacy 1996 pp 1081 6011 2 Bryans J Reasoning about XACML policies using CSP Technical Report CS TR 924 University of Newcastle 2005 3 Crampton J Authorization and antichains Ph D thesis Birkbeck University of London London England 2002 4 Formal Systems Europe Ltd Failures Divergence Refinement FDR2 User Manual 1999 URL http www fsel com 5 Guelev D M Ryan and P Y Schobbens Model che
12. ceedings of the 2004 ACM workshop on Formal methods in security engineering 2004 pp 56 65 Zhang N M Ryan and D Guelev Evaluating access control policies through model checking in ISC 2005 pp 446 460
13. cking access control policies in ISC 2004 pp 219 230 6 Harrison M and W Ruzzo Monotonic protection systems in A J R DeMillo D Dobkin and R Lipton editors Foundations of Secure Computation Academic Press 1978 pp 337 363 7 Harrison M W Ruzzo and J Ullman Protection in operating systems Communications of the ACM 1976 8 Kleiner E and T Newcomb Using CSP to decide safety problems for access control policies Technical Gdo RR 06 04 Oxford University Computing Laboratory Parks Road Oxford OX1 3QD UK 2006 9 Koch M L Mancini and F Parisi Presicce Decidability of safety in graph based models for access control in ESORICS 02 Proceedings of the 7th European Symposium on Research in Computer Security 2002 pp 229 243 120 10 11 12 13 14 15 16 17 18 19 20 21 22 E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 Lazi R T Newcomb and A Roscoe On model checking data independent systems with arrays without reset Theory and Practice of Logic Programming Special Issue on Verification and Computational Logic 4 2004 Lazi R T Newcomb and A Roscoe Polymorphic systems with arrays 2 counter machines and multiset rewriting in Proceedings of INFINITY 2004 pp 3 19 Li N J Mitchell and W Winsborough Beyond proof of compliance security analysis in trust management J ACM 52 20
14. definition of We now reduce the problem involving a Universal SATL formula to a set of problems involving propositional SATL formulas This allows us to henceforth re strict our attention to a single propositional formula involving object constants from a finite set C C X and paths of the system that have objects C in continual existence Proposition 4 3 The model checking problem P V21 n is equivalent to the conjunction of a finite number of model checking problems of the form P C 4 where wW is a propositional formula referring only to objects in a finite set C Proof Take any n distinct objects C 01 0 We show that it is sufficient to consider the V quantifier ranging over this finite set thus reducing the first order problem to a finite set of propositional problems We can temporarily invent notation and write PEV21 0n 0 iff PEV211 C n CO Proving the forward direction is trivial The backwards direction can be proved as follows Take any path r of P and any objects o 0 as instances for 1 2n By Proposition 4 2 we know that for every bijection oz is also a path of P so we find such a that maps each o into C Assuming the right hand side we know that om j 7177 v1 0n Apply structural induction on to deduce T H 2109 ar a Finally notice that P Va C n C is equivalent to PIC H Vay C n C Q because Y only inspects paths where i
15. e structures using union to form a state using Q to fill in the C x C x A part The reader might notice that there are parts of the matrices in the final trace which are always blank e g 01C x gC x A they do not directly correspond to any information that could be extracted from states S and 9S While there is some freedom about what values these permissions can have it is safest to set all these permissions off This is because if one of these o o C objects is destroyed we would need o0 0 a and 0 0 a to be off in subsequent states for all objects o Conversely if one was created we d need these permissions to be off in previous states Contrast this with destroying objects in C discussed below 5 We cannot call these states as we do not necessarily have M C O x O x A E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 117 It can be seen readily from the definition that a O M Q It remains to show that Qi D151 D O riS D aiGi iSi O BOn 1Gn 1 ci CUaC Qit1 Dosi DiS oS TiSi D D On 1S8n 1 Because of the underlined terms this can be deduced from S S by checking the cases in the definition of Notice that no o C ever appears in the destroy field of a command instance because the resulting state would not have an abstraction This is important because otherwise we would require all permissions in the row and column o
16. f that object to be off in the subsequent state which is not guaranteed by our definition of Oj41 Mi 1 Otherwise the proof is straightforward We now want to show that the trace equivalence between the abstract and concrete systems means that checking the abstract system will give us the same results as checking the concrete system Note first that satisfaction can be applied to traces as well as paths Proposition 4 6 The abstract and concrete systems are indistinguishable by any propositional formula mentioning only objects in C Proof Observe that checking an atomic proposition used in on a concrete state returns the same truth value as checking it on the representative abstract state This means that checking on a path returns the same truth value as checking on the associated trace The result now follows from the trace equivalence of the abstract and concrete systems Propositions 4 4 and 4 5 Theorem 4 7 Model checking for Universal SATL is decidable i e there exists a procedure that given an access control policy P and a closed Universal SATL formula answers whether P Proof Proposition 4 3 means we can instead consider the model checking problem PIC amp for a propositional formula mentioning only objects in the finite set C By Proposition 4 6 we can check the finite computable abstract system using traditional model checking algorithms for linear temporal logic 19 to deduce
17. hough all these models obtain decidability of the HRU safety problem unfortunately none of them is powerful enough to fully express many practical systems This is because they gain decidability by placing restrictions on the type of policies that can be considered We instead reexamine the original problem in 7 One source of undecidability is that the safety question is a property of an access control policy plus an initial matrix It asks questions that always begin From a given initial state is it pos sible We believe that initial states are not so important when assessing the security of a policy More common questions administrators ask about their access control systems are If a user doesn t have permission a can he somehow obtain permission b and From any state with at least three users can some user x grant a permission to some user y In other words they tend to implicitly assume the system is already up and running Also answering these questions can be viewed as answering the HRU safety problem for a whole range of initial states For example if we show that any user E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 109 without right a cannot obtain right b and if we know that the initial state of our access control system does not have a granted to any user then we know that the system does not allow users to obtain right b This paper We present a protecti
18. i41 We call the command instance that creates this transition c C U C to highlight that it is instantiated only with objects from C UC Our aim is to show that there is a concrete trace 01 Mi ioe On Mn with Oi Mi E Qi for each i In a reversal of the previous construction we map the objects in C back out into the whole of and we want to do this in such a way that each new command instance uses objects that do not overlap with those used by any other new command instance in the path We therefore require a different injection g C X C for each command c C U C which we use to form a new sequence of commands c1 CUa1C Cn 1 CUon 1C 01 M O2 M2 On Mn We need to set up each state O M in the trace in such a way that it captures the initial conditions on objects o C expected by each command C Uo C yet to be executed we obtain these values from the states 5 and the final conditions on objects o C expected by each command already executed we obtain these values from the states S This can be done because the injections g do not overlap so the proposed states are Oi Mi Qi B 01S o4 1S _1 D 49 On 1Sy 1 Above each injection a applies to objects outside of C and permissions which are not just between C so oS returns a structure O M with ONC Mn C x C x A and M C CUC x CUC x A The operator combines thes
19. ically simpler because we group atomic series of commands into single actions We introduce a temporal logic that is able to express a wide range of safety properties over such models The model checking problem for the entire logic is undecidable but we believe this provides a framework for investigating what kinds of useful safety problems can be decided for access control policies This paper makes a significant start on that investigation We present a frag ment of this logic that is able to pose practical questions about access control policies such as those suggested above another example is If there are at least three un privileged users and one administrator can the users conspire so that one of them is elevated into a privileged state We show that there exists an algorithm for the model checking problem over this fragment and have built a proof of concept implementation As remarked above this result also provides a procedure for checking the HRU safety problem for certain sets of initial states This can be turned into an incom plete but sound procedure for checking the original HRU safety problem i e for a single specified initial state by attempting to find a set of initial states containing the specified state which is expressible in Universal SATL and for which the check succeeds Organisation In Section 2 we present our formal model of access control In Section 3 we introduce our temporal logic SATL and demonstrate
20. nerated the transition 01 M1 O2 M2 was instantiated with objects C U D C X where D is some set of objects disjoint from C Let o be any injection from C U D to C U C which preserves C We know such an injection exists because D lt m C We lift this injection to states as follows o O M o 0 o O and o domo o 01 o 02 a 01 02 a M and 01 02 domo It now follows that o 01 M1 o O2 M2 using the same command c except we instantiate with objects CUC instead of CUD This can be seen from the definition of by detailing cases It can be seen also by the more informal observation that c only removes objects which are not inspected updated by the command instance and renames other objects uniformly We also have o O M y a O M for i 1 2 as required 4 They are not bisimilar a stronger equivalence between transition systems For example an abstract system might have an infinitely long behaviour which destroys an infinite number of objects this could never happen in any concrete system 116 E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 Proposition 4 5 All abstract traces are concrete traces Proof Now let s suppose we have a sequence of abstract transitions Q1 gt gt Qn We know that each transition exists because there is a concrete transition from some state S 7 Q to some state S 7 Q
21. on matrix model of access control similar to HRU Policy rules are expressed as parameterised commands that provided some specified permissions meet some precondition may create destroy objects and grant take permissions We then introduce a first order linear temporal logic which is interpreted over finite runs of the access control system The logic can quantify over all currently existing objects and possesses the temporal operator always The atomic proposi tions can make assertions about the state of particular permissions on the quantified variables or equality relationships between the variables We call this logic Safety Access Temporal Logic SATL because it can express a variety of safety properties over access control systems The model checking problem for the whole logic is undecidable because it can express the HRU safety problem 7 However we show that the problem is decidable for a fragment of the logic which we call Universal SATL Formulas in this fragment only have quantifiers Y which may only appear at the outermost level We have a prototype implementation of the finite abstract model used in the proof of decidability It is written in CSP 15 for use in the model checker FDR 4 We also give an example to illustrate the effectiveness of our approach Contributions We describe a model of access control which is more expressive than that given in 7 because we allow testing for the absence of permissions but techn
22. owing about the Employee Information System regardless of the number of employees if directors cannot demote managers then it is not possible for two managers to conspire so that one of them awards the other a bonus 6 Conclusions Summary We have introduced a first order temporal logic for a protection matrix model of access control Although the model checking problem for the whole logic is undecidable we have identified a useful fragment of the logic for which the problem is decidable This allows us to check practical requirements of such systems without having to restrict the policy language We described how the HRU safety problem can be reduced to our decidable problem in some cases We have also built a prototype implementation of the model checking procedure Related Work Guelev Ryan and Schobbens 5 presented the RW formalism based on propositional logic for expressing access control policies and queries The paper also presents an algorithm implemented in Prolog for calculating the ability of a fixed number of agents to achieve a certain goal in the presence of a fixed number of resources In addition a tool was provided which takes an RW script as input and converts the policy description into XACML 21 Universal SATL can be compared to RW formulas which only use existential quantification Another related work is 2 where it is shown how access control mechanisms with a bounded number of subjects and resources can be expressed
23. s only and their tem poral scope is restricted to the lifetime of the selected object This is necessary to prevent the logic from being able to test properties of objects that do not exist E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 113 but produces a quirk of this logic quantifiers do not distribute over the temporal operator e g in general Vx 0 4 OV a We say that a formula satisfies a policy P written P when every path of P satisfies The model checking problem for some fragment of SATL is the following given any formula from the logic and any policy P does P H We will also require the notation P C which means all paths of P that have all objects in the set C in continual existence satisfy The model checking problem for the whole of SATL is undecidable This is because we are able to express the HRU safety problem which is shown in 7 to be reducible to the halting problem for Turing machines The HRU safety problems asks assuming a single fixed initial state can a certain access right be eventually granted We express such problems using a SATL formula Vz En Wl Cinta OE VV Tn gt O Yy y2 7 y1 y2 Here w expresses the exact state of the permissions between x variables in the initial state and the Vy clause says that initially there are no other objects The O clause asserts that no right
24. t by default but the command may specify permissions to grant to the object in Cgran Observe also that we do not include any initial state in the transition system We take the view that a policy in fact has many possible initial states and we allow the policy designer to specify constraints or assumptions about initial states within our logic Our formalisation of access control differs from HRU in some ways that we hope simplifies our model We make no distinction between subjects and objects by giving a permission 0 0 Subject to objects o that should be regarded as subjects one can generate the same expressive power We also collect together all the sequen tial primitive operations that make up an atomic command in HRU and assume a command is a single structure that specifies the total effect Finally as it creates no extra technical overhead we also allow commands to be enabled by permissions being off as well as on Example 2 1 We reproduce an example given in 22 called the Employee Informa tion System It features the employees of a company some of whom are managers and or directors and may award bonuses to other employees We will use access rights Manager Director and Bonus a Se ee ee a B EC e a E enem _ x aan ae x Manager Eee mens ae y Bonus ae Y Dircon S _ ae ean evn E viysManager x y x y y Manager a a zeal E a E ae z y lz x anase S Manager y y Director Fig
25. the truth of on the concrete system P C 5 Automation We can model the abstraction described in the proof of Theorem 4 7 in the process algebra CSP 15 The CSP events represent commands instantiated by objects from CUC We model each permission in C U C x C U C x A as a separate process each able to accept events if they meet the precondition of the associated command and change state if appropriate Processes representing permissions outside of C x C x A do not retain state but remain in a permanent nondeterministic state in accordance with y All these permissions are then combined using the CSP parallel 118 E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 operator and the refinement checker FDR 4 can be used to explore which states are reachable More details are provided in 8 Example 5 1 We complete our running example of the Employee Information Sys tem We set C oz 0 to represent the two managers mentioned in the spec ification formula and C 01 0 because the maximum number of parameters in any one command is two The abstraction was coded in CSP and checked using the refinement checker FDR It gave a counter example ce 01 Ox 3 Oy Oz We interpret this as the scenario where some director o demotes oy then oy can give a bonus to oz Removing cg from the system gives us a check that succeeds Using our theorem this proves the foll
26. the undecidability 110 E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 of the model checking problem for the whole logic This problem is shown to be decidable over the fragment Universal SATL in Section 4 In Section 5 we briefly describe our implementation Conclusions related work and future work are presented in Section 6 2 lt A Model for Access Control We assume an infinite universe of objects and a finite set of access rights A A state is a pair O M where O is a finite subset of and represents the set of currently existing objects and M is a subset of O x O x A representing the permissions which are currently granted For example a permission Frank passwd x represents whether object Frank has access right x to object passwd and might model whether a user called Frank is able to execute a program that changes his password An access control policy P is a finite set of commands where a command c 1 n is a 6 tuple of finite sets Coes Coff Ccreate Cgrants Ctake Cdestroy Intuitively the first two components represent the precondition of the command permissions that must be on and off and the last four components represent the atomic action of the command objects to create permissions to grant and take and objects to destroy More formally each of Con Coff Cgrant Ctake are subsets of F x F x A and Cereate Cdestroy are subsets of F Here F is the
27. ts instance object is in contin ual existence To check the propositional formula on the system we employ an abstract tran sition system where an abstract state records only relationships between the finite set of objects C thus an abstract state is a subset of C x C x A and represents any concrete state containing that exact relationship between the objects in C Pre cisely we use an abstraction function which takes a state O M with O D C and maps it to a O M Mn CxCx A Note that this mapping is not total states that do not have all objects C in existence do not have abstractions We need a notion of transitions on our abstract systems The usual require ment is that an abstract transition exists exactly when there is some corresponding concrete transition This is not desirable as a definition because it is not directly computable each abstract state represents an infinite number of concrete states and we cannot check them all Instead we use the following observation Because our abstract states record no information about objects outside of C and because our systems are data in dependent with respect to objects we can consider all objects outside of C to be homogeneous Furthermore each command only inspects and or changes a finite E Kleiner T Newcomb Electronic Notes in Theoretical Computer Science 185 2007 107 120 115 number of objects In a manner similar to 14 this allows us to collapse
Download Pdf Manuals
Related Search