1 

     2 Dear Christian

     3 

     4 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%%.

     5 

     6 The reviews for your paper are appended to this email.  We hope you find them useful in preparing subsequent versions of your submission.

     7 

     8 Best wishes

     9 

    10 

    11 Jason Crampton & Sushil Jajodia

    12 Programme Co-chairs

    13 

    14 

    15 ----------------------- REVIEW 1 ---------------------

    16 PAPER: 184

    17 TITLE: A Formal Model and Correctness Proof for an Access Control Policy Framework

    18 AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban

    19 

    20 

    21 ----------- REVIEW -----------

    22 The paper presents a formalization of the (dynamic) model of the

    23 Role-Compatibility (RC) model, in the interactive prover Isabelle, for

    24 the authorization of core operations in an operating system.  The

    25 authors use the inductive approach, introduced by Paulson, for

    26 cryptographic protocols.  The formalization of the model takes into

    27 account the dynamic behavior of the operation of an operating system.

    28 There are two groups of rules: admissible, formalizing the conditions

    29 under which operating system actions can be executed, and granted,

    30 formalizing the authorization requirements.  The authors develop a

    31 static check for taintable objects.  It is claimed that the rules can

    32 be easly adapted to the access control model of SELinux.  

    33 

    34 The English of the paper is good.  I have found few typos:

    35 

    36 - page 4, line -8: deletion Of IPCs --> deletion of IPCs

    37 - page 5, line 17: these function --> these functions

    38 - page 6, line 15: the way how the --> the way the

    39 - page 7, line 5: for the the role --> for the role

    40 - page 9, line 10: For example staring --> For example starting

    41 - page 10, line -6: unique process IDs --> unique process ID

    42 - page 12, line -6: process in tainted --> process is tainted

    43 - page 14, line -13: provisio --> proviso

    44 

    45 The formalisation seems to be reasonable although I would have liked

    46 an appendix to the paper in which the formalization is reported fully.

    47 

    48 The static check for taintable objects of the operating system seems

    49 to be useful and its (limited) scope of applicability is honestly

    50 discussed.

    51 

    52 The effort of taking into account te dynamic of the system, not only

    53 the authorization policies, is intersting and important to develop

    54 more precise security analysis techniques.  However, the authors

    55 should give a better idea of what kind of properties the proposed

    56 check can verify.  For example, can they perform information flow

    57 analysis?  

    58 

    59 My main concern with the paper is the lack of examples on which the

    60 various rules are shown and that the static check is not applied to a

    61 (possibly realistic) scenario to show its usefulness.  The advantages

    62 of the proposed check are only argued abstractly.  It is thus

    63 difficult to understand the degree of automation with which the static

    64 check can be carried out.  I know that Isabelle offers a high degree

    65 of automation to various proof attempts but the paper does not offer

    66 hints about this crucial aspect.  If the static check is not fully

    67 automated, then the usefulness of the formal model is greatly

    68 decreased.  

    69 

    70 For this reason, I suggest to consider the paper as borderline.  

    71 

    72 I have also the following comments on some aspects of the paper:

    73 

    74 - in Section 3, the notion of state is not precisely characterized.

    75   One can derive that there is a given notion of initial state and

    76   that the other state can be derived by applying to the initial state

    77   a (finite) sequence of actions of the operating system, but I was

    78   not able to find a place where this is explictly formalized.  

    79 

    80 - at the end of page 5, the definition of new_proc seems to be

    81   unnecessarely restrictive.  The thing that needs to be formalized

    82   here is the fact that the function returns a distinct identifier

    83   w.r.t. the existing identifiers in a state.  Taking the max of the

    84   identifiers (naturals) and adding one is indeed a way to ensure this

    85   but it is certanly not the only way.  An alterantive, more general,

    86   formalization is to assume the existence of an infinite set of

    87   identifiers, taking out all the identifiers in the actual state, and

    88   then pick any of the remaining identifiers.  This admits as an

    89   implementation the proposed definition of new_proc but also many

    90   others.  This seems to be important in the light of the remark at

    91   page 14, immediately after the statement of Theorem 2, saying that

    92   "we have no control over which process ID a process will be assigned

    93   with."  This does not seem to hold with the proposed definition of

    94   new_proc.  It does hold with the alternative definition above.

    95 

    96 - at the end of page 7, the notion of seeds are introduced but the

    97   reader is left with wondering how these are identified.  This is

    98   unswered only very late in the paper.  I suggest the authors to give

    99   some hints about this issue already here and mention that it is

   100   further discussed later in the paper.

   101 

   102 - at page 9, towards the end of Section 3, it is discussed that the

   103   restriction to the (so-called) undeletable objects of the proposed

   104   static check is needed to avoid to consider infinitely many objects

   105   and that this is crucial to make the check effective.  I am not sure

   106   to have understood exactly what the authors really mean.  One may

   107   (automatically) reason about infinitely many objects by using

   108   suitable constraints.  It may well be the case that it is possible

   109   to find (finitary) symbolic representations for states containing

   110   finitely many objects (but whose exact number is unknown).  This is

   111   standard, e.g., in the infinite state model checking of parametric

   112   systems.  The authors may have a look at the following seminal paper

   113   to have an idea of what can be done for the verification of systems

   114   with infinite state spaces:

   115 

   116   @article{AbdullaTCS,

   117     author = {P. A. Abdulla and B. Jonsson},

   118     title = {Model Checking of Systems with Many Identical Timed Processes},   

   119     journal = {Theoretical Computer Science},

   120     vol = {290 (1)}, 

   121     pages = {241--264},

   122     year = 2003,

   123   }

   124 

   125   I believe that this point should be clarified by the authors to put

   126   their verification technique in the right relationship with others.

   127 

   128   A similar observation can be done for the following sentence at the

   129   end of page 10: "otherwise exploring all possible "reachable"

   130   objects can lead to the potential infinity like in the dynamic

   131   model."  Indeed, there can be several sources of infinity in a

   132   problem that, as shown for example by the paper by Adbulla and

   133   Jonsson paper above, can be tamed and an exhaustive reachability

   134   analysis can be done.

   135 

   136 

   137 ----------------------- REVIEW 2 ---------------------

   138 PAPER: 184

   139 TITLE: A Formal Model and Correctness Proof for an Access Control Policy Framework

   140 AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban

   141 

   142 

   143 ----------- REVIEW -----------

   144 This work presents a specification of the role-compatibility (RC) model in the

   145 Isabelle theorem prover. RC is a role-based access control model created for use

   146 in Rule Set Based Access Control (RSBAC), an access control kernel module that

   147 provides implementations of mandatory, role-based, and access control-list

   148 models of access control for Linux. The model is to be used to detect the spread

   149 of "taintable" resources. The initial state of the system is assumed to contain

   150 some "seeds" (tainted files), which may then spread through the system. The

   151 static check, then, is whether a particular resource (e.g., the root of the

   152 filesystem) is taintable. The tainted^s relation

   153 (a static formulation of the taintable relation) is defined and proven to be

   154 sound and complete with respect to the work's notion of taintable.

   155 

   156 The authors claim that their approach is more accurate than policy analysis,

   157 since it takes into account additional details of the operating system, such as

   158 the processes that are started. This allows their approach to avoid the

   159 "over-approximations" of policy analysis (e.g., when a process assuming a

   160 particular role could cause a violation, but such a process is never created).

   161 These added details, however, seem at times to be based more on the authors'

   162 intuition than any particular implementation. For example:

   163 - A newly created process is assigned the ID: $\Max(current_ids) + 1$. Linux

   164   (where RC is currently implemented) uses $next_id++ % MAX_ID$ [unless taken]

   165   (i.e., it maintains a counter which is incremented when an ID is assigned, so

   166   cloning and terminating repeatedly still increases the counter rather than

   167   creating the same ID every time).

   168 - The set of users is assumed to be fixed (not a requirement in RSBAC or Linux).

   169 

   170 Thus, the model is more all-encompassing than some approaches to policy analysis

   171 due to modeling these details at all, but it falls short of verifying any

   172 particular implementation since these details are not justified. The work is

   173 poorly positioned among related work, as the authors seem unaware of the huge

   174 body of work on various techniques in access control static analysis [e.g.,

   175 1--3], especially work that also models the system at the process level [3].

   176 

   177 The methods for specifying the model are not claimed to be novel, and are a

   178 somewhat straightforward and unsurprising application of Paulson's inductive

   179 method. The authors say their approach can be easily applied to other access

   180 control models, but this seems more as a result of the approach being obvious

   181 than of it being particularly reusable. Furthermore, the authors do not

   182 demonstrate how a practical analysis would be carried out using this model;

   183 instead, they briefly discuss the way they they imagine it being used and the

   184 (uncited) reasons they believe the model's assumptions (only checking

   185 undeletable files for taintedness, the existence of a set of known "seed" files

   186 that are tainted in the initial state) are not too restrictive for it to be

   187 usable in practice.

   188 

   189 The work's main claimed contribution is the formalization of RC in Isabelle. The

   190 specification the authors present does not use novel techniques that can be

   191 reapplied elsewhere and is not shown to have a practical advantage over existing

   192 analysis techniques for role-based access control models. We question,

   193 therefore, whether this formalization alone is a sufficient contribution to

   194 warrant acceptance to a top venue such as ESORICS.

   195 

   196 [1] Mikhail I. Gofman, Ruiqi Luo, Ayla C. Solomon, Yingbin Zhang, Ping Yang,

   197 Scott D. Stoller: RBAC-PAT: A Policy Analysis Tool for Role Based Access

   198 Control. TACAS 2009:46--49.

   199 

   200 [2] Scott D. Stoller, Ping Yang, C. R. Ramakrishnan, Mikhail I. Gofman:

   201 Efficient policy analysis for administrative role based access control. ACM

   202 Conference on Computer and Communications Security 2007:445--455.

   203 

   204 [3] Arosha K. Bandara, Emil Lupu, Alessandra Russo: Using Event Calculus to

   205 Formalise Policy Specification and Analysis. POLICY 2003.

   206 

   207 

   208 ----------------------- REVIEW 3 ---------------------

   209 PAPER: 184

   210 TITLE: A Formal Model and Correctness Proof for an Access Control Policy Framework

   211 AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban

   212 

   213 

   214 ----------- REVIEW -----------

   215 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. 

   216 

   217 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: 

   218 

   219 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.

   220 

   221 J. Bryans. Reasoning about XACML policies using CSP. In Proceedings of the 2005 workshop on Secure web services, page 35. ACM, 2005.

   222 

   223 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.

   224 

   225 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.

   226 

   227 Joseph Y. Halpern and Vicky Weissman. Using first-order logic to reason about policies. ACM Trans. Inf. Syst. Secur., 11(4), 2008.

   228 

   229 Prathima Rao, Dan Lin, Elisa Bertino, Ninghui Li, Jorge Lobo: EXAM: An Environment for Access Control Policy Analysis and Management. POLICY 2008: 238-240

   230 

   231 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.

   232 

   233 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.

   234 

   235 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.