计算机系统安全：安全模型

1 .第7章 安全模型 南京大学计算机系 黄皓教授 2010年12月13日-12月6日 

2 . 参考文献 I. Simone Fischer-Hübner，IT-Security and Privacy， Lecture Notes in Computer Science 1958. II. D. Elliott Bell and Leonard J. LaPadula， Secure Computer Systems: Mathematical Foundations。 III. D. Elliott Bell and Leonard J. LaPadula， Secure Computer Systems: Mathematical Model。 IV. K.J. Biba, Integrity Considerations for Secure Computer Systems, USAF Electronic Systems Division, Bedford, Mass., April 1977. V. David D. Clark, David Il. Wilson, A Comparison of Commercial and MilitarY computer Security Policies， IEEE Symposium on Security and Privacy April 27 - 29, 1987, pp184-194. VI. D.Brewer, M.Nash, The Chinese Wall Security Policy, Proceedings of the 1989 IEEE Symposium on Security and Privacy, Oakland, May 1989. 2010-12-13 南京大学计算机系讲义 2 

3 . Contents 1. Basic Concept 2. The Generalised Framework for Access Control (GFAC) 3. Bell La Padula Model 4. Biba model 5. Clark-Wilson Model 6. Chinese Wall Model 7. RBAC 8. TBAC 9. Noninterference Model 2010-12-13 南京大学计算机系讲义 3 

4 .1. Basic Concept 

5 .1. Basic Concept IT-Security  View: protection of the system, protection from the system;  Aims: confidentiality, integrity , availability, reliability, functionality, anonymity, pseudonymity, unobservability, unlinkablity;  Security models  Security functions: I&A, AC, Audit, Object reuse, reliability of service,  Security mechanism：password, ACL, cryptography, physical control,etc. 2010-12-13 南京大学计算机系讲义 5 

6 .Security Aims  Confidentiality: prevention of unauthorised or improper disclosure of data.  Integrity: data continues to be a proper physical and semantic representation of information. 1. Preventing unauthorised users from making modifications. 2. Preventing authorised users from making improper modifications 3. Maintaining internal data consistency (self-consistency of interdependent data).  external data consistency (consistency of data with the real- world environment that the data represents). 

7 .Security Aims  Availability: prevention of the unauthorised withholding of data or resources.  timely response  fair allocation  fault tolerance  utility or usability  controlled concurrency 

8 .Security Aims  In the English language, a distinction is made between "security" and "safety".Important aspects of safety are functionality and reliability  Functionality: the system performs its functions always “as required”.  Reliability: all functions performed on a system are always equally performed under equal constraints. 

9 .1. Basic Concept Security Aims  Anonymity  Anonymity of a user means that the user may use a resource or service without disclosing the user's identity. For example, electronic cash.  Pseudonymity  Pseudonymity of a user means that the user may use a resource or service without disclosing its user identity, but can still be accountable for that use.  Unobservability  ensures that a user may use a resource or service without others, especially third parties, being able to observe that the resource or service is being used. 2010-12-13 南京大学计算机系讲义 9 

10 .1. Basic Concept Formal System Development Path Formal Model Proof Design Verification Top-Level Specification Proof Intermediate-Level Specification Proof Low-Level Specification Proof Implementation Verification Implementation 2010-12-13 南京大学计算机系讲义 10 

11 .Security Models  For the design of a secure system, the system´s security policy has to be defined.  A security policy is a set of rules that regulate how an organisation manages, protects and distributes information.  A (formal) security model is a (mathematically) precise statement of the security policy. 

12 . 什么是安全模型？  系统的元素  模型从抽象层次规定了系  具有行为能力的主体； 统行为和约束行为的方式 。  不具有行为能力的客体 ；  系统的操作行为  模型往往用状态来表示  系统行为所依赖的环境  可以执行的命令  行为对系统产生的效果  对系统行为的约束方式  对行为的控制策略 

13 .1. Basic Concept Security Objective Formal Model Proof Design Verification Top-Level Specification Proof Intermediate-Level Specification Proof Low-Level Specification Proof Implementation Verification Implementation 2010-12-13 南京大学计算机系讲义 13 

14 .1. Basic Concept Proof the security model enforces the security policy I. Definition of security-relevant state variables (subjects, objects, security attributes, access rights) II. Definition of conditions for a secure state (invariants, security properties); III. Definition of state transition function; IV. Proof that the functions maintain the secure state; V. Definition of the initial state; VI. Proof that the initial state is secure; M. Gasser, Building a secure computer system, van Nostrand Reinhold, 1988. 2010-12-13 南京大学计算机系讲义 14 

15 .Formal system development path  Design verification: proving the consistency between the formal specification of a system and a formal security model.  the specification conforms to the functions, invariants, and constraints of the model.  Implementation verification: proving the consistency between the formal specification and its program implementation.  Complete formal implementation verification is not possible with today’s technology. —— Simone Fischer-Hübner, IT Security and Privacy, Springer.  Establishing correctness is a matter of belief, not proof. 

