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.