Dear Christian Urban,

   We are happy to inform you that you paper 42,

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

has been accepted for presentation at the third edition of the

International Conference on Certified Programs and Proofs.

   Enclosed are the reviews for your paper. Please pay close attention to

the comments of the reviewers in preparing the final version of your paper,

which will be due on Monday September 16, 2013.

   Kind regards,

Georges Gonthier

Michael Norrish

   CPP 13 program chairs

----------------------- REVIEW 1 ---------------------

PAPER: 42

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

AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban

OVERALL EVALUATION: 0 (borderline paper)

REVIEWER'S CONFIDENCE: 4 (high)

----------- REVIEW -----------

This paper presents a formalisation of the Role-Compatibility access control model (RC-Model), which is similar to the Domain-Type Enforcement (DTE) model of SELinux, in Isabelle/HOL. The model is formalised with respect to an abstract operating system model with operations such as CreateFile, CloneProcess, WriteFile etc. Execution is modelled as sequences / traces of such events. Meaning is given to RC-Model policies by restricting the allowable traces of events to those permitted by the policy.

Policies are further given meaning in terms of a notion of "taintedness" introduced by the authors. An initial set of /seeds/ are initially tainted; taint spreads out through the system (for instance from a process p to a file f when p writes to f etc.) as execution proceeds.

Since the possible state space (sequences of allowed events) is infinite, the authors then devise a static, finite check to determine whether a particular entity can become tainted. This check effectively builds an abstraction (tainted^s) of the system in which all newly-created objects are aggregated together (which makes it finite), but records precise information regarding the taintedness of initial objects (which makes it precise for those objects).

The authors prove that their static check is both sound and complete (for undeletable objects).

The development appears technically sound. However, the ideas are fairly well understood from e.g. Paulson's work on the inductive model of security protocols, and from work devising finite, safe abstractions of access control systems, where the idea of aggregation for newly-created objects to produce finite, safe abstractions of systems is well applied.

I would also argue that some of the claims in the motivation could be made more precise or backed-up with better evidence. For instance, the claim in the opening sentence -- which OSes exactly use RBAC? SELinux uses DTE which seems simpler than the RC-Model, but the authors never cite the DTE papers when mentioning SELinux. I assume that the similarity between DTE and RC-Model is the basis for the claim that the RC-Model is used to secure "Apache servers". This should be made clear.

In general, I would suggest citing the SELinux papers, especially on the Domain-Type Enforcement model -- you certainly have space. Broader treatment of related work (e.g. on finite abstractions of dynamic access control systems by aggregation -- see e.g. Fred Spiessens' work on SCOLLAR) could also be accommodated in page limit I think.

One other point is that the "tainted" notion seems to be presented mostly in terms of tracking the effects of a brek-in (see last paragraph of Section 4). However, it seems like it could equally well be used to reason about confidentiality in the absence of covert channels. This might deserve some discussion.

Overall the work is solid, but isn't huge on novelty. Hence, my score of Borderline.

Minor comments:

- Drop the word "randomly" in quotes from page 5. new process IDs need only be unique, no?

- Explain more explicitly that states are sequences of events; that paths are stored in reverse-order.

- consider putting the "tained" relation into its own subsection, as this is new material over and above the straight RC-Model, right?

- On second-to-last line of page 10, drop "anchor of"

----------------------- REVIEW 2 ---------------------

PAPER: 42

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

AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban

OVERALL EVALUATION: 2 (accept)

REVIEWER'S CONFIDENCE: 4 (high)

----------- REVIEW -----------

This paper presents a formalization and correctness proof for the an access control policy framework called the Role-Compatibility Model. The paper introduces the dynamic semantics of a system controlled by an RC-model policy. It then develops a static check which is capable of determining all possible effects of a given RC-model policy on an initial system configuration. Finally, the paper proves the correctness of this check with respect to the dynamic semantics.

In part, the paper is a case study of formalizing a recently introduced semi-formal system. However, the authors go beyond this by introducing a dynamic semantics which allows them to establish the correctness of the model they formalize. The contributions are interesting and relevant. I recommend the paper be accepted.

----------------------- REVIEW 3 ---------------------

PAPER: 42

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

AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban

OVERALL EVALUATION: -1 (weak reject)

REVIEWER'S CONFIDENCE: 4 (high)

----------- REVIEW -----------

The paper formalizes the Role-Compatibility (RC) model of [4,5]. It defines its dynamic semantics, a notion of "taintability" (roughly the ability to influence a resource), and a more abstract semantics that is sound and complete for tainting. Both semantics consider only static, declarative policies, rather than e.g. actual executables and file contents. 

I am a bit surprised by the choice of RC as a starting point, inasmuch as there is a vast literature on RBAC, including more widely deployed systems, and papers using SMTs to check whether a policy excludes bad traces. Also, tainting is an important property, but many others are meant to be enforced by RBAC policies.

The paper is well written, but its theorem is not very surprising, as the three main new definitions are closely aligned. Arguably, policies being complete is too much to hope for with real RBAC systems. Also, there is not much discussion of the formalization effort itself. 

Related work: "Gran: Model Checking Grsecurity RBAC Policies" at CSF 2012 explores similar issues with policies (but does not provide formal proofs); in particular it defines a property similar to tainting, develops an abstraction for dynamic taintability, and report issues with role inheritance rules.

----------------------- REVIEW 4 ---------------------

PAPER: 42

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

AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban

OVERALL EVALUATION: 2 (accept)

REVIEWER'S CONFIDENCE: 3 (medium)

----------- REVIEW -----------

This is an appealing formalisation paper about an area with which I am not very familiar.  The background explanations are clear though, so I felt I was getting a good picture of what had been done, and its significance.  In essence, the paper describes an access-control formalism  due to Ott called the Role-Compatibility Model, develops an "obvious" mechanisation of that model, and then describes a nice decision procedure (original to this paper?) for checking the possible effects of corruption or tainting.  If one's security policy has been well-designed, then the d.p. will tell one that various forms of compromise can or can't affect permanent/important parts of the system.  So, for example, a compromised user account may well spread "compromise" or "taint" over a large proportion of the system (everything that user can touch), but should not be able to affect permanent files/resources owned by root (the contents of the /usr/bin directory, say).

I hesitate to rank the paper more strongly because of my own lack of confidence, but this seems like a strong contribution.  The formalisation of the RC model is elegantly done, but is perhaps fairly obvious given Paulson's well-known approach of characterising all possible system traces with an inductive relation.  However, adding to that contribution by inventing a finite abstraction of a system's dynamic behaviour, thereby creating a verified decision procedure for access control policy correctness, seems like something that certainly deserves to be published at CPP.

My only request for change would be for the authors to make it clearer whether or not their d.p. is original to them, and the degree of contribution they think it represents to the security community.