# HG changeset patch # User Christian Urban # Date 1371956149 -3600 # Node ID fb962189e9210a10a19eb589c14bce225575aca8 # Parent 31d3d2b3f6b0c11655b54cf21f85281cba0853d0 added reviews from ESORICS diff -r 31d3d2b3f6b0 -r fb962189e921 ESORICS-Reviews --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ESORICS-Reviews Sun Jun 23 03:55:49 2013 +0100 @@ -0,0 +1,235 @@ + +Dear Christian + +We regret to inform you that your submission to ESORICS 2013, "A Formal Model and Correctness Proof for an Access Control Policy Framework", has not been accepted. The conference was extremely competitive this year, with 43 papers out of 242 being accepted, an acceptance rate of around 18%%. + +The reviews for your paper are appended to this email. We hope you find them useful in preparing subsequent versions of your submission. + +Best wishes + + +Jason Crampton & Sushil Jajodia +Programme Co-chairs + + +----------------------- REVIEW 1 --------------------- +PAPER: 184 +TITLE: A Formal Model and Correctness Proof for an Access Control Policy Framework +AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban + + +----------- REVIEW ----------- +The paper presents a formalization of the (dynamic) model of the +Role-Compatibility (RC) model, in the interactive prover Isabelle, for +the authorization of core operations in an operating system. The +authors use the inductive approach, introduced by Paulson, for +cryptographic protocols. The formalization of the model takes into +account the dynamic behavior of the operation of an operating system. +There are two groups of rules: admissible, formalizing the conditions +under which operating system actions can be executed, and granted, +formalizing the authorization requirements. The authors develop a +static check for taintable objects. It is claimed that the rules can +be easly adapted to the access control model of SELinux. + +The English of the paper is good. I have found few typos: + +- page 4, line -8: deletion Of IPCs --> deletion of IPCs +- page 5, line 17: these function --> these functions +- page 6, line 15: the way how the --> the way the +- page 7, line 5: for the the role --> for the role +- page 9, line 10: For example staring --> For example starting +- page 10, line -6: unique process IDs --> unique process ID +- page 12, line -6: process in tainted --> process is tainted +- page 14, line -13: provisio --> proviso + +The formalisation seems to be reasonable although I would have liked +an appendix to the paper in which the formalization is reported fully. + +The static check for taintable objects of the operating system seems +to be useful and its (limited) scope of applicability is honestly +discussed. + +The effort of taking into account te dynamic of the system, not only +the authorization policies, is intersting and important to develop +more precise security analysis techniques. However, the authors +should give a better idea of what kind of properties the proposed +check can verify. For example, can they perform information flow +analysis? + +My main concern with the paper is the lack of examples on which the +various rules are shown and that the static check is not applied to a +(possibly realistic) scenario to show its usefulness. The advantages +of the proposed check are only argued abstractly. It is thus +difficult to understand the degree of automation with which the static +check can be carried out. I know that Isabelle offers a high degree +of automation to various proof attempts but the paper does not offer +hints about this crucial aspect. If the static check is not fully +automated, then the usefulness of the formal model is greatly +decreased. + +For this reason, I suggest to consider the paper as borderline. + +I have also the following comments on some aspects of the paper: + +- in Section 3, the notion of state is not precisely characterized. + One can derive that there is a given notion of initial state and + that the other state can be derived by applying to the initial state + a (finite) sequence of actions of the operating system, but I was + not able to find a place where this is explictly formalized. + +- at the end of page 5, the definition of new_proc seems to be + unnecessarely restrictive. The thing that needs to be formalized + here is the fact that the function returns a distinct identifier + w.r.t. the existing identifiers in a state. Taking the max of the + identifiers (naturals) and adding one is indeed a way to ensure this + but it is certanly not the only way. An alterantive, more general, + formalization is to assume the existence of an infinite set of + identifiers, taking out all the identifiers in the actual state, and + then pick any of the remaining identifiers. This admits as an + implementation the proposed definition of new_proc but also many + others. This seems to be important in the light of the remark at + page 14, immediately after the statement of Theorem 2, saying that + "we have no control over which process ID a process will be assigned + with." This does not seem to hold with the proposed definition of + new_proc. It does hold with the alternative definition above. + +- at the end of page 7, the notion of seeds are introduced but the + reader is left with wondering how these are identified. This is + unswered only very late in the paper. I suggest the authors to give + some hints about this issue already here and mention that it is + further discussed later in the paper. + +- at page 9, towards the end of Section 3, it is discussed that the + restriction to the (so-called) undeletable objects of the proposed + static check is needed to avoid to consider infinitely many objects + and that this is crucial to make the check effective. I am not sure + to have understood exactly what the authors really mean. One may + (automatically) reason about infinitely many objects by using + suitable constraints. It may well be the case that it is possible + to find (finitary) symbolic representations for states containing + finitely many objects (but whose exact number is unknown). This is + standard, e.g., in the infinite state model checking of parametric + systems. The authors may have a look at the following seminal paper + to have an idea of what can be done for the verification of systems + with infinite state spaces: + + @article{AbdullaTCS, + author = {P. A. Abdulla and B. Jonsson}, + title = {Model Checking of Systems with Many Identical Timed Processes}, + journal = {Theoretical Computer Science}, + vol = {290 (1)}, + pages = {241--264}, + year = 2003, + } + + I believe that this point should be clarified by the authors to put + their verification technique in the right relationship with others. + + A similar observation can be done for the following sentence at the + end of page 10: "otherwise exploring all possible "reachable" + objects can lead to the potential infinity like in the dynamic + model." Indeed, there can be several sources of infinity in a + problem that, as shown for example by the paper by Adbulla and + Jonsson paper above, can be tamed and an exhaustive reachability + analysis can be done. + + +----------------------- REVIEW 2 --------------------- +PAPER: 184 +TITLE: A Formal Model and Correctness Proof for an Access Control Policy Framework +AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban + + +----------- REVIEW ----------- +This work presents a specification of the role-compatibility (RC) model in the +Isabelle theorem prover. RC is a role-based access control model created for use +in Rule Set Based Access Control (RSBAC), an access control kernel module that +provides implementations of mandatory, role-based, and access control-list +models of access control for Linux. The model is to be used to detect the spread +of "taintable" resources. The initial state of the system is assumed to contain +some "seeds" (tainted files), which may then spread through the system. The +static check, then, is whether a particular resource (e.g., the root of the +filesystem) is taintable. The tainted^s relation +(a static formulation of the taintable relation) is defined and proven to be +sound and complete with respect to the work's notion of taintable. + +The authors claim that their approach is more accurate than policy analysis, +since it takes into account additional details of the operating system, such as +the processes that are started. This allows their approach to avoid the +"over-approximations" of policy analysis (e.g., when a process assuming a +particular role could cause a violation, but such a process is never created). +These added details, however, seem at times to be based more on the authors' +intuition than any particular implementation. For example: +- A newly created process is assigned the ID: $\Max(current_ids) + 1$. Linux + (where RC is currently implemented) uses $next_id++ % MAX_ID$ [unless taken] + (i.e., it maintains a counter which is incremented when an ID is assigned, so + cloning and terminating repeatedly still increases the counter rather than + creating the same ID every time). +- The set of users is assumed to be fixed (not a requirement in RSBAC or Linux). + +Thus, the model is more all-encompassing than some approaches to policy analysis +due to modeling these details at all, but it falls short of verifying any +particular implementation since these details are not justified. The work is +poorly positioned among related work, as the authors seem unaware of the huge +body of work on various techniques in access control static analysis [e.g., +1--3], especially work that also models the system at the process level [3]. + +The methods for specifying the model are not claimed to be novel, and are a +somewhat straightforward and unsurprising application of Paulson's inductive +method. The authors say their approach can be easily applied to other access +control models, but this seems more as a result of the approach being obvious +than of it being particularly reusable. Furthermore, the authors do not +demonstrate how a practical analysis would be carried out using this model; +instead, they briefly discuss the way they they imagine it being used and the +(uncited) reasons they believe the model's assumptions (only checking +undeletable files for taintedness, the existence of a set of known "seed" files +that are tainted in the initial state) are not too restrictive for it to be +usable in practice. + +The work's main claimed contribution is the formalization of RC in Isabelle. The +specification the authors present does not use novel techniques that can be +reapplied elsewhere and is not shown to have a practical advantage over existing +analysis techniques for role-based access control models. We question, +therefore, whether this formalization alone is a sufficient contribution to +warrant acceptance to a top venue such as ESORICS. + +[1] Mikhail I. Gofman, Ruiqi Luo, Ayla C. Solomon, Yingbin Zhang, Ping Yang, +Scott D. Stoller: RBAC-PAT: A Policy Analysis Tool for Role Based Access +Control. TACAS 2009:46--49. + +[2] Scott D. Stoller, Ping Yang, C. R. Ramakrishnan, Mikhail I. Gofman: +Efficient policy analysis for administrative role based access control. ACM +Conference on Computer and Communications Security 2007:445--455. + +[3] Arosha K. Bandara, Emil Lupu, Alessandra Russo: Using Event Calculus to +Formalise Policy Specification and Analysis. POLICY 2003. + + +----------------------- REVIEW 3 --------------------- +PAPER: 184 +TITLE: A Formal Model and Correctness Proof for an Access Control Policy Framework +AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban + + +----------- REVIEW ----------- +This paper focuses on the previously published framework, Role-Compatibility Model (RC-model). Their static analysis discovers semantic inconsistencies of RC-model. In particular, they indicate InheritParentRole of RC-model. Their approach seems reasonable but this work is to determine the correctness of RC-model. Instead, it would be interesting if they analyze NIST RBAC model with their approach. Since RC-model itself is not formally designed, it is hard to judge how novel their analysis work is. In addition, they claim access control policy framework is formulated but it is hard to determine how their examples are related to role-based access control policies. The authors need to use generic RBAC-centric examples if their goal is to show their approach can be adapted for other RBAC models. + +Even though they briefly address their experiments in the conclusion, it is questionable how the formulated model can support real-world RBAC policies due to the lack of details on their experiment and proofs. Also, the references should be improved including logic-based reasoning of access control policies. Here are several papers that the authors need to consider: + +Elisa Bertino, Barbara Catania, Elena Ferrari, and Paolo Perlasca. A logical framework for reasoning about access control models. ACM Trans. Inf. Syst. Secur, 6:71–127, 2003. + +J. Bryans. Reasoning about XACML policies using CSP. In Proceedings of the 2005 workshop on Secure web services, page 35. ACM, 2005. + +K. Fisler, S. Krishnamurthi, L.A. Meyerovich, and M.C. Tschantz. Verification and changeimpact analysis of access control policies. In Proceedings of the 27th international conference on Software engineering, pages 196–205. ACM New York, NY, USA, 2005. + +V. Kolovski, J. Hendler, and B. Parsia. Analyzing web access control policies. In Proceedings of the 16th international conference on World Wide Web, page 686. ACM, 2007. + +Joseph Y. Halpern and Vicky Weissman. Using first-order logic to reason about policies. ACM Trans. Inf. Syst. Secur., 11(4), 2008. + +Prathima Rao, Dan Lin, Elisa Bertino, Ninghui Li, Jorge Lobo: EXAM: An Environment for Access Control Policy Analysis and Management. POLICY 2008: 238-240 + +Alessandro Armando, Enrico Giunchiglia, and Serena Elisa Ponta. Formal specification and automatic analysis of business processes under authorization constraints: an action-based approach. In Proceedings of the 6th International Conference on Trust, Privacy and Security in Digital Business (TrustBus’09), 2009. + +G. Ahn, Hongxin Hu, Joohyung Lee, and Yunsong Meng. Reasoning about XACML policy descriptions in answer set programming (preliminary report). In Proceedings of International Workshop on Nonmonotonic Reasoning (NMR), 2010. + +G. Ahn, Hongxin Hu, Joohyung Lee, and Yunsong Meng. Representing and reasoning about web access control policies. In Proc. 34th Annual IEEE Computer Software and Applications Conference (COMPSAC 2010), pages 137–146, 2010.