untitled

Size: px

Start display at page:

Download "untitled"

诫颜
5 years ago
Views:

1 /2004/15(12) Journal of Software Vol.15, No.12 1,2+ 1 (, ) 2 (, ) Covert Channel Analysis in Secure Operating Systems with High Security Levels QING Si-Han 1,2+ 1 (Engineering Research Center for Information Security Technology, The Chinese Academy of Sciences, Beijing , China) 2 (Institute of Software, The Chinese Academy of Sciences, Beijing , China) + Corresponding author: Phn: , qsihan@ercist.iscas.ac.cn, Received ; Accepted Qing SH. Covet channel analysis in secure operating systems with high security levels. Journal of Software, 2004,15(12):1837~ Abstract: The thirty years, development of covert channel analysis research is summarized. The essence of covert channel and its analysis is depicted according to our theoretical research and engineering experience in this area. The state of the art in the application of covert channel analysis approaches to the real systems is illustrated. Some major threads and emerging trends of the research in this area are presented. Key words: secure operating system; covert channel analysis; information flow; storage channel; timing channel : 30,,,,. : ; ; ; ; : TP301 : A Lampson [1] :,,.,, 30, [2,3].,.,,. 1985, TCSEC [4],., B2,,, Supported by the National Natural Science Foundation of China under Grant No ( ); the National Grand Fundamental Research 973 Program of China under Grant No.G ( (973)) : (1939 ),,,,,.

2 1838 Journal of Software 2004,15(12). GB GB/T ,. 30,,,., ,,.,. 1977,Schaefer [5] :,. 1978,Huskamp [6] :,. 1983,Kemmerer [7] :,. 1990,Tsai, Gligor Chandersekaran [8].,,, M I(M),I(M) I(S i ) I(S j ), M S i S j M. Lampson,Schaefer,Huskamp Kemmerer,.Tsai, : (1), ; (2), ; (3) TCB. 1.2, ,,.1975,Lipner [9],,.,,,., ( :CPU ),,,.,, I(M).,,.,,.,,.,,,. :(1) ;(2),.

3 : ,.,,,,.,, 1,.,,, 1.,,,, ,,,.,,,.,.,.,,,.,.,,.,,.,,,.,,, ,.,Tsai TCB,,, 3 : (1).TCB,,, TCB. (2) TCB.TCB TCB,,, TCB. (3).TCB,,, TCB.,, TCB, ,. :(1) ;(2) ;(3)., :(1) ;(2) ;(3),,.,, ,,.,

4 1840 Journal of Software 2004,15(12),,.,., :. :CPU I/O. 1.3 Kemmerer : (1) ; (2) ; (3) ; (4),,. Kemmerer : (1) ; (2), ; (3) ; (4),,.,., CPU., CPU. 1.4,,.,.,,.,.,., /,., TCB TCB,.,, :(1) ;(2) ;(3).,.,.,, 3 : (1) (DTLS) ;(2) (FTLS) ;(3). 2,. :(1), ;(2),, , SRM,Kemmerer 1983,. : 1. TCB, TCB / ;

5 : , TCB, /., TCB, R.,, TCB, M.,,. 3., : R, M, M. R, R R, r., r., r R,r,R., r R. 4., R M,.,,., 4 : (1), L ; (2), N ; (3), S ; (4), P. 5.,.,. SRM : 1.,, [7]. 2. DTLS,FTLS. 3.. SRM : 1. SRM,,.,. 2. TCB, TCB. 3.,. SRM,.,Porras Kemmerer [10] (CFT), SRM.,., [10]., SRM ,,.,1995,McHugh [11] SRM.. Global var a,b,c,d Procedure SC1 (Var u: uvar) = begin a := if b then c else d; u := c; end; SC1 a M b R c R d R u M, b,c,d a; b,c,d

6 1842 Journal of Software 2004,15(12) u.,.,.,.,.,mchugh SRM, 3 : (1).,, u_in. R.,, u_out.,, M.(2).,, M.(3).,,.,.,,. SC1( ) SC1(=b) SC1( b) a M M b R R c R R d R u_in R R R u_out M ,Kemmerer Taylor [12], Trusted DG/UX (B2 ).DG/UX Unix, 170,400, 23..DG/UX,,,.,,.,,.,DG/UX.,,. DG/UX,,,Kemmerer Taylor SRM DG/UX, SRM.,.,,., open, cm pn. open, sci. DG/UX,,,., cm 48, 24 sci. SRM, SRM, SRM. : 1),,. 2),,. : 1),. 2).,.

