Dear ChristianWe 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 wishesJason Crampton & Sushil JajodiaProgramme Co-chairs----------------------- REVIEW 1 ---------------------PAPER: 184TITLE: A Formal Model and Correctness Proof for an Access Control Policy FrameworkAUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban----------- REVIEW -----------The paper presents a formalization of the (dynamic) model of theRole-Compatibility (RC) model, in the interactive prover Isabelle, forthe authorization of core operations in an operating system. Theauthors use the inductive approach, introduced by Paulson, forcryptographic protocols. The formalization of the model takes intoaccount the dynamic behavior of the operation of an operating system.There are two groups of rules: admissible, formalizing the conditionsunder which operating system actions can be executed, and granted,formalizing the authorization requirements. The authors develop astatic check for taintable objects. It is claimed that the rules canbe 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 --> provisoThe formalisation seems to be reasonable although I would have likedan appendix to the paper in which the formalization is reported fully.The static check for taintable objects of the operating system seemsto be useful and its (limited) scope of applicability is honestlydiscussed.The effort of taking into account te dynamic of the system, not onlythe authorization policies, is intersting and important to developmore precise security analysis techniques. However, the authorsshould give a better idea of what kind of properties the proposedcheck can verify. For example, can they perform information flowanalysis? My main concern with the paper is the lack of examples on which thevarious rules are shown and that the static check is not applied to a(possibly realistic) scenario to show its usefulness. The advantagesof the proposed check are only argued abstractly. It is thusdifficult to understand the degree of automation with which the staticcheck can be carried out. I know that Isabelle offers a high degreeof automation to various proof attempts but the paper does not offerhints about this crucial aspect. If the static check is not fullyautomated, then the usefulness of the formal model is greatlydecreased. 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: 184TITLE: A Formal Model and Correctness Proof for an Access Control Policy FrameworkAUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban----------- REVIEW -----------This work presents a specification of the role-compatibility (RC) model in theIsabelle theorem prover. RC is a role-based access control model created for usein Rule Set Based Access Control (RSBAC), an access control kernel module thatprovides implementations of mandatory, role-based, and access control-listmodels of access control for Linux. The model is to be used to detect the spreadof "taintable" resources. The initial state of the system is assumed to containsome "seeds" (tainted files), which may then spread through the system. Thestatic check, then, is whether a particular resource (e.g., the root of thefilesystem) is taintable. The tainted^s relation(a static formulation of the taintable relation) is defined and proven to besound 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 asthe processes that are started. This allows their approach to avoid the"over-approximations" of policy analysis (e.g., when a process assuming aparticular 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 analysisdue to modeling these details at all, but it falls short of verifying anyparticular implementation since these details are not justified. The work ispoorly positioned among related work, as the authors seem unaware of the hugebody 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 asomewhat straightforward and unsurprising application of Paulson's inductivemethod. The authors say their approach can be easily applied to other accesscontrol models, but this seems more as a result of the approach being obviousthan of it being particularly reusable. Furthermore, the authors do notdemonstrate 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 checkingundeletable files for taintedness, the existence of a set of known "seed" filesthat are tainted in the initial state) are not too restrictive for it to beusable in practice.The work's main claimed contribution is the formalization of RC in Isabelle. Thespecification the authors present does not use novel techniques that can bereapplied elsewhere and is not shown to have a practical advantage over existinganalysis techniques for role-based access control models. We question,therefore, whether this formalization alone is a sufficient contribution towarrant 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 AccessControl. 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. ACMConference on Computer and Communications Security 2007:445--455.[3] Arosha K. Bandara, Emil Lupu, Alessandra Russo: Using Event Calculus toFormalise Policy Specification and Analysis. POLICY 2003.----------------------- REVIEW 3 ---------------------PAPER: 184TITLE: A Formal Model and Correctness Proof for an Access Control Policy FrameworkAUTHORS: 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-240Alessandro 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.