16 .2. 访问控制矩阵模型 

17 .2.1 HRU 模型  A. Harrison, W. L. Ruzzo, and J. D. Ullman. Protection in operating systems. Proceedings of the 5th annual SIGOPS Conference, 1975.  Michael A. Harrison and Walter L. Ruzzo (University of California, Berkeley), Jeffrey D. Ullman (Princeton University), Protection in Operating Systems, Communications of the ACM 19(8), pp461-471, Aug. 1976. 

18 .一、传统的操作系统安全 2.1 HRU 模型  访问控制矩阵  所有的主体的集合用S={s1,s2, ……，sm} 表示  所有的客体用O ={o1,o2,……，on}表示  所有的权限用R表示  访问矩阵是以主体为行索引、以客体为列索引的矩阵的第i行第j 列的矩阵元素a[si,oj] ⊆ R 表示主体si对客体oj拥有的权限。 

19 .2.1 HRU 模型 文件1 文件2 进程1 进程2 进程1 r, w, own r r, w, e, own w 进程2 a r, own r r, w, e, own  对于文件客体的r、w、a、own都比较清楚。  对于进程的读、写等在不同的系统中可能含义不同。  读：“读”进程可以接收“被读”进程发送的消息。  读： “读”进程可以读取“被读”进程的状态。 

20 .2.1 HRU 模型——系统的状态  系统的状态  所有的内存、缓存、寄存器、设备的状态等。  系统的保护状态  系统状态中涉及安全的子集。  系统的保护状态可以用三元组(S, O, A)表示。  假设Ｐ是所有的保护状态的集合，Ｑ是Ｐ的一个子集表示系统 的合法状态。  如果系统的安全状态在Ｑ中，则系统是安全的；  如果在Ｐ－Ｑ 中，则系统是不安全的。  系统的保护就是将系统控制在状态集Q中。 

21 .2.1 HRU 模型—— 状态的转换  当进程执行操作后，保护系统的状态会发生转换。  系统的初始状态设为X0={S0,O0,A0}  当系统执行一系列操作t1,t2,…后，系统状态依次变成 X1,X2,…。记为： Xi ├─ti Xi+1  当一个系统从状态x开始，经过一系列的操作后，转换到 状态Y，可以记作： X ├─* Y 

22 .2.1 HRU 模型—— 基本命令  create subject s  create object o 事前条件s ∉ S 事前条件o ∉ O 事后条件S’=S∪ {s}, O’=O∪ {s}, 事后条件S’=S, O’=O∪ {o}, ∀y∈O’, a’[s,y] = φ. ∀x∈S’, a’[x,o] = φ. ∀x∈S’, a’[x,s] = φ. ∀x∈S’, y∈O, a’[x,y] = a[x,y] ∀x∈S, y∈O, a’[x,y] = a[x,y]  destroy subject s  destroy object o 事前条件s ∈ S 事前条件o ∈ O 事后条件S’=S\ {s}, O’=O\{s}, 事后条件S’=S, O’=O\{o}, ∀y∈O’, a’[s,y] = φ. ∀x∈S’, a’[x,o] = φ. ∀x∈S’, a’[x,s] = φ. ∀x∈S’, y∈O’, a’[x,y] = a[x,y] ∀x∈S’, y∈O’, a’[x,y] = a[x,y] 

23 .2.1 HRU 模型 —— 基本命令  create subject s  create object o 事前条件s ∉ S 事前条件o ∉ O 事后条件S’=S∪ {s}, O’=O∪ {s}, 事后条件S’=S, O’=O∪ {o}, ∀y∈O’, a’[s,y] = φ. ∀x∈S’, a’[x,o] = φ.s o o o s ∀x∈S’, a’[x,s] = φ. 1 2 3 1 2 ∀x∈S’, s1 y∈O, a’[x,y] = a[x,y] ∀x∈S, y∈O, a’[x,y] = a[x,y] s2 o1 o2 o3 s1 s s2  destroy subject s  destroy s1 object o 事前条件s ∈ S s 事前条件o ∈ O s 事后条件S’=S\ {s}, O’=O\{s}, 2 事后条件S’=S, O’=O\{o}, ∀y∈O’, a’[s,y] = φ. ∀x∈S’, a’[x,o] = φ. ∀x∈S’, a’[x,s] = φ. ∀x∈S’, y∈O’, a’[x,y] = a[x,y] ∀x∈S’, y∈O’, a’[x,y] = a[x,y] 

