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.