rc: comparison Paper.thy

equal deleted inserted replaced

-:301f567e2a8e
+:4d25a9919688
 We have approximately 1000 lines of code for definitions and 6000 lines of
 code for proofs. Our formalisation is available from the
 Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/rc/}.\\[-12mm]
-%  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"!
-%  1. Both Dynamic and Statical analysis, and proved link between two \\
-%  2. Tainting Relation Formalisation  \\
-%  3. Formalisation and Verification than Model Checking  \\
-%  4. Universal Checker of Policy  \\
-%  5. source of RC rules made more precise \\
-%  6. RC example of Webserver with CGIs (key notion: Program Based Roles)  \\
-%  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.
-%The distinct feature of RC is to deal with program based roles, such as server behaviour.
-%This is in contrast to usual RSBAC models where roles are modeled around a hierachy, for
-%example in a company.
 %In a word, what the manager need is that given the
 %initial state of the system, a policy checker that make sure the under the policy
 %he made, this important file cannot: 1. be deleted; 2. be tainted.
 %Formally speaking, this policy-checker @{text "PC"} (a function that given the
 %initial state of system, a policy and an object, it tells whether this object
 % 1. fully statical, that means this policy-checker should not rely on the system
 %running information, like new created files/process, and most importantly the
 %trace of system running.
 % 2. decidable, that means this policy-checker should always terminate.
-%   The purpose of an operating system is to provide a common
-%  interface for accessing resources. This interface is typically
-%  realised as a collection of system calls, for example for reading
-%  and writing files, forking of processes, or sending and receiving
-%  messages. Role based access control is one approach for
-%  restricting access to such system calls: if a user has
-%  suffient rights, then a system call can be performed.
-%  a user might have
-%  one or more roles and acces is granted if the role has sufficent
-%  rights
-%  static world...make predictions about accessing
-%  files, do they translate into actual systems behaviour.
 *}
 (*<*)
 end

changeset 3	4d25a9919688
parent 1	dcde836219bc
child 8	2dab4bbb6684