24 .2.1 HRU 模型 —— 基本命令  create subject s  create object o 事前条件s ∉ S 事前条件o ∉ O 事后条件S’=S∪ {s}, O’=O∪ {s}, 事后条件S’=S, O’=O∪ {o}, ∀y∈O’, a’[s,y] = φ. ∀x∈S’, a’[x,o] = φ. ∀x∈S’, a’[x,s] = φ. ∀x∈S’, y∈O, a’[x,y] = a[x,y] ∀x∈S, y∈O, a’[x,y] = a[x,y] o1 o2 o3 s1 s2 φ s1 s2  destroy subject s  destroy object o 事前条件s ∈ S 事前条件o o1 o 2 o ∈ Os 3 1 s s 2 s1 事后条件S’=S\ {s}, O’=O\{s}, 事后条件S’=S, O’=O\{o}, s φ φ φ φ φ φ ∀y∈O’, a’[s,y] = φ. s2 ∀x∈S’, a’[x,o] = φ. ∀x∈S’, a’[x,s] = φ. ∀x∈S’, y∈O’, a’[x,y] = a[x,y] ∀x∈S’, y∈O’, a’[x,y] = a[x,y] 

25 .系统状态的转换 —— 基本命令  create subject s  create object o 事前条件s ∉ S 事前条件o ∉ O 事后条件S’=S∪ {s}, O’=O∪ {s}, 事后条件S’=S, O’=O∪ {o}, ∀y∈O’, a’[s,y] = φ. ∀x∈S’, a’[x,o] = φ. ∀x∈S’, a’[x,s] = φ. ∀x∈S’, y∈O, a’[x,y] = a[x,y] ∀x∈S, y∈O, a’[x,y] = a[x,y] o1 o2 o3 s1 s2 s1 s2  destroy subject s  destroy object o 事前条件s ∈ S 事前条件o o1 o 2 o ∈ Os 3 1 s s 2 s1 φ 事后条件S’=S\ {s}, O’=O\{s}, 事后条件S’=S, O’=O\{o}, s φ φ φ φ φ φ ∀y∈O’, a’[s,y] = φ. s2 ∀x∈S’, a’[x,o] = φ. φ ∀x∈S’, a’[x,s] = φ. ∀x∈S’, y∈O’, a’[x,y] = a[x,y] ∀x∈S’, y∈O’, a’[x,y] = a[x,y] 

26 .2.1 HRU 模型 —— 基本命令  create subject s  create object o 事前条件s ∉ S 事前条件o ∉ O 事后条件S’=S∪ {s}, O’=O∪ {s}, 事后条件S’=S, O’=O∪ {o}, ∀y∈O’, a’[s,y] = φ. ∀x∈S’, a’[x,o] = φ. ∀x∈S’, a’[x,s] = φ. ∀x∈S’, y∈O, a’[x,y] = a[x,y] ∀x∈S, y∈O, a’[x,y] = a[x,y] o1 o2 o3 s1 s2 s  destroy subject s  destroy 1 object o s 事前条件s ∈ S 2 事前条件o ∈ O 事后条件S’=S\ {s}, O’=O\{s}, 事后条件S’=S, O’=O\{o}, o o o s s s ∀y∈O’, a’[s,y] = φ. 1 2 3 1 2 ∀x∈S’, s1 a’[x,o] = φ. φ ∀x∈S’, a’[x,s] = φ. s ∀x∈S’, φ φ y∈O’, φ φ a’[x,y] = φ a[x,y] φ s2 φ ∀x∈S’, y∈O’, a’[x,y] = a[x,y] 

27 .2.1 HRU 模型 —— 基本命令  enter r into a[s,o]  delete r from a[s,o] 事前条件s ∈ S, o ∈ O  事前条件s ∈ S, o ∈ O 事后条件  事后条件  S’=S, O’=O, S’=S, O’=O,  a’[s,o] = a [s,o] ∪{ r } a’[s,o] = a [s,o] \{ r }  ∀x∈S’, y∈O’, (x, y) ≠(s,o) ∀x∈S’, y∈O’, (x, y) ≠(s,o) → a’[x,y] = a [x,y] → a’[x,y] = a [x,y] 

28 .2.1 HRU 模型 —— 单步命令  系统命令  单步命令 command create·file(p, f) 系统命令中仅仅包含一条基本 create object f; 命令则称为单步命令。例如： enter own into a[p,f]; enter r into a[p,f]; command make·own(p, f) enter w into a[p,f]; enter own into a[p, f]; end end command spawn·process(p, q) create subject q; enter own into a[p,q]; enter r into a[p,q]; enter w into a[p,q]; enter r into a[q,p]; enter w into a[q,p]; end 

29 .2.1 HRU 模型 —— 条件命令  条件命令  例 command (X1, … Xk) command grant·read ·file if r1 in ( Xs1, Xo1) if own in a[p,f] then r2 in ( Xs2, Xo2) enter r into a[q,f]; rm in ( Xsm, Xom) end then op1; op2; …… opn; end