7 : Denning [13],.,(1)., b, a:=b b a, a b,.,.,if x=a then y:=b else z:=c y x z x., y b z c.(2), b a, a b.(3),.,a:=b SL(a) SL(b), SL(x) x.(4).,, :(a) ;(b),. : (1),. (2) TCB. (3). : (1). (2),,. (3) TCB ,Tsai, Gligor Chandersekaran [8],.Tsai, :(1), / ;(2), ;(3),. Secure Xenix.,(1) ;(2) / ;(i), / ;(ii) FCD;(iii), ;(iv) ;(v) /, ;(3),. : (1),,. (2). (3) /,. : (1), FCD,. (2),,. (3),.,He Gligor [14], TCB,.,,.

8 1844 Journal of Software 2004,15(12) 2.4 Feiertag [15,16],Goguen Meseguer [17],. TCB,.,,, 1 ( ), 2., [18] :, 1 2.,.. TCB, X Y,w, Y. w/x w X. w,y Y(w). X Y, Y w, Y(w)=Y(w/X).,, TCB. Y-, :(1) Y Y ;(2), Y-.,., Goguen Meseguer [19] : X Y, X, Y-., TCB. TCB,. : (1) ; (2) ; (3) TCB. : (1),,, ; (2),., TCB, ; (3),., [11],. 2.5,.,.,.,,,.,,,. [20], SAT SRM,SRM,.,,.,. 3, /.,. 3.1, :(1).,.(2)..

9 : 1845,0 1, 0 1.,,.(3) TCB. TCB,.,,.,,.(4). :(i) TCB ;(ii).,,.,..,.(5).tcb, :(i), CPU ;(ii), ;(iii), ;(iv) ;(6).,.,(a), 0;(b),. 3.2, Millen [21] Tsai Gligor [22],. Tsai Gligor Markov,,,. :,0 1., 0 1,.,, ( ).,., B(0) : B(0)=b(T R +T S +2T CS ) 1.,b, 1.T R,.T S,. CPU,.T CS. Secure Xenix,T CS 20ms., 0 1,.,.1964,Shannon [23].Millen.,,,, 0., ( ),. 1,., TCB 0 1, a,b,c,d 4. 0/a 1/d 0/b State 0 State 1 1/c Fig.1 Two-State graph of a covert channel 1, C:

10 1846 Journal of Software 2004,15(12) C= lim(log 2 N i ( t)) / t t N i (t) i t, : N i (t)= N j ( t T ij ) (2),T ij i j. 1, (2) : N 0 (t)=n 0 (t a)+n 1 (t c), N 1 (t)=n 0 (t b)+n 1 (t d)., N i (t)=a i x t. (2), : A i x t t = Tij A j x. j j :(P I)A 0,,P x,i.(p I), Det(P I) 0., (1) : t C = lim (log 2 Ai x ) / t = log 2 x. t,x.,. 1, x : a c x 1 x Det ( P I ) = 0, b d x x 1 x (a+d) x a x d+1 x (b+c)= ,Shieh [24] Millen.,,, ;,,.Shieh,. 3.3.,,,.,., ;.,.,.,,.,, TCB.,., TCB,, ;.,.,.,.,.,. 4 (1) 4.1, 3,.,,.,,,,, ;.,,.

11 : ,,. :(1) ;(2) ;(3). Hu [25],.,, [9]. :(1),, ;(2).Hu VAX 5%~6%,. Tsai Gligor [22].,.,., 75%,,.,.,, TCB,.,,.,,., TCB,,. 4.3,,. :.,, ;,,.,. :(1) TCB ( );(2).,., [26,27]. 5,,,.,,,.,,.,,,.,.,,,,,,.,.,,.,,,.,MITRE,Gypsy,Ina Flo/MLS,SRI HDM.,,,.,.,,,.,., view, view,,,.,?.

