|
1 From VM Fri Sep 6 13:27:30 2013 |
|
2 X-VM-v5-Data: ([nil nil nil nil t nil nil nil nil] |
|
3 ["8896" "Monday" "26" "August" "2013" "16:57:55" "+0200" "CPP 2013" "cpp2013@easychair.org" nil "98" "CPP 2013 notification for paper 42" "^From:" nil nil "8" nil nil nil nil nil nil nil nil nil nil] |
|
4 nil) |
|
5 Return-Path: <cpp2013@easychair.org> |
|
6 Delivered-To: unknown |
|
7 Received: from mailbroy.in.tum.de (131.159.46.88:995) by |
|
8 Christians-MacBook-Air-2.local with POP3-SSL; 26 Aug 2013 16:26:47 -0000 |
|
9 X-Original-To: urbanc@mailbroy.informatik.tu-muenchen.de |
|
10 Delivered-To: urbanc@mailbroy.informatik.tu-muenchen.de |
|
11 Received: from localhost (scan46 [10.46.146.16]) |
|
12 by mail46.informatik.tu-muenchen.de (Postfix) with ESMTP id 9A063885ECCEA |
|
13 for <urbanc@mailbroy.informatik.tu-muenchen.de>; Mon, 26 Aug 2013 16:58:08 +0200 (CEST) |
|
14 X-Virus-Scanned: amavisd-new at informatik.tu-muenchen.de |
|
15 X-Spam-MTA-Flag: NO |
|
16 X-Spam-MTA-Status: No, score=0.0 required=5.0 tests=none autolearn=unavailable |
|
17 version=3.3.2 |
|
18 X-Spam-MTA-Level: |
|
19 X-Spam-MTA-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on scan46 |
|
20 Received: from mail46.informatik.tu-muenchen.de ([10.46.146.15]) |
|
21 by localhost (mail46.informatik.tu-muenchen.de [10.46.146.16]) (amavisd-new, port 10024) |
|
22 with ESMTP id i--Dvm4t7vwc |
|
23 for <urbanc@mailbroy.informatik.tu-muenchen.de>; |
|
24 Mon, 26 Aug 2013 16:58:03 +0200 (CEST) |
|
25 Received: from mailrelay1.informatik.tu-muenchen.de (mailrelay1.informatik.tu-muenchen.de [131.159.254.14]) |
|
26 by mail46.informatik.tu-muenchen.de (Postfix) with ESMTP id 119618133D93D |
|
27 for <urbanc@mailbroy.informatik.tu-muenchen.de>; Mon, 26 Aug 2013 16:58:03 +0200 (CEST) |
|
28 Received: by mailrelay1.informatik.tu-muenchen.de (Postfix) |
|
29 id E3FAA27E4D; Mon, 26 Aug 2013 16:58:02 +0200 (CEST) |
|
30 Delivered-To: christian.urban@informatik.tu-muenchen.de |
|
31 Received: from mailrelay1.informatik.tu-muenchen.de (localhost [127.0.0.1]) |
|
32 by mailrelay1.informatik.tu-muenchen.de (Postfix) with ESMTP id CD21927E49 |
|
33 for <urbanc@in.tum.de>; Mon, 26 Aug 2013 16:58:02 +0200 (CEST) |
|
34 Received: from maildmz2.informatik.tu-muenchen.de (maildmz2.informatik.tu-muenchen.de [131.159.0.15]) |
|
35 by mailrelay1.informatik.tu-muenchen.de (Postfix) with ESMTP id C41B127E48 |
|
36 for <urbanc@in.tum.de>; Mon, 26 Aug 2013 16:58:02 +0200 (CEST) |
|
37 Received: by maildmz2.informatik.tu-muenchen.de (Postfix, from userid 1506) |
|
38 id BF13F4C7BD; Mon, 26 Aug 2013 16:58:02 +0200 (CEST) |
|
39 X-Spam-Checker-Version: SpamAssassin 3.2.5-tuminfo_1 (2008-06-10) on maildmz2 |
|
40 X-Spam-Level: |
|
41 X-Spam-Status: No, score=-2.6 required=7.0 tests=AWL,BAYES_00 autolearn=ham |
|
42 version=3.2.5-tuminfo_1 |
|
43 Received: from maildmz2.informatik.tu-muenchen.de (localhost [127.0.0.1]) |
|
44 by maildmz2.informatik.tu-muenchen.de (Postfix) with ESMTP id 07430491BD |
|
45 for <urbanc@in.tum.de>; Mon, 26 Aug 2013 16:57:54 +0200 (CEST) |
|
46 Received: from easychair.org (easychair.org [80.241.208.147]) |
|
47 by maildmz2.informatik.tu-muenchen.de (Postfix) with ESMTP id E7286491BC |
|
48 for <urbanc@in.tum.de>; Mon, 26 Aug 2013 16:57:53 +0200 (CEST) |
|
49 Received: from localhost.localdomain (m1647.giga-dns.com [80.241.208.147]) |
|
50 by easychair.org (8.14.5/8.14.5) with ESMTP id r7QEvt6V020904 |
|
51 for <urbanc@in.tum.de>; Mon, 26 Aug 2013 16:57:55 +0200 |
|
52 Message-Id: <201308261457.r7QEvt6V020904@easychair.org> |
|
53 Content-Disposition: inline |
|
54 Content-Transfer-Encoding: 8bit |
|
55 Content-Type: text/plain; charset="UTF-8" |
|
56 MIME-Version: 1.0 |
|
57 X-Mailer: MIME::Lite 3.029 (F2.82; T1.38; A2.12; B3.13; Q3.13) |
|
58 From: CPP 2013 <cpp2013@easychair.org> |
|
59 To: Christian Urban <urbanc@in.tum.de> |
|
60 Subject: CPP 2013 notification for paper 42 |
|
61 Date: Mon, 26 Aug 2013 16:57:55 +0200 |
|
62 |
|
63 Dear Christian Urban, |
|
64 |
|
65 We are happy to inform you that you paper 42, |
|
66 A Formal Model and Correctness Proof for an Access Control Policy Framework |
|
67 has been accepted for presentation at the third edition of the |
|
68 International Conference on Certified Programs and Proofs. |
|
69 Enclosed are the reviews for your paper. Please pay close attention to |
|
70 the comments of the reviewers in preparing the final version of your paper, |
|
71 which will be due on Monday September 16, 2013. |
|
72 |
|
73 Kind regards, |
|
74 Georges Gonthier |
|
75 Michael Norrish |
|
76 CPP 13 program chairs |
|
77 |
|
78 |
|
79 ----------------------- REVIEW 1 --------------------- |
|
80 PAPER: 42 |
|
81 TITLE: A Formal Model and Correctness Proof for an Access Control Policy Framework |
|
82 AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban |
|
83 |
|
84 OVERALL EVALUATION: 0 (borderline paper) |
|
85 REVIEWER'S CONFIDENCE: 4 (high) |
|
86 |
|
87 ----------- REVIEW ----------- |
|
88 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. |
|
89 |
|
90 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. |
|
91 |
|
92 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). |
|
93 |
|
94 The authors prove that their static check is both sound and complete (for undeletable objects). |
|
95 |
|
96 |
|
97 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. |
|
98 |
|
99 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. |
|
100 |
|
101 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. |
|
102 |
|
103 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. |
|
104 |
|
105 Overall the work is solid, but isn't huge on novelty. Hence, my score of Borderline. |
|
106 |
|
107 Minor comments: |
|
108 |
|
109 - Drop the word "randomly" in quotes from page 5. new process IDs need only be unique, no? |
|
110 - Explain more explicitly that states are sequences of events; that paths are stored in reverse-order. |
|
111 - consider putting the "tained" relation into its own subsection, as this is new material over and above the straight RC-Model, right? |
|
112 - On second-to-last line of page 10, drop "anchor of" |
|
113 |
|
114 |
|
115 ----------------------- REVIEW 2 --------------------- |
|
116 PAPER: 42 |
|
117 TITLE: A Formal Model and Correctness Proof for an Access Control Policy Framework |
|
118 AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban |
|
119 |
|
120 OVERALL EVALUATION: 2 (accept) |
|
121 REVIEWER'S CONFIDENCE: 4 (high) |
|
122 |
|
123 ----------- REVIEW ----------- |
|
124 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. |
|
125 |
|
126 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. |
|
127 |
|
128 |
|
129 ----------------------- REVIEW 3 --------------------- |
|
130 PAPER: 42 |
|
131 TITLE: A Formal Model and Correctness Proof for an Access Control Policy Framework |
|
132 AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban |
|
133 |
|
134 OVERALL EVALUATION: -1 (weak reject) |
|
135 REVIEWER'S CONFIDENCE: 4 (high) |
|
136 |
|
137 ----------- REVIEW ----------- |
|
138 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. |
|
139 |
|
140 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. |
|
141 |
|
142 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. |
|
143 |
|
144 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. |
|
145 |
|
146 |
|
147 ----------------------- REVIEW 4 --------------------- |
|
148 PAPER: 42 |
|
149 TITLE: A Formal Model and Correctness Proof for an Access Control Policy Framework |
|
150 AUTHORS: Chunhan Wu, Xingyuan Zhang and Christian Urban |
|
151 |
|
152 OVERALL EVALUATION: 2 (accept) |
|
153 REVIEWER'S CONFIDENCE: 3 (medium) |
|
154 |
|
155 ----------- REVIEW ----------- |
|
156 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). |
|
157 |
|
158 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. |
|
159 |
|
160 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. |
|
161 |