1
+ − 1
(*<*)
+ − 2
theory Paper
+ − 3
imports rc_theory final_theorems rc_theory os_rc
+ − 4
begin
+ − 5
+ − 6
(* THEOREMS *)
+ − 7
+ − 8
+ − 9
notation (Rule output)
+ − 10
"==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+ − 11
+ − 12
syntax (Rule output)
+ − 13
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ − 14
("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+ − 15
+ − 16
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
+ − 17
("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+ − 18
+ − 19
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+ − 20
+ − 21
notation (Axiom output)
+ − 22
"Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+ − 23
+ − 24
notation (IfThen output)
+ − 25
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 26
syntax (IfThen output)
+ − 27
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ − 28
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 29
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ − 30
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+ − 31
+ − 32
notation (IfThenNoBox output)
+ − 33
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 34
syntax (IfThenNoBox output)
+ − 35
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ − 36
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ − 37
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ − 38
"_asm" :: "prop \<Rightarrow> asms" ("_")
+ − 39
+ − 40
(* insert *)
+ − 41
notation (latex)
+ − 42
"Set.empty" ("\<emptyset>")
+ − 43
+ − 44
translations
+ − 45
"{x} \<union> A" <= "CONST insert x A"
+ − 46
"{x,y}" <= "{x} \<union> {y}"
+ − 47
"{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
+ − 48
"{x}" <= "{x} \<union> \<emptyset>"
+ − 49
+ − 50
lemma impeq:
+ − 51
"A = B \<Longrightarrow> (B \<Longrightarrow> A)"
+ − 52
by auto
+ − 53
+ − 54
+ − 55
+ − 56
+ − 57
consts DUMMY::'a
+ − 58
+ − 59
abbreviation
+ − 60
"is_parent f pf \<equiv> (parent f = Some pf)"
+ − 61
+ − 62
context tainting_s_sound begin
+ − 63
+ − 64
notation (latex output)
+ − 65
source_dir ("anchor") and
+ − 66
SProc ("P_\<^bsup>_\<^esup>") and
+ − 67
SFile ("F_\<^bsup>_\<^esup>") and
+ − 68
SIPC ("I'(_')\<^bsup>_\<^esup>") and
+ − 69
READ ("Read") and
+ − 70
WRITE ("Write") and
+ − 71
EXECUTE ("Execute") and
+ − 72
CHANGE_OWNER ("ChangeOwner") and
+ − 73
CREATE ("Create") and
+ − 74
SEND ("Send") and
+ − 75
RECEIVE ("Receive") and
+ − 76
DELETE ("Delete") and
+ − 77
compatible ("permissions") and
+ − 78
comproles ("compatible") and
+ − 79
DUMMY ("\<^raw:\mbox{$\_$}>") and
+ − 80
Cons ("_::_" [78,77] 79) and
+ − 81
Proc ("") and
+ − 82
File ("") and
+ − 83
File_type ("") and
+ − 84
Proc_type ("") and
+ − 85
IPC ("") and
+ − 86
init_processes ("init'_procs") and
+ − 87
os_grant ("admissible") and
+ − 88
rc_grant ("granted") and
+ − 89
exists ("alive") and
+ − 90
default_fd_create_type ("default'_type") and
+ − 91
InheritParent_file_type ("InheritPatentType") and
+ − 92
NormalFile_type ("NormalFileType") and
+ − 93
deleted ("deleted _ _" [50, 100] 100) and
+ − 94
taintable_s ("taintable\<^isup>s") and
+ − 95
tainted_s ("tainted\<^isup>s") and
+ − 96
all_sobjs ("reachable\<^isup>s") and
+ − 97
init_obj2sobj ("\<lbrakk>_\<rbrakk>") and
+ − 98
erole_functor ("erole'_aux") --"I have a erole_functor and etype_aux to handle
+ − 99
efficient, but their name not same, so ..., but don't work"
+ − 100
+ − 101
+ − 102
abbreviation
+ − 103
"is_process_type s p t \<equiv> (type_of_process s p = Some t)"
+ − 104
+ − 105
abbreviation
+ − 106
"is_current_role s p r \<equiv> (currentrole s p = Some r)"
+ − 107
+ − 108
abbreviation
+ − 109
"is_file_type s f t \<equiv> (etype_of_file s f = Some t)"
+ − 110
+ − 111
lemma osgrant2:
+ − 112
"\<lbrakk>p \<in> current_procs \<tau>; f \<notin> current_files \<tau>; parent f = Some pf; pf \<in> current_files \<tau>\<rbrakk> \<Longrightarrow>
+ − 113
os_grant \<tau> (CreateFile p f)"
+ − 114
by simp
+ − 115
+ − 116
lemma osgrant6:
+ − 117
"\<lbrakk>p \<in> current_procs \<tau>; u \<in> init_users\<rbrakk> \<Longrightarrow> os_grant \<tau> (ChangeOwner p u)"
+ − 118
by simp
+ − 119
+ − 120
lemma osgrant10:
+ − 121
"\<lbrakk>p \<in> current_procs \<tau>; p' = new_proc \<tau>\<rbrakk> \<Longrightarrow> os_grant \<tau> (Clone p p')"
+ − 122
by simp
+ − 123
+ − 124
+ − 125
lemma rcgrant1:
+ − 126
"\<lbrakk>is_parent f pf; is_file_type s pf t; is_current_role s p r;
+ − 127
default_fd_create_type r = InheritParent_file_type;
+ − 128
(r, File_type t, WRITE) \<in> compatible\<rbrakk>
+ − 129
\<Longrightarrow> rc_grant s (CreateFile p f)"
+ − 130
by simp
+ − 131
+ − 132
lemma rcgrant1':
+ − 133
"\<lbrakk>is_parent f pf; is_file_type s pf t; is_current_role s p r;
+ − 134
default_fd_create_type r = NormalFile_type t';
+ − 135
(r, File_type t, WRITE) \<in> compatible;
+ − 136
(r, File_type t', CREATE) \<in> compatible\<rbrakk>
+ − 137
\<Longrightarrow> rc_grant s (CreateFile p f)"
+ − 138
by simp
+ − 139
+ − 140
lemma rcgrant4:
+ − 141
"\<lbrakk>is_current_role s p r; is_file_type s f t; (r, File_type t, EXECUTE) \<in> compatible\<rbrakk>
+ − 142
\<Longrightarrow> rc_grant s (Execute p f)"
+ − 143
by simp
+ − 144
+ − 145
lemma rcgrant7:
+ − 146
"\<lbrakk>is_current_role s p r; r' \<in> comproles r\<rbrakk> \<Longrightarrow> rc_grant s (ChangeRole p r')"
+ − 147
by simp
+ − 148
+ − 149
lemma rcgrant_CHO:
+ − 150
"\<lbrakk>is_current_role s p r;
+ − 151
type_of_process s p = Some t;
+ − 152
(r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> rc_grant s (ChangeOwner p u)"
+ − 153
by(simp)
+ − 154
+ − 155
lemma pf_in_current_paper:
+ − 156
"\<lbrakk>is_parent f pf; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> pf \<in> current_files s"
+ − 157
by (simp add:parent_file_in_current)
+ − 158
+ − 159
lemma dels:
+ − 160
shows "deleted (Proc p') ((Kill p p')#s)"
+ − 161
and "deleted (File f) ((DeleteFile p f)#s)"
+ − 162
and "deleted (IPC i) ((DeleteIPC p i)#s)"
+ − 163
and "deleted obj s \<Longrightarrow> deleted obj (e#s)"
+ − 164
apply simp_all
+ − 165
apply(case_tac e)
+ − 166
apply(simp_all)
+ − 167
done
+ − 168
+ − 169
lemma tainted_10:
+ − 170
"\<lbrakk>(File f) \<in> tainted s; valid (e # s); f \<in> current_files (e # s)\<rbrakk>
+ − 171
\<Longrightarrow> (File f) \<in> tainted (e # s)"
+ − 172
apply(rule tainted.intros)
+ − 173
apply(assumption)
+ − 174
apply(assumption)
+ − 175
apply(simp only: exists.simps)
+ − 176
done
+ − 177
+ − 178
definition
+ − 179
Init ("init _")
+ − 180
where
+ − 181
"Init obj \<equiv> exists [] obj"
+ − 182
+ − 183
lemma Init_rhs:
+ − 184
shows "Init (File f) = (f \<in> init_files)"
+ − 185
and "Init (Proc p) = (p \<in> init_processes)"
+ − 186
and "Init (IPC i) = (i \<in> init_ipcs)"
+ − 187
unfolding Init_def
+ − 188
by(simp_all)
+ − 189
+ − 190
notation (latex output)
+ − 191
Init ("_ \<in> init")
+ − 192
+ − 193
lemma af_init':
+ − 194
"\<lbrakk>f \<in> init_files; is_file_type [] f t\<rbrakk>
+ − 195
\<Longrightarrow> SFile (t, f) (Some f) \<in> all_sobjs"
+ − 196
apply(rule af_init)
+ − 197
apply(simp)
+ − 198
by (simp add:etype_of_file_def)
+ − 199
+ − 200
declare [[show_question_marks = false]]
+ − 201
+ − 202
+ − 203
(*>*)
+ − 204
+ − 205
section {* Introduction *}
+ − 206
+ − 207
text {*
+ − 208
Role-based access control models are used in many operating systems
+ − 209
for enforcing security properties. The
+ − 210
\emph{Role-Compatibility Model} (RC-Model), introduced by Ott
+ − 211
\cite{ottrc,ottthesis}, is one such role-based access control
+ − 212
model. It defines \emph{roles}, which are associated with processes,
+ − 213
and defines \emph{types}, which are associated with system
+ − 214
resources, such as files and directories. The RC-Model also includes
+ − 215
types for interprocess communication, that is message queues,
+ − 216
sockets and shared memory. A policy in the RC-Model gives every user
+ − 217
a default role, and also specifies how roles can be
+ − 218
changed. Moreover, it specifies which types of resources a role has
+ − 219
permission to access, and also the \emph{mode} with which the role
+ − 220
can access the resources, for example read, write, send, receive and
+ − 221
so on.
+ − 222
+ − 223
The RC-Model is built on top of a collection of system calls
+ − 224
provided by the operating system, for instance system calls for
+ − 225
reading and writing files, cloning and killing of processes, and
+ − 226
sending and receiving messages. The purpose of the RC-Model is to
+ − 227
restrict access to these system calls and thereby enforce security
+ − 228
properties of the system. A problem with the RC-Model and role-based
+ − 229
access control models in general is that a system administrator has
+ − 230
to specify an appropriate access control policy. The difficulty with
+ − 231
this is that \emph{``what you specify is what you get but not
+ − 232
necessarily what you want''} \cite[Page 242]{Jha08}. To overcome
+ − 233
this difficulty, a system administrator needs some kind of sanity
+ − 234
check for whether an access control policy is really securing
+ − 235
resources. Existing works, for example \cite{sanity01,sanity02},
+ − 236
provide sanity checks for policies by specifying properties and
+ − 237
using model checking techniques to ensure a policy at hand satisfies
+ − 238
these properties. However, these checks only address the problem on
+ − 239
the level of policies---they can only check ``on the surface''
+ − 240
whether the policy reflects the intentions of the system
+ − 241
administrator---these checks are not justified by the actual
+ − 242
behaviour of the operating system. The main problem this paper addresses is to check
+ − 243
when a policy matches the intentions of a system administrator
+ − 244
\emph{and} given such a policy, the operating system actually
+ − 245
enforces this policy.
+ − 246
+ − 247
Our work is related to the preliminary work by Archer et al
+ − 248
\cite{Archer03} about the security model of SELinux.
+ − 249
They also give a dynamic model of system calls on which the access
+ − 250
controls are implemented. Their dynamic model is defined in terms of
+ − 251
IO automata and mechanised in the PVS theorem prover. For specifying
+ − 252
and reasoning about automata they use the TAME tool in PVS. Their work checks
+ − 253
well-formedness properties of access policies by type-checking
+ − 254
generated definitions in PVS. They can also ensure some ``\emph{simple
+ − 255
properties}'' (their terminology), for example whether a process
+ − 256
with a particular PID is present in every reachable state from
+ − 257
an initial state. They also consider ``\emph{deeper properties}'', for
+ − 258
example whether only a process with root-permissions
+ − 259
or one of its descendents ever gets permission to write to kernel
+ − 260
log files. They write that they can state such deeper
+ − 261
properties about access policies, but about checking such properties
+ − 262
they write that ``\emph{the feasibility of doing
+ − 263
so is currently an open question}'' \cite[Page 167]{Archer03}.
+ − 264
We improve upon their results by using our sound and complete
+ − 265
static policy check to make this feasible.
+ − 266
+ − 267
Our formal models and correctness proofs are mechanised in the
+ − 268
interactive theorem prover Isabelle/HOL. The mechanisation of the models is a
+ − 269
prerequisite for any correctness proof about the RC-Model, since it
+ − 270
includes a large number of interdependent concepts and very complex
+ − 271
operations that determine roles and types. In our opinion it is
+ − 272
futile to attempt to reason about them by just using ``pencil-and-paper''.
+ − 273
Following good experience in earlier mechanisation work
+ − 274
\cite{ZhangUrbanWu12}, we use Paulson's inductive method for
+ − 275
reasoning about sequences of events \cite{Paulson98}. For example
+ − 276
we model system calls as events and reason about an inductive
+ − 277
definition of valid traces, that is lists of events. Central to
+ − 278
this paper is a notion of a resource being \emph{tainted}, which for
+ − 279
example means it contains a virus or a back door. We use our model
+ − 280
of system calls in order to characterise how such a tainted object
+ − 281
can ``spread'' through the system. For a system administrator the
+ − 282
important question is whether such a tainted file, possibly
+ − 283
introduced by a user, can affect core system files and render the
+ − 284
whole system insecure, or whether it can be contained by the access
+ − 285
policy. Our results show that a corresponding check can be performed
+ − 286
statically by analysing the initial state of the system and the access policy.
+ − 287
\smallskip
+ − 288
+ − 289
\noindent
+ − 290
{\bf Contributions:}
+ − 291
We give a complete formalisation of the RC-Model in the interactive
+ − 292
theorem prover Isabelle/HOL. We also give a dynamic model of the
+ − 293
operating system by formalising all security related events that can
+ − 294
happen while the system is running. As far as we are aware, we are
+ − 295
the first ones who formally prove that if a policy in the RC-Model
+ − 296
satisfies an access property, then there is no sequence of events
+ − 297
(system calls) that can violate this access property. We also prove
+ − 298
the opposite: if a policy does not meet an access property, then
+ − 299
there is a sequence of events that will violate this property in our
+ − 300
model of the operating system. With these two results in place we
+ − 301
can show that a static policy check is sufficient in order to
+ − 302
guarantee the access properties before running the system. Again as
+ − 303
far as we know, no such check that is the operating
+ − 304
system behaviour has been designed before.
+ − 305
+ − 306
+ − 307
%Specified dynamic behaviour of the system;
+ − 308
%we specified a static AC model; designed a tainted relation for
+ − 309
%the system; proved that they coincide.
+ − 310
%In our paper ....
+ − 311
+ − 312
*}
+ − 313
+ − 314
section {* Preliminaries about the RC-Model *}
+ − 315
+ − 316
+ − 317
text {*
+ − 318
The Role-Compatibility Model (RC-Model) is a role-based access
+ − 319
control model. It has been introduced by Ott \cite{ottrc} and is
+ − 320
used in running systems for example to secure Apache servers. It
+ − 321
provides a more fine-grained control over access permissions than
+ − 322
simple Unix-style access control models. This more fine-grained
+ − 323
control solves the problem of server processes running as root with
+ − 324
too many access permissions in order to accomplish a task at
+ − 325
hand. In the RC-Model, system administrators are able to restrict
+ − 326
what the role of server is allowed to do and in doing so reduce the
+ − 327
attack surface of a system.
+ − 328
+ − 329
Policies in the RC-Model talk about \emph{users}, \emph{roles},
+ − 330
\emph{types} and \emph{objects}. Objects are processes, files or
+ − 331
IPCs (interprocess communication objects---such as message queues,
+ − 332
sockets and shared memory). Objects are the resources of a system an
+ − 333
RC-policy can restrict access to. In what follows we use the letter
+ − 334
@{term u} to stand for users, @{text r} for roles, @{term p} for
+ − 335
processes, @{term f} for files and @{term i} for IPCs. We also
+ − 336
use @{text obj} as a generic variable for objects.
+ − 337
The RC-Model has the following eight kinds of access modes to objects:
+ − 338
+ − 339
\begin{isabelle}\ \ \ \ \ %%%
+ − 340
\begin{tabular}{@ {}l}
+ − 341
@{term READ}, @{term WRITE}, @{term EXECUTE}, @{term "CHANGE_OWNER"},
+ − 342
@{term CREATE}, @{term SEND}, @{term RECEIVE} and @{term DELETE}
+ − 343
\end{tabular}
+ − 344
\end{isabelle}
+ − 345
+ − 346
In the RC-Model, roles group users according to tasks they need to
+ − 347
accomplish. Users have a default role specified by the policy,
+ − 348
which is the role they start with whenever they log into the system.
+ − 349
A process contains the information about its owner (a user), its
+ − 350
role and its type, whereby a type in the RC-Model allows system
+ − 351
administrators to group resources according to a common criteria.
+ − 352
Such detailed information is needed in the RC-Model, for example, in
+ − 353
order to allow a process to change its ownership. For this the
+ − 354
RC-Model checks the role of the process and its type: if the access
+ − 355
control policy states that the role has @{term CHANGE_OWNER} access mode for
+ − 356
processes of that type, then the process is permitted to assume a
+ − 357
new owner.
+ − 358
+ − 359
Files in the RC-Model contain the information about their types. A
+ − 360
policy then specifies whether a process with a given role can access
+ − 361
a file under a certain access mode. Files, however, also
+ − 362
include in the RC-Model information about roles. This information is
+ − 363
used when a process is permitted to execute a file. By doing so it
+ − 364
might change its role. This is often used in the context of
+ − 365
web-servers when a cgi-script is uploaded and then executed by the
+ − 366
server. The resulting process should have much more restricted
+ − 367
access permissions. This kind of behaviour when executing a file can
+ − 368
be specified in an RC-policy in several ways: first, the role of the
+ − 369
process does not change when executing a file; second, the process
+ − 370
takes on the role specified with the file; or third, use the role of
+ − 371
the owner, who currently owns this process. The RC-Model also makes
+ − 372
assumptions on how types can change. For example for files and IPCs
+ − 373
the type can never change once they are created. But processes can
+ − 374
change their types according to the roles they have.
+ − 375
+ − 376
As can be seen, the information contained in a policy in the
+ − 377
RC-Model can be rather complex: Roles and types, for example, are
+ − 378
policy-dependent, meaning each policy needs to define a set of roles and a
+ − 379
set of types. Apart from recording for each role the information
+ − 380
which type of resource it can access and under which access-mode, it
+ − 381
also needs to include a role compatibility set. This set specifies how one
+ − 382
role can change into another role. Moreover it needs to include default
+ − 383
information for cases when new processes or files are created.
+ − 384
For example, when a process clones itself, the type of the new
+ − 385
process is determined as follows: the policy might specify a default
+ − 386
type whenever a process with a certain role is cloned, or the policy
+ − 387
might specify that the cloned process inherits the type of the
+ − 388
parent process.
+ − 389
+ − 390
Ott implemented the RC-Model on top of Linux, but only specified it
+ − 391
as a set of informal rules, partially given as logic formulas,
+ − 392
partially given as rules in ``English''. Unfortunately, some
+ − 393
presentations about the RC-Model give conflicting definitions for
+ − 394
some concepts---for example when defining the semantics of the special role
+ − 395
``inherit parent''. In \cite{ottrc} it means inherit the initial role
+ − 396
of the parent directory, but in \cite{ottweb} it means inherit
+ − 397
the role of the parent process. In our formalisation we mainly follow the
+ − 398
version given in \cite{ottrc}. In the next section we give a mechanised
+ − 399
model of the system calls on which the RC-Model is implemented.
+ − 400
*}
+ − 401
+ − 402
+ − 403
+ − 404
section {* Dynamic Model of System Calls *}
+ − 405
+ − 406
text {*
+ − 407
Central to the RC-Model are processes, since they initiate any action
+ − 408
involving resources and access control. We use natural numbers to stand for process IDs,
+ − 409
but do not model the fact that the number of processes in any practical
+ − 410
system is limited. Similarly, IPCs and users are represented by natural
+ − 411
numbers. The thirteen actions a process can perform are represented by
+ − 412
the following datatype of \emph{events}
+ − 413
+ − 414
\begin{isabelle}\ \ \ \ \ %%%
+ − 415
\mbox{
+ − 416
\begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l@ {\hspace{3mm}}l@
+ − 417
{\hspace{1.5mm}}l@ {\hspace{3mm}}l@ {\hspace{1.5mm}}l@
+ − 418
{\hspace{3mm}}l@ {\hspace{1.5mm}}l}
+ − 419
event
+ − 420
& @{text "::="} & @{term "CreateFile p f"} & @{text "|"} & @{term "ReadFile p f"} & @{text "|"} & @{term "Send p i"} & @{text "|"} & @{term "Kill p p'"} \\
+ − 421
& @{text "|"} & @{term "WriteFile p f"} & @{text "|"} & @{term "Execute p f"} & @{text "|"} & @{term "Recv p i"}\\
+ − 422
& @{text "|"} & @{term "DeleteFile p f"} & @{text "|"} & @{term "Clone p p'"} & @{text "|"} & @{term "CreateIPC p i"} \\
+ − 423
& @{text "|"} & @{term "ChangeOwner p u"} & @{text "|"} & @{term "ChangeRole p r"} & @{text "|"} & @{term "DeleteIPC p i"}\\
+ − 424
\end{tabular}}
+ − 425
\end{isabelle}
+ − 426
+ − 427
\noindent
+ − 428
with the idea that for example in @{term Clone} a process @{term p} is cloned
+ − 429
and the new process has the ID @{term "p'"}; with @{term Kill} the
+ − 430
intention is that the process @{term p} kills another process with
+ − 431
ID @{term p'}. We will later give the definition what the role
+ − 432
@{term r} can stand for in the constructor @{term ChangeRole}
+ − 433
(namely \emph{normal roles} only). As is custom in Unix, there is no
+ − 434
difference between a directory and a file. The files @{term f} in
+ − 435
the definition above are simply lists of strings. For example, the
+ − 436
file @{text "/usr/bin/make"} is represented by the list @{text
+ − 437
"[make, bin, usr]"} and the @{text root}-directory is the @{text
+ − 438
Nil}-list. Following the presentation in \cite{ottrc}, our model of
+ − 439
IPCs is rather simple-minded: we only have events for creation and deletion Of IPCs,
+ − 440
as well as sending and receiving messages.
+ − 441
+ − 442
Events essentially transform one state of the system into
+ − 443
another. The system starts with an initial state determining which
+ − 444
processes, files and IPCs are active at the start of the system. We assume the
+ − 445
users of the system are fixed in the initial state; we also assume
+ − 446
that the policy does not change while the system is running. We have
+ − 447
three sets, namely
+ − 448
@{term init_processes},
+ − 449
@{term init_files} and
+ − 450
@{term init_ipcs}
+ − 451
specifying the processes, files and IPCs present in the initial state.
+ − 452
We will often use the abbreviation
+ − 453
+ − 454
\begin{center}
+ − 455
@{thm (lhs) Init_def} @{text "\<equiv>"}
+ − 456
@{thm (rhs) Init_rhs(1)[where f=obj]} @{text "\<or>"}
+ − 457
@{thm (rhs) Init_rhs(2)[where p=obj]} @{text "\<or>"}
+ − 458
@{thm (rhs) Init_rhs(3)[where i=obj]}
+ − 459
\end{center}
+ − 460
+ − 461
\noindent
+ − 462
There are some assumptions we make about the files present in the initial state: we always
+ − 463
require that the @{text "root"}-directory @{term "[]"} is part of the initial state
+ − 464
and for every file in the initial state (excluding @{term "[]"}) we require that its
+ − 465
parent is also part of the
+ − 466
initial state.
+ − 467
After the initial state, the next states are determined
+ − 468
by a list of events, called the \emph{trace}. We need to define
+ − 469
functions that allow us to make some observations about traces. One
+ − 470
such function is called @{term "current_procs"} and
+ − 471
calculates the set of ``alive'' processes in a state:
+ − 472
+ − 473
%initial state:
+ − 474
%We make assumptions about the initial state, they're:
+ − 475
%1. there exists a set of processes, files, IPCs and users already in the initial state,
+ − 476
%users are not changed in system's running, we regards users adding and deleting a
+ − 477
%administration task, not the issue for our policy checker;
+ − 478
%2. every object in the initial state have got already roles/types/owner ... information assigned;
+ − 479
%3. all the policy information are already preloaded in the initial state, including:
+ − 480
%a compatible type table, @{term compatible};
+ − 481
%a mapping function from a role to its compatible role set, @{term comproles};
+ − 482
%every role's default values is pre-set, e.g. default process create type and
+ − 483
%and default file/directory create type.
+ − 484
+ − 485
\begin{isabelle}\ \ \ \ \ %%%
+ − 486
\mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ − 487
@{thm (lhs) current_procs.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) current_procs.simps(1)}\\
+ − 488
@{thm (lhs) current_procs.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) current_procs.simps(2)}\\
+ − 489
@{thm (lhs) current_procs.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) current_procs.simps(3)}\\
+ − 490
@{term "current_procs (DUMMY#s)"} & @{text "\<equiv>"} & @{term "current_procs s"}
+ − 491
\end{tabular}}
+ − 492
\end{isabelle}
+ − 493
+ − 494
\noindent
+ − 495
The first clause states that in the empty trace, that is initial
+ − 496
state, the processes are given by @{text "init_processes"}. The
+ − 497
events for cloning a process, respectively killing a process, update this
+ − 498
set of processes appropriately. Otherwise the set of live
+ − 499
processes is unchanged. We have similar functions for alive files and
+ − 500
IPCs, called @{term "current_files"} and @{term "current_ipcs"}.
+ − 501
+ − 502
We can use these function in order to formally model which events are
+ − 503
\emph{admissible} by the operating system in each state. We show just three
+ − 504
rules that give the gist of this definition. First the rule for changing
+ − 505
an owner of a process:
+ − 506
+ − 507
\begin{center}
+ − 508
@{thm[mode=Rule] osgrant6}
+ − 509
\end{center}
+ − 510
+ − 511
\noindent
+ − 512
We require that the process @{text p} is alive in the state @{text s}
+ − 513
(first premise) and that the new owner is a user that existed in the initial state
+ − 514
(second premise).
+ − 515
Next the rule for creating a new file:
+ − 516
+ − 517
\begin{center}
+ − 518
@{thm[mode=Rule] osgrant2}
+ − 519
\end{center}
+ − 520
+ − 521
\noindent
+ − 522
It states that
+ − 523
a file @{text f} can be created by a process @{text p} being alive in the state @{text s},
+ − 524
the new file does not exist already in this state and there exists
+ − 525
a parent file @{text "pf"} for the new file. The parent file is just
+ − 526
the tail of the list representing @{text f}. % if it exists
+ − 527
%(@{text "Some"}-case) or @{text None} if it does not.
+ − 528
Finally, the rule for cloning a process:
+ − 529
+ − 530
\begin{center}
+ − 531
@{thm[mode=Rule] osgrant10}
+ − 532
\end{center}
+ − 533
+ − 534
\noindent
+ − 535
Clearly the operating system should only allow to clone a process @{text p} if the
+ − 536
process is currently alive. The cloned process will get the process
+ − 537
ID generated by the function @{term new_proc}. This process ID should
+ − 538
not already exist. Therefore we define @{term new_proc} as
+ − 539
+ − 540
\begin{isabelle}\ \ \ \ \ %%%
+ − 541
\mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ − 542
@{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"}
+ − 543
\end{tabular}}
+ − 544
\end{isabelle}
+ − 545
+ − 546
\noindent
+ − 547
namely the highest ID currently in existence increased by one. The
+ − 548
admissibility rules for the other events impose similar conditions.
+ − 549
+ − 550
However, the admissibility check by the operating system is only one
+ − 551
``side'' of the constraints the RC-Model imposes. We also need to
+ − 552
model the constraints of the access policy. For this we introduce
+ − 553
separate @{text granted}-rules involving the sets @{text
+ − 554
permissions} and @{text "compatible r"}: the former contains triples
+ − 555
describing access control rules; the latter specifies for each role @{text r}
+ − 556
which roles are compatible with @{text r}. These sets are used in the
+ − 557
RC-Model when a process having a role @{text r} takes on a new role
+ − 558
@{text r'}. For example, a login-process might belong to root;
+ − 559
once the user logs in, however, the role of the process should change to
+ − 560
the user's default role. The corresponding @{text "granted"}-rule is
+ − 561
as follows
+ − 562
+ − 563
\begin{center}
+ − 564
@{thm[mode=Rule] rcgrant7}
+ − 565
\end{center}
+ − 566
+ − 567
\noindent
+ − 568
where we check whether the process @{text p} has currently role @{text r} and
+ − 569
whether the RC-policy states that @{text r'} is in the role compatibility
+ − 570
set of @{text r}.
+ − 571
+ − 572
The complication in the RC-Model arises from the
+ − 573
way how the current role of a process in a state @{text s} is
+ − 574
calculated---represented by the predicate @{term is_current_role} in our formalisation.
+ − 575
For defining this predicate we need to trace the role of a process from
+ − 576
the initial state to the current state. In the
+ − 577
initial state all processes have the role given by the function
+ − 578
@{term "init_current_role"}. If a @{term Clone} event happens then
+ − 579
the new process will inherit the role from the parent
+ − 580
process. Similarly, if a @{term ChangeRole} event happens, then
+ − 581
as seen in the rule above we just change the role accordingly. More interesting
+ − 582
is an @{term Execute} event in the RC-Model. For this event we have
+ − 583
to check the role attached to the file to be executed.
+ − 584
There are a number of cases: If the role of the file is a
+ − 585
\emph{normal} role, then the process will just take on this role
+ − 586
when executing the file (this is like the setuid mechanism in Unix). But
+ − 587
there are also four \emph{special} roles in the RC-Model:
+ − 588
@{term "InheritProcessRole"}, @{term "InheritUserRole"},
+ − 589
@{term "InheritParentRole"} and @{term
+ − 590
InheritUpMixed}. For example, if a file to be executed has
+ − 591
@{term "InheritProcessRole"} attached to it, then the process
+ − 592
that executes this file keeps its role regardless of the information
+ − 593
attached to the file. In this way programs can be can quarantined;
+ − 594
@{term "InheritUserRole"} can be used for login shells
+ − 595
to make sure they run with the user's default role.
+ − 596
The purpose of the other special roles is to determine the
+ − 597
role of a process according to the directory in which the
+ − 598
files are stored.
+ − 599
+ − 600
Having the notion of current role in place, we can define the
+ − 601
granted rule for the @{term Execute}-event: Suppose a process @{term
+ − 602
p} wants to execute a file @{text f}. The RC-Model first fetches the
+ − 603
role @{text r} of this process (in the current state @{text s}) and
+ − 604
the type @{text t} of the file. It then checks if the tuple @{term
+ − 605
"(r, t, EXECUTE)"} is part of the policy, that is in our
+ − 606
formalisation being an element in the set @{term compatible}. The
+ − 607
corresponding rule is as follows
+ − 608
+ − 609
\begin{center}
+ − 610
@{thm[mode=Rule] rcgrant4}
+ − 611
\end{center}
+ − 612
+ − 613
\noindent
+ − 614
The next @{text granted}-rule concerns the @{term CreateFile} event.
+ − 615
If this event occurs, then we have two rules in our RC-Model
+ − 616
depending on how the type of the created file is derived. If the type is inherited
+ − 617
from the parent directory @{text pf}, then the @{term granted}-rule is as follows:
+ − 618
+ − 619
\begin{center}
+ − 620
@{thm[mode=Rule] rcgrant1}
+ − 621
\end{center}
+ − 622
+ − 623
\noindent
+ − 624
We check whether @{term pf} is the parent file (directory) of @{text f} and check
+ − 625
whether the type of @{term pf} is @{term t}. We also need to fetch the
+ − 626
the role @{text r} of the process that seeks to get permission for creating
+ − 627
the file. If the default type of this role @{text r} states that the
+ − 628
type of the newly created file will be inherited from the parent file
+ − 629
type, then we only need to check that the policy states that @{text r}
+ − 630
has permission to write into the directory @{text pf}.
+ − 631
+ − 632
The situation is different if the default type of role @{text r} is
+ − 633
some \emph{normal} type, like text-file or executable. In such cases we want
+ − 634
that the process creates some predetermined type of files. Therefore in the
+ − 635
rule we have to check whether the role is allowed to create a file of that
+ − 636
type, and also check whether the role is allowed to write any new
+ − 637
file into the parent file (directory). The corresponding rule is
+ − 638
as follows.
+ − 639
+ − 640
\begin{center}
+ − 641
@{thm[mode=Rule] rcgrant1'}
+ − 642
\end{center}
+ − 643
+ − 644
\noindent
+ − 645
Interestingly, the type-information in the RC-model is also used for
+ − 646
processes, for example when they need to change their owner. For
+ − 647
this we have the rule
+ − 648
+ − 649
\begin{center}
+ − 650
@{thm[mode=Rule] rcgrant_CHO}
+ − 651
\end{center}
+ − 652
+ − 653
\noindent
+ − 654
whereby we have to obtain both the role and type of the process @{term p}, and then check
+ − 655
whether the policy allows a @{term ChangeOwner}-event for that role and type.
+ − 656
+ − 657
Overall we have 13 rules for the admissibility check by the operating system and
+ − 658
14 rules for the granted check by the RC-Model.
+ − 659
They are used to characterise when an event @{text e} is \emph{valid} to
+ − 660
occur in a state @{text s}. This can be inductively defined as the set of valid
+ − 661
states.
+ − 662
+ − 663
\begin{center}
+ − 664
\begin{tabular}{@ {}c@ {}}
+ − 665
\mbox{@{thm [mode=Axiom] valid.intros(1)}}\hspace{5mm}
+ − 666
\mbox{@{thm [mode=Rule] valid.intros(2)}}
+ − 667
\end{tabular}
+ − 668
\end{center}
+ − 669
+ − 670
The novel notion we introduce in this paper is the @{text tainted}
+ − 671
relation. It characterises how a system can become infected when
+ − 672
a file in the system contains, for example, a virus. We assume
+ − 673
that the initial state contains some tainted
+ − 674
objects (we call them @{term "seeds"}). Therefore in the initial state @{term "[]"}
+ − 675
an object is tainted, if it is an element in @{text "seeds"}.
+ − 676
+ − 677
\begin{center}
+ − 678
\mbox{@{thm [mode=Rule] tainted.intros(1)}}
+ − 679
\end{center}
+ − 680
+ − 681
\noindent
+ − 682
Let us first assume such a tainted object is a file @{text f}.
+ − 683
If a process reads or executes a tainted file, then this process becomes
+ − 684
tainted (in the state where the corresponding event occurs).
+ − 685
+ − 686
\begin{center}
+ − 687
\mbox{@{thm [mode=Rule] tainted.intros(3)}}\hspace{3mm}
+ − 688
\mbox{@{thm [mode=Rule] tainted.intros(6)}}
+ − 689
\end{center}
+ − 690
+ − 691
\noindent
+ − 692
We have a similar rule for a tainted IPC, namely
+ − 693
+ − 694
\begin{center}
+ − 695
\mbox{@{thm [mode=Rule] tainted.intros(9)}}
+ − 696
\end{center}
+ − 697
+ − 698
\noindent
+ − 699
which means if we receive anything from a tainted IPC, then
+ − 700
the process becomes tainted. A process is also tainted
+ − 701
when it is a produced by a @{text Clone}-event.
+ − 702
+ − 703
\begin{center}
+ − 704
\mbox{@{thm [mode=Rule] tainted.intros(2)}}
+ − 705
\end{center}
+ − 706
+ − 707
\noindent
+ − 708
However, the tainting relationship must also work in the
+ − 709
``other'' direction, meaning if a process is tainted, then
+ − 710
every file that is written or created will be tainted.
+ − 711
This is captured by the four rules:
+ − 712
+ − 713
\begin{center}
+ − 714
\begin{tabular}{c}
+ − 715
\mbox{@{thm [mode=Rule] tainted.intros(4)}} \hspace{3mm}
+ − 716
\mbox{@{thm [mode=Rule] tainted.intros(7)}} \medskip\\
+ − 717
\mbox{@{thm [mode=Rule] tainted.intros(5)}} \hspace{3mm}
+ − 718
\mbox{@{thm [mode=Rule] tainted.intros(8)}}
+ − 719
\end{tabular}
+ − 720
\end{center}
+ − 721
+ − 722
\noindent
+ − 723
Finally, we have three rules that state whenever an object is tainted
+ − 724
in a state @{text s}, then it will be still tainted in the
+ − 725
next state @{term "e#s"}, provided the object is still \emph{alive}
+ − 726
in that state. We have such a rule for each kind of objects, for
+ − 727
example for files the rule is:
+ − 728
+ − 729
\begin{center}
+ − 730
\mbox{@{thm [mode=Rule] tainted_10}}
+ − 731
\end{center}
+ − 732
+ − 733
\noindent
+ − 734
Similarly for alive processes and IPCs (then respectively with premises
+ − 735
@{term "p \<in> current_procs (e#s)"} and @{term "i \<in> current_ipcs (e#s)"}).
+ − 736
When an object present in the initial state can be tainted in
+ − 737
\emph{some} state (system run), we say it is @{text "taintable"}:
+ − 738
+ − 739
\begin{isabelle}\ \ \ \ \ %%%
+ − 740
\mbox{\begin{tabular}{lcl}
+ − 741
@{thm (lhs) taintable_def} & @{text "\<equiv>"} & @{term "init obj"} @{text "\<and>"} @{thm (rhs) taintable_def}
+ − 742
\end{tabular}}
+ − 743
\end{isabelle}
+ − 744
+ − 745
Before we can describe our static check deciding when a file is taintable, we
+ − 746
need to describe the notions @{term deleted} and @{term undeletable}
+ − 747
for objects. The former characterises whether there is an event that deletes
+ − 748
these objects (files, processes or IPCs). For this we have the following
+ − 749
four rules:
+ − 750
+ − 751
\begin{center}
+ − 752
\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+ − 753
\begin{tabular}{c}
+ − 754
@{thm [mode=Axiom] dels(1)}\\[-2mm]
+ − 755
@{thm [mode=Axiom] dels(2)}\\[-2mm]
+ − 756
@{thm [mode=Axiom] dels(3)}
+ − 757
\end{tabular} &
+ − 758
@{thm [mode=Rule] dels(4)}
+ − 759
\end{tabular}
+ − 760
\end{center}
+ − 761
+ − 762
+ − 763
\noindent
+ − 764
Note that an object cannot be deleted in the initial state @{text
+ − 765
"[]"}. An object is then said to be @{text "undeletable"} provided
+ − 766
it did exist in the initial state and there does not exists a valid
+ − 767
state in which the object is deleted:
+ − 768
+ − 769
\begin{isabelle}\ \ \ \ \ %%%
+ − 770
\mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+ − 771
@{thm (lhs) undeletable_def} & @{text "\<equiv>"} & %%@{thm (rhs) undeletable_def}
+ − 772
@{term "init obj \<and> \<not>(\<exists> s. (valid s \<and> deleted obj s))"}
+ − 773
\end{tabular}}
+ − 774
\end{isabelle}
+ − 775
+ − 776
\noindent
+ − 777
The point of this definition is that our static taintable check will only be
+ − 778
complete for undeletable objects. But these are
+ − 779
the ones system administrators are typically interested in (for
+ − 780
example system files). It should be clear, however, that we cannot
+ − 781
hope for a meaningful check by just trying out all possible
+ − 782
valid states in our dynamic model. The reason is that there are
+ − 783
potentially infinitely many of them and therefore the search space would be
+ − 784
infinite. For example staring from an
+ − 785
initial state containing a process @{text p} and a file @{text pf},
+ − 786
we can create files @{text "f\<^isub>1"}, @{text "f\<^isub>2"}, @{text "..."}
+ − 787
via @{text "CreateFile"}-events. This can be pictured roughly as follows:
+ − 788
+ − 789
\begin{center}
+ − 790
\begin{tabular}[t]{c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}cc}
+ − 791
\begin{tabular}[t]{c}
+ − 792
Initial state:\\
+ − 793
@{term "{p, pf}"}
+ − 794
\end{tabular} &
+ − 795
\begin{tabular}[t]{c}
+ − 796
\\
+ − 797
@{text "\<Longrightarrow>"}\\[2mm]
+ − 798
{\small@{term "CreateFile p (f\<^isub>1#pf)"}}
+ − 799
\end{tabular}
+ − 800
&
+ − 801
\begin{tabular}[t]{c}
+ − 802
\\
+ − 803
@{term "{p, pf, f\<^isub>1#pf}"}
+ − 804
\end{tabular}
+ − 805
&
+ − 806
\begin{tabular}[t]{c}
+ − 807
\\
+ − 808
@{text "\<Longrightarrow>"}\\[2mm]
+ − 809
{\small@{term "CreateFile p (f\<^isub>2#f\<^isub>1#pf)"}}
+ − 810
\end{tabular}
+ − 811
&
+ − 812
\begin{tabular}[t]{c}
+ − 813
\\
+ − 814
@{term "{p, pf, f\<^isub>1#pf, f\<^isub>2#f\<^isub>1#pf}"}
+ − 815
\end{tabular} &
+ − 816
\begin{tabular}[t]{c}
+ − 817
\\
+ − 818
@{text "..."}\\
+ − 819
\end{tabular}
+ − 820
\end{tabular}
+ − 821
\end{center}
+ − 822
+ − 823
\noindent
+ − 824
Instead, the idea of our static check is to use
+ − 825
the policies of the RC-model for generating an answer, since they
+ − 826
provide always a finite ``description of the system''. As we
+ − 827
will see in the next section, this needs some care, however.
+ − 828
*}
+ − 829
+ − 830
section {* Our Static Check *}
+ − 831
+ − 832
text {*
+ − 833
Assume there is a tainted file in the system and suppose we face the
+ − 834
problem of finding out whether this file can affect other files,
+ − 835
IPCs or processes? One idea is to work on the level of policies only, and
+ − 836
check which operations are permitted by the role and type of this
+ − 837
file. Then one builds the ``transitive closure'' of this information
+ − 838
and checks for example whether the role @{text root} has become
+ − 839
affected, in which case the whole system is compromised. This is indeed the solution investigated
+ − 840
in~\cite{guttman2005verifying} in the context of information flow
+ − 841
and SELinux.
+ − 842
+ − 843
Unfortunately, restricting the calculations to only use policies is
+ − 844
too simplistic for obtaining a check that is sound and complete---it
+ − 845
over-approximates the dynamic tainted relation defined in the previous
+ − 846
section. To see the problem consider
+ − 847
the case where the tainted file has, say, the type @{text bin}. If
+ − 848
the RC-policy contains a role @{text r} that can both read and write
+ − 849
@{text bin}-files, we would conclude that all @{text bin}-files can potentially
+ − 850
be tainted. That
+ − 851
is indeed the case, \emph{if} there is a process having this role @{text
+ − 852
r} running in the system. But if there is \emph{not}, then the
+ − 853
tainted file cannot ``spread''. A similar problem arises in case there
+ − 854
are two processes having the same role @{text r}, and this role is
+ − 855
restricted to read files only. Now if one of the processes is tainted, then
+ − 856
the simple check involving only policies would incorrectly infer
+ − 857
that all processes involving that role are tainted. But since the
+ − 858
policy for @{text r} is restricted to be read-only, there is in fact
+ − 859
no danger that both processes can become tainted.
+ − 860
+ − 861
The main idea of our sound and complete check is to find a ``middle'' ground between
+ − 862
the potentially infinite dynamic model and the too coarse
+ − 863
information contained in the RC-policies. Our solution is to
+ − 864
define a ``static'' version of the tainted relation, called @{term
+ − 865
"tainted_s"}, that records relatively precisely the information
+ − 866
about the initial state of the system (the one in which an object
+ − 867
might be a @{term seed} and therefore tainted). However,
+ − 868
we are less precise about the objects created in every subsequent
+ − 869
state. The result is that we can avoid the potential infinity of
+ − 870
the dynamic model.
+ − 871
For the @{term tainted_s}-relation we will consider the following
+ − 872
three kinds of \emph{items} recording the information we need about
+ − 873
processes, files and IPCs, respectively:
+ − 874
+ − 875
\begin{center}
+ − 876
\begin{tabular}{l@ {\hspace{5mm}}l}
+ − 877
& Recorded information:\smallskip\\
+ − 878
Processes: & @{term "SProc (r, dr, t, u) po"}\\
+ − 879
Files: & @{term "SFile (t, a) fo"}\\
+ − 880
IPCs: & @{term "SIPC (t) io"}
+ − 881
\end{tabular}
+ − 882
\end{center}
+ − 883
+ − 884
\noindent
+ − 885
For a process we record its role @{text r}, its default role @{text dr} (used to determine
+ − 886
the role when executing a file or changing the owner of a process), its type @{text t}
+ − 887
and its owner @{text u}. For a file we record
+ − 888
just the type @{text t} and its @{term "source_dir"} @{text a} (we define this
+ − 889
notion shortly). For IPCs we only record its type @{text t}. Note the superscripts
+ − 890
@{text po}, @{text fo} and @{text io} in each item. They are optional arguments and depend on
+ − 891
whether the corresponding object is present in the initial state or not.
+ − 892
If it \emph{is}, then for processes and IPCs we will record @{term "Some(id)"},
+ − 893
where @{text id} is the natural number that uniquely identifies a process or IPC;
+ − 894
for files we just record their path @{term "Some(f)"}. If the object is
+ − 895
\emph{not} present in the initial state, that is newly created, then we just have
+ − 896
@{term None} as superscript.
+ − 897
Let us illustrate the different superscripts with the following example
+ − 898
where the initial state contains a process @{term p} and a file (directory)
+ − 899
@{term pf}. Then this
+ − 900
process creates a file via a @{term "CreateFile"}-event and after that reads
+ − 901
the created file via a @{term Read}-event:
+ − 902
+ − 903
\begin{center}
+ − 904
\begin{tabular}[t]{ccccc}
+ − 905
\begin{tabular}[t]{c}
+ − 906
Initial state:\\
+ − 907
@{term "{p, pf}"}
+ − 908
\end{tabular} &
+ − 909
\begin{tabular}[t]{c}
+ − 910
\\
+ − 911
@{text "\<Longrightarrow>"}\\
+ − 912
{\small@{term "CreateFile p (f#pf)"}}
+ − 913
\end{tabular}
+ − 914
&
+ − 915
\begin{tabular}[t]{c}
+ − 916
\\
+ − 917
@{term "{p, pf, f#pf}"}
+ − 918
\end{tabular}
+ − 919
&
+ − 920
\begin{tabular}[t]{c}
+ − 921
\\
+ − 922
@{text "\<Longrightarrow>"}\\
+ − 923
{\small@{term "ReadFile p (f#pf)"}}
+ − 924
\end{tabular}
+ − 925
&
+ − 926
\begin{tabular}[t]{c}
+ − 927
\\
+ − 928
@{term "{p, pf, f#pf}"}
+ − 929
\end{tabular}
+ − 930
\end{tabular}
+ − 931
\end{center}
+ − 932
+ − 933
\noindent
+ − 934
For the two objects in the initial state our static check records
+ − 935
the information @{term "SProc (r, dr, t, u) (Some(p))"} and @{term
+ − 936
"SFile (t', a) (Some(pf))"} (assuming @{text "r"}, @{text t} and so
+ − 937
on are the corresponding roles, types etc). In both cases we have
+ − 938
the superscript @{text "Some(...)"} since they are objects present
+ − 939
in the initial state. For the file @{term "f#pf"} created by the
+ − 940
@{term "CreateFile"}-event, we record @{term "SFile (t', a')
+ − 941
(None)"}, since it is a newly created file. The @{text
+ − 942
"ReadFile"}-event does not change the set of objects, therefore no
+ − 943
new information needs to be recorded. The problem we are avoiding
+ − 944
with this setup of recording the precise information for the initial
+ − 945
state is where two processes have the same role and type
+ − 946
information, but only one is tainted in the initial state, but the
+ − 947
other is not. The recorded unique process IDs allows us to
+ − 948
distinguish between both processes. For all newly created objects,
+ − 949
on the other hand, we do not care. This is crucial, because
+ − 950
otherwise exploring all possible ``reachable'' objects can lead to
+ − 951
the potential infinity like in the dynamic model.
+ − 952
+ − 953
An @{term source_dir} for a file is the ``nearest'' directory that
+ − 954
is present in the initial state and has not been deleted in a state
+ − 955
@{text s}. Its definition is the recursive function
+ − 956
+ − 957
\begin{isabelle}\ \ \ \ \ %%%
+ − 958
\mbox{\begin{tabular}{lcl}
+ − 959
@{thm (lhs) source_dir.simps(1)} & @{text "\<equiv>"} \;\; &
+ − 960
@{text "if"} @{text "\<not> deleted [] s"} @{text "then"} @{term "Some []"} @{text "else"} @{term "None"}\\
+ − 961
@{thm (lhs) source_dir.simps(2)} & @{text "\<equiv>"} &
+ − 962
@{text "if"} @{term "(f#pf) \<in> init_files \<and> \<not>(deleted (File (f#pf)) s)"}\\
+ − 963
& & @{text "then"} @{term "Some (f#pf)"} @{text "else"} @{term "source_dir s pf"}\\
+ − 964
\end{tabular}}
+ − 965
\end{isabelle}
+ − 966
+ − 967
\noindent
+ − 968
generating an optional value.
+ − 969
The first clause states that the anchor of the @{text
+ − 970
root}-directory is always its own anchor unless it has been
+ − 971
deleted. If a file is present in the initial state and not deleted
+ − 972
in @{text s}, then it is also its own anchor, otherwise the anchor
+ − 973
will be the anchor of the parent directory. For example if we have
+ − 974
a directory @{text pf} in the initial state, then its anchor is @{text "Some pf"}
+ − 975
(assuming it is not deleted). If we create a new file in this directory,
+ − 976
say @{term "f#pf"}, then its anchor will also be @{text "Some pf"}.
+ − 977
The purpose of @{term source_dir} is to determine the
+ − 978
role information when a file is executed, because the role of the
+ − 979
corresponding process, according to the RC-model, is determined by the role information of the
+ − 980
anchor of the file to be executed.
+ − 981
+ − 982
There is one last problem we have to solve before we can give the
+ − 983
rules of our @{term "tainted_s"}-check. Suppose an RC-policy
+ − 984
includes the rule @{text "(r, foo, Write) \<in> permissions"}, that is
+ − 985
a process of role @{text "r"} is allowed to write files of type @{text "foo"}.
+ − 986
If there is a tainted process with this role, we would conclude that
+ − 987
also every file of that type can potentially become tainted. However, that
+ − 988
is not the case if the initial state does not contain any file
+ − 989
with type @{text foo} and the RC-policy does not allow the
+ − 990
creation of such files, that is does not contain an access rule
+ − 991
@{text "(r, foo, Create) \<in> permissions"}. In a sense the original
+ − 992
@{text "(r, foo, Write)"} is ``useless'' and should not contribute
+ − 993
to the relation characterising the objects that are tainted.
+ − 994
To exclude such ``useless'' access rules, we define
+ − 995
a relation @{term "all_sobjs"} restricting our search space
+ − 996
to only configurations that correspond to states in our dynamic model.
+ − 997
We first have a rule for reachable items of the form @{text "F(t, f)\<^bsup>Some f\<^esup>"}
+ − 998
where the file @{text f} with type @{text t} is present in
+ − 999
the initial state.
+ − 1000
+ − 1001
\begin{center}
+ − 1002
@{thm [mode=Rule] af_init'}
+ − 1003
\end{center}
+ − 1004
+ − 1005
\noindent
+ − 1006
We have similar reachability rules for processes and IPCs that are part of the
+ − 1007
initial state. Next is the reachability rule in case a file is created
+ − 1008
+ − 1009
\begin{center}
+ − 1010
@{thm [mode=Rule] af_cfd[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ − 1011
\end{center}
+ − 1012
+ − 1013
\noindent
+ − 1014
where we require that we have a reachable parent directory, recorded
+ − 1015
as @{text "F(t, a)\<^bsup>fo\<^esup>"}, and also a
+ − 1016
process that can create the file, recorded as @{text "P(r, dr, pt,
+ − 1017
u)\<^bsup>po\<^esup>"}. As can be seen, we also require that we have both @{text "(r, t,
+ − 1018
Write)"} and \mbox{@{text "(r, t', Create)"}} in the @{text permissions} set
+ − 1019
for this rule to apply. If we did \emph{not} impose this requirement
+ − 1020
about the RC-policy, then there would be no way to create a file
+ − 1021
with @{term "NormalFileType t'"} according to our ``dynamic'' model.
+ − 1022
However in case we want to create a
+ − 1023
file of type @{term InheritPatentType}, then we only need the access-rule
+ − 1024
@{text "(r, t, Write)"}:
+ − 1025
+ − 1026
\begin{center}
+ − 1027
@{thm [mode=Rule] af_cfd'[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ − 1028
\end{center}
+ − 1029
+ − 1030
\noindent
+ − 1031
We also have reachability rules for processes executing files, and
+ − 1032
for changing their roles and owners, for example
+ − 1033
+ − 1034
\begin{center}
+ − 1035
@{thm [mode=Rule] ap_crole[where sp="po" and fr="dr"]}
+ − 1036
\end{center}
+ − 1037
+ − 1038
\noindent
+ − 1039
which states that when we have a process with role @{text r}, and the role
+ − 1040
@{text "r'"} is in the corresponding role-compatibility set, then also
+ − 1041
a process with role @{text "r'"} is reachable.
+ − 1042
+ − 1043
The crucial difference between between the ``dynamic'' notion of validity
+ − 1044
and the ``static'' notion of @{term "all_sobjs"}
+ − 1045
is that there can be infinitely many valid states, but assuming the initial
+ − 1046
state contains only finitely many objects, then also @{term "all_sobjs"} will
+ − 1047
be finite. To see the difference, consider the infinite ``chain'' of events
+ − 1048
just cloning a process @{text "p\<^isub>0"}:
+ − 1049
+ − 1050
\begin{center}
+ − 1051
\begin{tabular}[t]{c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}cc}
+ − 1052
\begin{tabular}[t]{c}
+ − 1053
Initial state:\\
+ − 1054
@{term "{p\<^isub>0}"}
+ − 1055
\end{tabular} &
+ − 1056
\begin{tabular}[t]{c}
+ − 1057
\\
+ − 1058
@{text "\<Longrightarrow>"}\\[2mm]
+ − 1059
{\small@{term "Clone p\<^isub>0 p\<^isub>1"}}
+ − 1060
\end{tabular}
+ − 1061
&
+ − 1062
\begin{tabular}[t]{c}
+ − 1063
\\
+ − 1064
@{term "{p\<^isub>0, p\<^isub>1}"}
+ − 1065
\end{tabular}
+ − 1066
&
+ − 1067
\begin{tabular}[t]{c}
+ − 1068
\\
+ − 1069
@{text "\<Longrightarrow>"}\\[2mm]
+ − 1070
{\small@{term "Clone p\<^isub>0 p\<^isub>2"}}
+ − 1071
\end{tabular}
+ − 1072
&
+ − 1073
\begin{tabular}[t]{c}
+ − 1074
\\
+ − 1075
@{term "{p\<^isub>0, p\<^isub>1, p\<^isub>2}"}
+ − 1076
\end{tabular} &
+ − 1077
\begin{tabular}[t]{c}
+ − 1078
\\
+ − 1079
@{text "..."}\\
+ − 1080
\end{tabular}
+ − 1081
\end{tabular}
+ − 1082
\end{center}
+ − 1083
+ − 1084
\noindent
+ − 1085
The corresponding reachable objects are
+ − 1086
+ − 1087
\begin{center}
+ − 1088
\begin{tabular}[t]{cccc}
+ − 1089
\begin{tabular}[t]{c}
+ − 1090
@{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>}"}
+ − 1091
\end{tabular} &
+ − 1092
\begin{tabular}[t]{c}
+ − 1093
@{text "\<Longrightarrow>"}
+ − 1094
\end{tabular}
+ − 1095
&
+ − 1096
\begin{tabular}[t]{c}
+ − 1097
@{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>, P(r, dr, t, u)\<^bsup>None\<^esup>}"}
+ − 1098
\end{tabular}
+ − 1099
\end{tabular}
+ − 1100
\end{center}
+ − 1101
+ − 1102
\noindent
+ − 1103
where no further progress can be made because the information
+ − 1104
recorded about @{text "p\<^isub>2"}, @{text "p\<^isub>3"} and so on is just the same
+ − 1105
as for @{text "p\<^isub>1"}, namely @{text "P(r, dr, t, u)\<^bsup>None\<^esup>"}. Indeed we
+ − 1106
can prove the lemma:
+ − 1107
+ − 1108
\begin{lemma}\label{finite}
+ − 1109
If @{text "finite init"}, then @{term "finite all_sobjs"}.
+ − 1110
\end{lemma}
+ − 1111
+ − 1112
\noindent
+ − 1113
This fact of @{term all_sobjs} being finite enables us to design a
+ − 1114
decidable tainted-check. For this we introduce inductive rules defining the
+ − 1115
set @{term "tainted_s"}. Like in the ``dynamic'' version of tainted,
+ − 1116
if an object is element of @{text seeds}, then it is @{term "tainted_s"}.
+ − 1117
+ − 1118
\begin{center}
+ − 1119
@{thm [mode=Rule] ts_init}
+ − 1120
\end{center}
+ − 1121
+ − 1122
\noindent
+ − 1123
The function @{text "\<lbrakk>_\<rbrakk>"} extracts the static information from an object.
+ − 1124
For example for a process it extracts the role, default role, type and
+ − 1125
user; for a file the type and the anchor. If a process in tainted and creates
+ − 1126
a file with a normal type @{text "t'"} then also the created file
+ − 1127
is tainted. The corresponding rule is
+ − 1128
+ − 1129
\begin{center}
+ − 1130
@{thm [mode=Rule] ts_cfd[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ − 1131
\end{center}
+ − 1132
+ − 1133
\noindent
+ − 1134
If a tainted process creates a file that inherits the type of the directory,
+ − 1135
then the file will also be tainted:
+ − 1136
+ − 1137
\begin{center}
+ − 1138
@{thm [mode=Rule] ts_cfd'[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ − 1139
\end{center}
+ − 1140
+ − 1141
\noindent
+ − 1142
If a tainted process changes its role, then also with this changed role
+ − 1143
it will be tainted:
+ − 1144
+ − 1145
\begin{center}
+ − 1146
@{thm [mode=Rule] ts_crole[where pt=t and sp="po" and fr="dr"]}
+ − 1147
\end{center}
+ − 1148
+ − 1149
\noindent
+ − 1150
Similarly when a process changes its owner. If a file is tainted, and
+ − 1151
a process has read-permission to that type of files, then the
+ − 1152
process becomes tainted. The corresponding rule is
+ − 1153
+ − 1154
\begin{center}
+ − 1155
@{thm [mode=Rule] ts_read[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ − 1156
\end{center}
+ − 1157
+ − 1158
\noindent
+ − 1159
If a process is tainted and it has write-permission for files of type @{text t},
+ − 1160
then these files will be tainted:
+ − 1161
+ − 1162
\begin{center}
+ − 1163
@{thm [mode=Rule] ts_write[where sd=a and sf="fo" and sp="po" and fr="dr"]}
+ − 1164
\end{center}
+ − 1165
+ − 1166
\noindent
+ − 1167
We omit the remaining rules for executing a file, cloning a process and
+ − 1168
rules involving IPCs, which are similar. A simple consequence of our definitions
+ − 1169
is that every tainted object is also reachable:
+ − 1170
+ − 1171
\begin{lemma}
+ − 1172
@{text "tainted\<^isup>s \<subseteq> reachable\<^isup>s"}
+ − 1173
\end{lemma}
+ − 1174
+ − 1175
\noindent
+ − 1176
which in turn means that the set of @{term "tainted_s"} items is finite by Lemma~\ref{finite}.
+ − 1177
+ − 1178
Returning to our original question about whether tainted objects can spread
+ − 1179
in the system. To answer this question, we take these tainted objects as
+ − 1180
seeds and calculate the set of items that are @{term "tainted_s"}. We proved this
+ − 1181
set is finite and can be enumerated using the rules for @{term tainted_s}.
+ − 1182
However, this set is about items, not about whether objects are tainted or not.
+ − 1183
Assuming an item in @{term tainted_s} arises from an object present in the initial
+ − 1184
state, we have recorded enough information to translate items back into objects
+ − 1185
via the function @{text "|_|"}:
+ − 1186
+ − 1187
\begin{center}
+ − 1188
\begin{tabular}{lcl}
+ − 1189
@{text "|P(r, dr, t, u)\<^bsup>po\<^esup>|"} & @{text "\<equiv>"} & @{text po}\\
+ − 1190
@{text "|F(t, a)\<^bsup>fo\<^esup>|"} & @{text "\<equiv>"} & @{text fo}\\
+ − 1191
@{text "|I(t\<^bsup>\<^esup>)\<^bsup>io\<^esup>|"} & @{text "\<equiv>"} & @{text io}
+ − 1192
\end{tabular}
+ − 1193
\end{center}
+ − 1194
+ − 1195
\noindent
+ − 1196
Using this function, we can define when an object is @{term taintable_s} in terms of
+ − 1197
an item being @{term tainted_s}, namely
+ − 1198
+ − 1199
\begin{isabelle}\ \ \ \ \ %%%
+ − 1200
\mbox{\begin{tabular}{lcl}
+ − 1201
@{thm (lhs) taintable_s_def} & @{text "\<equiv>"} & @{text "\<exists>item. item \<in> tainted\<^isup>s \<and> |item| = Some obj"}
+ − 1202
\end{tabular}}
+ − 1203
\end{isabelle}
+ − 1204
+ − 1205
\noindent
+ − 1206
Note that @{term taintable_s} is only about objects that are present in
+ − 1207
the initial state, because for all other items @{text "|_|"} returns @{text None}.
+ − 1208
+ − 1209
+ − 1210
With these definitions in place, we can state our theorem about the soundness of our
+ − 1211
static @{term taintable_s}-check for objects.
+ − 1212
+ − 1213
\begin{theorem}[Soundness]
+ − 1214
@{thm [mode=IfThen] static_sound}
+ − 1215
\end{theorem}
+ − 1216
+ − 1217
\noindent
+ − 1218
The proof of this theorem generates for every object that is ``flagged'' as
+ − 1219
@{term taintable_s} by our check, a sequence of events which shows how the
+ − 1220
object can become tainted in the dynamic model. We can also state a completeness
+ − 1221
theorem for our @{term taintable_s}-check.
+ − 1222
+ − 1223
\begin{theorem}[Completeness]
+ − 1224
@{thm [mode=IfThen] static_complete}
+ − 1225
\end{theorem}
+ − 1226
+ − 1227
\noindent
+ − 1228
This completeness theorem however needs to be restricted to
+ − 1229
undeletebale objects. The reason is that a tainted process can be
+ − 1230
killed by another process, and after that can be ``recreated'' by a
+ − 1231
cloning event from an untainted process---remember we have no control
+ − 1232
over which process ID a process will be assigned with. Clearly, in
+ − 1233
this case the cloned process should be considered untainted, and
+ − 1234
indeed our dynamic tainted relation is defined in this way. The
+ − 1235
problem is that a static test cannot know about a process being
+ − 1236
killed and then recreated. Therefore the static test will not be
+ − 1237
able to ``detect'' the difference. Therefore we solve this problem
+ − 1238
by considering only objects that are present in the initial state
+ − 1239
and cannot be deleted. By the latter we mean that the RC-policy
+ − 1240
stipulates an object cannot be deleted (for example it has been created
+ − 1241
by @{term root} in single-user mode, but in the everyday running
+ − 1242
of the system the RC-policy forbids to delete an object belonging to
+ − 1243
@{term root}). Like @{term "taintable_s"}, we also have a static check
+ − 1244
for when a file is undeletable according to an RC-policy.
+ − 1245
+ − 1246
This restriction to undeletable objects might be seen as a great
+ − 1247
weakness of our result, but in practice this seems to cover the
+ − 1248
interesting scenarios encountered by system administrators. They
+ − 1249
want to know whether a virus-infected file introduced by a user can
+ − 1250
affect the core system files. Our test allows the system
+ − 1251
administrator to find this out provided the RC-policy makes the core
+ − 1252
system files undeletable. We assume that this provisio is already part
+ − 1253
of best practice rule for running a system.
+ − 1254
+ − 1255
We envisage our test to be useful in two kind of situations: First, if
+ − 1256
there was a break-in into a system, then, clearly, the system
+ − 1257
administrator can find out whether the existing access policy was
+ − 1258
strong enough to contain the break-in, or whether core system files
+ − 1259
could have been affected. In the first case, the system
+ − 1260
administrator can just plug the hole and forget about the break-in;
+ − 1261
in the other case the system administrator is wise to completely
+ − 1262
reinstall the system.
+ − 1263
Second, the system administrator can proactively check whether an
+ − 1264
RC-policy is strong enough to withstand serious break-ins. To do so
+ − 1265
one has to identify the set of ``core'' system files that the policy
+ − 1266
should protect and mark every possible entry point for an attacker
+ − 1267
as tainted (they are the seeds of the @{term "tainted_s"} relation).
+ − 1268
Then the test will reveal
+ − 1269
whether the policy is strong enough or needs to be redesigned. For
+ − 1270
this redesign, the sequence of events our check generates should be
+ − 1271
informative.
+ − 1272
*}
+ − 1273
+ − 1274
+ − 1275
+ − 1276
+ − 1277
+ − 1278
section {*Conclusion and Related Works*}
+ − 1279
+ − 1280
+ − 1281
text {*
+ − 1282
We have presented the first completely formalised dynamic model of
+ − 1283
the Role-Compa\-tibility Model. This is a framework, introduced by Ott
+ − 1284
\cite{ottrc}, in which role-based access control policies
+ − 1285
can be formulated and is used in practice, for example, for securing Apache
+ − 1286
servers. Previously, the RC-Model was presented as a
+ − 1287
collection of rules partly given in ``English'', partly given as formulas.
+ − 1288
During the formalisation we uncovered an inconsistency in the
+ − 1289
semantics of the special role @{term "InheritParentRole"} in
+ − 1290
the existing works about the RC-Model \cite{ottrc,ottweb}. By proving
+ − 1291
the soundness and completeness of our static @{term
+ − 1292
"taintable_s"}-check, we have formally related the dynamic behaviour
+ − 1293
of the operating system implementing access control and the static
+ − 1294
behaviour of the access policies of the RC-Model. The
+ − 1295
crucial idea in our static check is to record precisely the
+ − 1296
information available about the initial state (in which some resources might be
+ − 1297
tainted), but be less precise
+ − 1298
about the subsequent states. The former fact essentially gives us
+ − 1299
the soundness of our check, while the latter results in a finite
+ − 1300
search space.
+ − 1301
+ − 1302
The two most closely related works are by Archer et al and by Guttman et al
+ − 1303
\cite{Archer03,guttman2005verifying}. The first describes a
+ − 1304
formalisation of the dynamic behaviour of SELinux carried out in the
+ − 1305
theorem prover PVS. However, they cannot use their formalisation in
+ − 1306
order to prove any ``deep'' properties about access control rules
+ − 1307
\cite[Page 167]{Archer03}. The second analyses access control
+ − 1308
policies in the context of information flow. Since this work
+ − 1309
is completely on the level of policies, it does
+ − 1310
not lead to a sound and complete check for files being taintable (a dynamic notion
+ − 1311
defined in terms of operations performed by the operating system).
+ − 1312
While our results concern the RC-Model, we expect that they
+ − 1313
equally apply to the access control model of SELinux. In fact,
+ − 1314
we expect that the formalisation is simpler for SELinux, since
+ − 1315
its rules governing roles are much simpler than in the RC-Model.
+ − 1316
The definition of our admissibility rules can be copied verbatim for SELinux;
+ − 1317
we would need to modify our granted rules and slightly adapt our
+ − 1318
static check. We leave this as future work.
+ − 1319
+ − 1320
+ − 1321
Our formalisation is carried out in the Isabelle/HOL theorem prover.
+ − 1322
It uses Paulson's inductive method for
+ − 1323
reasoning about sequences of events \cite{Paulson98}.
+ − 1324
We have approximately 1000 lines of code for definitions and 6000 lines of
+ − 1325
code for proofs. Our formalisation is available from the
+ − 1326
Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/rc/}.\\[-12mm]
+ − 1327
+ − 1328
+ − 1329
% 0. Not Policy-Analysis: cause even policy is analysed correct, there is still a gap between it and policy application to the real Access Control system. Hence here Our dynamic model is bridging this gap. Policy-Analysis "basic" based on "Information flow", but it is not enough: the static "write" right to a certain typed file do not mean a process having this right definitely can write the file, it has to pass a "particular" "Control Flow" to achieve the state of "There are this typed file and this righted process"!
+ − 1330
% 1. Both Dynamic and Statical analysis, and proved link between two \\
+ − 1331
% 2. Tainting Relation Formalisation \\
+ − 1332
% 3. Formalisation and Verification than Model Checking \\
+ − 1333
% 4. Universal Checker of Policy \\
+ − 1334
% 5. source of RC rules made more precise \\
+ − 1335
% 6. RC example of Webserver with CGIs (key notion: Program Based Roles) \\
+ − 1336
% 7. RBAC is more Policy-lever(with HUGE companies, many stablised num of roles but frequently varifying num of users); RC is more Program Base Roles, set for system with a lot of program based default value, once pre-setted, it will remains after running. which is key to policy checker.
+ − 1337
+ − 1338
%The distinct feature of RC is to deal with program based roles, such as server behaviour.
+ − 1339
%This is in contrast to usual RSBAC models where roles are modeled around a hierachy, for
+ − 1340
%example in a company.
+ − 1341
+ − 1342
+ − 1343
%In a word, what the manager need is that given the
+ − 1344
%initial state of the system, a policy checker that make sure the under the policy
+ − 1345
%he made, this important file cannot: 1. be deleted; 2. be tainted.
+ − 1346
%Formally speaking, this policy-checker @{text "PC"} (a function that given the
+ − 1347
%initial state of system, a policy and an object, it tells whether this object
+ − 1348
%will be fully protected or not) should satisfy this criteria:
+ − 1349
+ − 1350
% @{text "(PC init policy obj) \<and> (exists init obj) \<longrightarrow> \<not> taintable obj"}
+ − 1351
%If the @{text obj} exists in the initial-state, and @{text "PC"} justify the safety
+ − 1352
%of this object under @{text "policy"}, this object should not be @{text taintable}.
+ − 1353
%We call this criteria the \emph{completeness} of @{text "PC"}.
+ − 1354
%And there is the \emph{soundness} criteria of @{text "PC"} too, otherwise a "NO-to-ALL"
+ − 1355
%answer always satisfy the \emph{completeness}. \emph{soundness} formally is:
+ − 1356
% @{text "PC init policy obj \<longrightarrow> taintable obj"}
+ − 1357
+ − 1358
%This policy-checker should satisfy other properties:
+ − 1359
% 1. fully statical, that means this policy-checker should not rely on the system
+ − 1360
%running information, like new created files/process, and most importantly the
+ − 1361
%trace of system running.
+ − 1362
% 2. decidable, that means this policy-checker should always terminate.
+ − 1363
+ − 1364
+ − 1365
% The purpose of an operating system is to provide a common
+ − 1366
% interface for accessing resources. This interface is typically
+ − 1367
% realised as a collection of system calls, for example for reading
+ − 1368
% and writing files, forking of processes, or sending and receiving
+ − 1369
% messages. Role based access control is one approach for
+ − 1370
% restricting access to such system calls: if a user has
+ − 1371
% suffient rights, then a system call can be performed.
+ − 1372
+ − 1373
% a user might have
+ − 1374
% one or more roles and acces is granted if the role has sufficent
+ − 1375
% rights
+ − 1376
+ − 1377
% static world...make predictions about accessing
+ − 1378
% files, do they translate into actual systems behaviour.
+ − 1379
+ − 1380
+ − 1381
*}
+ − 1382
+ − 1383
+ − 1384
(*<*)
+ − 1385
end
+ − 1386
+ − 1387
end
+ − 1388
(*>*)
+ − 1389
+ − 1390
(*
+ − 1391
+ − 1392
Central to RC-Model is the roles and types. We start with do formalisation on
+ − 1393
types first.
+ − 1394
+ − 1395
\begin{isabelle}\ \ \ \ \ %%%
+ − 1396
\mbox{
+ − 1397
\begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{2mm}}l}
+ − 1398
@{text t_client} & @{text "="} & @{text "Christian"} \\
+ − 1399
& @{text "|"} & @{text "Chunhan"} \\
+ − 1400
& @{text "|"} & @{text " ... "} \\
+ − 1401
\end{tabular}}
+ − 1402
+ − 1403
\mbox{
+ − 1404
\begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{2mm}}l@ {\hspace{2mm}}l}
+ − 1405
@{text t_normal_file_type} & @{text "="} & @{text "WebServerLog_file"} & \\
+ − 1406
& @{text "|"} & @{text "WebData_file"} & @{text t_client} \\
+ − 1407
& @{text "|"} & @{text "CGI_file"} & @{text t_client} \\
+ − 1408
& @{text "|"} & @{text "Private_file"} & @{text t_client}
+ − 1409
\end{tabular}}
+ − 1410
+ − 1411
\mbox{
+ − 1412
\begin{tabular} {r@ {\hspace{1mm}}l@ {\hspace{5mm}}l}
+ − 1413
@{text t_rc_file_type}
+ − 1414
& @{text "="} & @{term "InheritParent_file_type"} \\
+ − 1415
& @{text "|"} & @{term "NormalFile_type t_normal_file_type"}
+ − 1416
\end{tabular}}
+ − 1417
\end{isabelle}
+ − 1418
+ − 1419
@{term "type_of_file"} function calculates the current type for the files:
+ − 1420
\begin{isabelle}\ \ \ \ \ %%%
+ − 1421
\mbox{\begin{tabular}{lcl}
+ − 1422
@{thm (lhs) type_of_file.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) type_of_file.simps(1)}\\
+ − 1423
@{thm (lhs) type_of_file.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) type_of_file.simps(2)}\\
+ − 1424
@{term "type_of_file (DUMMY#s)"} & @{text "\<equiv>"} & @{term "type_of_file s"}
+ − 1425
\end{tabular}}
+ − 1426
\end{isabelle}
+ − 1427
+ − 1428
Note that this @{term "type_of_file"} is not the function @{term "etype_of_file"}
+ − 1429
that we call in the grant check of RC-Model, @{term "rc_grant"}. The reason is
+ − 1430
that file's type can be set to a special type of @{term "InheritParent_file_type"},
+ − 1431
means that the ``efficient'' type of this file is the efficient type of its directory.
+ − 1432
\mbox{\begin{tabular}{lcl}
+ − 1433
@{thm (lhs) etype_aux.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) etype_aux.simps(1)}\\
+ − 1434
@{thm (lhs) etype_aux.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) etype_aux.simps(2)}\smallskip\\
+ − 1435
@{thm (lhs) etype_of_file_def} & @{text "\<equiv>"} & @{thm (rhs) etype_of_file_def}
+ − 1436
\end{tabular}}
+ − 1437
Here @{term etype_aux} is an auxiliary function which do recursion
+ − 1438
on the pathname of files. By the way, in our proofs, we do proved
+ − 1439
that functions like @{term "etype_of_file"} will always return
+ − 1440
``normal'' values.
+ − 1441
+ − 1442
+ − 1443
We have similar observation functions calculating the current type for processes
+ − 1444
and IPCs too, only diffence here is that there is no ``effcient'' type here for
+ − 1445
processes and IPCs, all types that calculated by @{term "type_of_process"} and
+ − 1446
@{term "type_of_ipc"} are alrealdy efficient types.
+ − 1447
+ − 1448
*}
+ − 1449
+ − 1450
text {*
+ − 1451
\begin{isabelle}\ \ \ \ \ %%%
+ − 1452
\mbox{
+ − 1453
\begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{2mm}}l@ {\hspace{2mm}}l}
+ − 1454
@{text t_normal_role} & @{text "="} & @{text "WebServer"} & \\
+ − 1455
& @{text "|"} & @{text "WS_client"} & @{text t_client} \\
+ − 1456
& @{text "|"} & @{text "UpLoader"} & @{text t_client} \\
+ − 1457
& @{text "|"} & @{text "CGI "} & @{text t_client}
+ − 1458
\end{tabular}}
+ − 1459
+ − 1460
\mbox{
+ − 1461
\begin{tabular} {r@ {\hspace{1mm}}l@ {\hspace{2mm}}l@ {\hspace{5mm}}l}
+ − 1462
@{text t_role}
+ − 1463
& @{text "="} & @{term "InheritParentRole"} & ``for file's initial/forced role,
+ − 1464
meaning using parent directory's
+ − 1465
role instead'' \\
+ − 1466
& @{text "|"} & @{term "UseForcedRole"} & ``for file's initial role'' \\
+ − 1467
& @{text "|"} & @{term "InheritProcessRole"} & ``using process' current role''\\
+ − 1468
& @{text "|"} & @{term "InheritUserRole"} & ``using owner's default role''\\
+ − 1469
& @{text "|"} & ... & \\
+ − 1470
& @{text "|"} & @{term "NormalRole t_normal_role"} & ``user-defined
+ − 1471
policy roles"
+ − 1472
\end{tabular}}
+ − 1473
\end{isabelle}
+ − 1474
+ − 1475
@{text "t_normal roles"} are normally user-defined roles in the
+ − 1476
policy, where @{text "WebServer"} is the role who plays for the
+ − 1477
server, while @{text "WS_client"} is the role server plays for
+ − 1478
certain client, so is for @{text "UpLoader"} role. @{text "CGI"} is
+ − 1479
the role that client's programme scripts play.
+ − 1480
+ − 1481
@{term "currentrole"} function calculates the current role of process, here we
+ − 1482
only show 3 cases of its definition, it responses to @{term "ChangeOwner"},
+ − 1483
@{term "ChangeRole"} events too.
+ − 1484
+ − 1485
\begin{isabelle}\ \ \ \ \ %%%
+ − 1486
\mbox{\begin{tabular}{lcl}
+ − 1487
@{thm (lhs) currentrole.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) currentrole.simps(1)}\\
+ − 1488
@{thm (lhs) currentrole.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) currentrole.simps(2)}\\
+ − 1489
@{thm (lhs) currentrole.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) currentrole.simps(3)}
+ − 1490
\end{tabular}}
+ − 1491
\end{isabelle}
+ − 1492
+ − 1493
If the event trace is @{term "[]"}, means the
+ − 1494
system state currently is the initial state, then @{term "init_currentrole"} will
+ − 1495
do. @{term "Execute p f"} event is one complex case, when this event happens, process
+ − 1496
@{term p}'s role will be changed according to the efficient initial role of the
+ − 1497
executable file @{term f}, here ``efficient'' is like the file's type too.
+ − 1498
+ − 1499
\begin{isabelle}\ \ \ \ \ %%%
+ − 1500
\mbox{\begin{tabular}{lcl}
+ − 1501
@{thm (lhs) initialrole.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) initialrole.simps(1)}\\
+ − 1502
@{thm (lhs) initialrole.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) initialrole.simps(2)}\\
+ − 1503
@{thm (lhs) initialrole.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) initialrole.simps(3)}\medskip\\
+ − 1504
+ − 1505
@{thm (lhs) erole_functor.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) erole_functor.simps(1)}\\
+ − 1506
@{thm (lhs) erole_functor.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) erole_functor.simps(2)}
+ − 1507
\end{tabular}}
+ − 1508
\end{isabelle}
+ − 1509
+ − 1510
If this efficient initial role is normal role, then RC-Model assigns
+ − 1511
this role to the process after execution finished. Otherwise if this
+ − 1512
efficient initial role is using special value @{term
+ − 1513
"UseForcedRole"}, then the new role for the process is then
+ − 1514
determinated by the efficient forced role of the executable file
+ − 1515
@{term "forcedrole"}. When new process is created, this process'
+ − 1516
role is assigned to its creator's role.
+ − 1517
*)