12 1848 Journal of Software 2004,15(12) References: [1] Lampson BW. A note on the confinement problem. CACM, 1973,16(10). [2] Qing SH, Liu WQ, Liu HF. Introduction to Operation System Security. Beijing: Science Press, 2003 (in Chinese). [3] NCSC. A guide to understanding covert channel analysis of trusted system, NCSC-TG-030, [4] U.S. Department of Defense. Trusted Computer System Evaluation Criteria, DoD STD [5] Schaefer M, Gold B, Linde R, Scheid J. Program confinement in KVM/370. In: Proc. of the 1977 Annual ACM Conf. New York: ACM, ~410. [6] Huskamp JC. Covert communication channels in timesharing systems. Technical Report UCB-CS-78-02, [7] Kemmerer RA. Shared resource matrix methodology: An approach to identifying storage and timing channels. ACM Trans. on Computer Systems, ~277. [8] Tsai CR, Gligor VD, Chandersekaran CS. A formal method for the identification of covert storage channels in source code. IEEE Trans. on Software Engineering, ~580. [9] Lipner SB. A comment on the confinement problem. Operating Systems Review, ~196. [10] Porras PA, Kemmerer RA. Covert flow trees: A technique for identifying and analyzing covert storage channels. In: Proc. of the 1991 IEEE Computer Society Symp. on Research in Security and Privacy ~51. [11] McHugh J. Covert channel analysis: A chapter of the handbook for the computer security certification of trusted system. NRL Technical Memorandum 5540:062A, [12] Kemmerer RA, Taylor TA. Modular covert channel analysis methodology for trusted DG/UXTM. IEEE Trans. on Software Engineering, Vol. 22, [13] Denning DE. A lattice model of secure information flow. Communications of the ACM, ~243. [14] He J, Gligor VD. Information flow analysis for covert-channel identification in multilevel secure operating systems. In: Proc. of the 3rd IEEE Workshop on Computer Security Foundations ~148. [15] Feiertag R. A technique for proving specifications are multilevel secure. Technical Report CSL-109, [16] Feiertag R, Levitt KN, Robinson L. Proving multilevel security of a system design. In: Proc. of the 6th ACM Symp. on Operating Systems Principles ~65. [17] Goguen JA, Meseguer J. Security policies and security models. In: Proc. of the IEEE Symp. on Security and Privacy ~20. [18] Millen JK. Foundations of covert-channel detection. Technical Report MTR-10538, The MlTRE Corporation, [19] Goguen JA, Meseguer J. Unwinding and inference vontrol. In: Proc. of the IEEE Symp. on Security and Privacy ~86. [20] Haigh JT, Kemmerer RA, McHugh J, Young WD. An experience using two covert channel analysis techniques on a real system design. IEEE Trans. on Software Engineering, ~168. [21] Millen JK. Finite-State noiseless covert channels. In: Proc. of the Computer Security Foundations Workshop ~85. [22] Tsai CR, Gligor VD. A bandwidth computation model for covert storage channels and its applications. In: Proc. of the IEEE Symp. on Security and Privacy ~121. [23] Shannon CE, Weaver W. The Mathematical Theory of Communication. Urbana: The University of Illinois Press, [24] Shieh SP. Estimating and measuring covert channels bandwidth in multivlevel secure operating system. Journal of Information Science and Engineering, 1999,15:91~106. [25] Hu WM. Reducing timing channels with fuzzy time. In: Proc. of the IEEE Symp. on Research in Security and Privacy ~20. [26] Shieh SP, Gligor VD. Auditing the use of covert channels in secure systems. In: Proc. of the IEEE Symp. on Research in Security and Privacy [27] Qing SH, Liu WQ, Weng HZ, Liu HF. Operation System Security. Beijing: Tsinghua University Press, 2004 (in Chinese).

13 : 1849 : [2],,.. :,2003. [27],,,.. :, EI Compendex ;SA ;COMPUAB ; ; ;

2 3. 1,,,.,., CAD,,,. : 1) :, 1,,. ; 2) :,, ; 3) :,; 4) : Fig. 1 Flowchart of generation and application of 3D2digital2building 2 :.. 3 : 1) :,

2 3. 1,,,.,., CAD,,,. : 1) :, 1,,. ; 2) :,, ; 3) :,; 4) : Fig. 1 Flowchart of generation and application of 3D2digital2building 2 :.. 3 : 1) :, 3 1 Vol. 3. 1 2008 2 CAA I Transactions on Intelligent Systems Feb. 2008, (,210093) :.,; 3., 3. :; ; ; ; : TP391 :A :167324785 (2008) 0120001208 A system f or automatic generation of 3D building models