Design of secure operating systems with high security levels
Tóm tắt
Numerous Internet security incidents have shown that support from secure operating systems is paramount to fighting threats posed by modern computing environments. Based on the requirements of the relevant national and international standards and criteria, in combination with our experience in the design and development of the ANSHENG v4.0 secure operating system with high security level (hereafter simply referred to as ANSHENG OS), this paper addresses the following key issues in the design of secure operating systems with high security levels: security architecture, security policy models, and covert channel analysis. The design principles of security architecture and three basic security models: confidentiality, integrity, and privilege control models are discussed, respectively. Three novel security models and new security architecture are proposed. The prominent features of these proposals, as well as their applications to the ANSHENG OS, are elaborated. Cover channel analysis (CCA) is a well-known hard problem in the design of secure operating systems with high security levels since to date it lacks a sound theoretical basis and systematic analysis approach. In order to resolve the fundamental difficulties of CCA, we have set up a sound theoretical basis for completeness of covert channel identification and have proposed a unified framework for covert channel identification and an efficient backward tracking search method. The successful application of our new proposals to the ANSHENG OS has shown that it can help ease and speedup the entire CCA process.
Tài liệu tham khảo
Spencer R, Smalley S, Loscocco P, et al. The Flask security architecture: System support for diverse security policies. In: Proceedings of the 8th USENIX Security Symposium. Washington DC: Usenix Assoc., 1999. 123–139
Wright C, Cowan C, Morris J, et al. Linux security modules: General security support for the Linux kernel. Usenix Security Symp., Usenix Assoc., 2002. 17–31
Kuhnhauser W, Ostrowski M. A framework to support multiple security policies. In: Proceedings of the 7th Canadian Computer Security Symposium, Ottawa, Canada, 1995
Bell D E. Modeling the multipolicy machine. In: Proc. of the New Security Paradigm Workshop, 1994, 2–9
Bell D E, La Padula L J. Secure Computer System: Unified Exposition and Multics Interpretation. Mitre Report, MTR-2997 Rev. 1, 1976
Ott A. Regel-Basierte zugriffskontrolle nach dem Generalized framework for access controlansatz am beispiel Linux. Diplomarbeit Universitat Hamburg, 1997
Lee T. Using mandatory integrity to enforce “commercial” security. In: Proceedings of IEEE Symposium on Security and Privacy. Oakland: IEEE Computer Society Press, 1988. 140–146
Bell D E. Security policy modeling for the next-generation packet switch. In: Proceedings of IEEE Symposium on Security and Privacy. Oakland: IEEE Computer Society Press, 1988. 212–216
Mayer F L. An interpretation of refined Bell-La Padula model for the TMach kernel. In: Proc of the 4th Aerospace Computer Security Application. Orlando: IEEE Computer Society Press, 1988. 368–378
Secure Computing Corporation. Assurance in the Fluke microkernel: Formal top-level specification. CDRL A004. Technical Report, Secure Computing Corporation, 1999
Ji Q G, Qing S H, He Y P. An improved dynamically modified confidentiality policies model. J Software (in Chinese), 2004, 15(10): 1547–1557
Biba K. Integrity consideration for secure computer systems. MITRE TR-3153, MITRE Corporation, 1977
Clark D, Wilson D. A comparison of commercial and military computer security policies. In: IEEE Symposium on Security and Privacy. Oakland, CA: IEEE, 1987. 184–194
Karger P. Implementing commercial data integrity with secure capabilities. In: IEEE Symposium on Security and Privacy. Oakland, CA: IEEE, 1988. 130–139
O’Brien R, Rogers C. Developing applications on LOCK. In: Proc 14th National Computer Security Conference. Washington DC, 1991. 147–156
National Security Agency, Security Enhanced Linux (SELinux). http://www.nsa.gov/selinux 2001
Ji Q G, Qing S H, He Y P. A formal model for integrity protection based on DTE technique. Sci China Ser F-Inf Sci, 2006, 49(5): 545–565
Saltzer J H, Schroeder M D. The protection of information in computer systems. Proc IEEE, 1975, 63(9): 1278–1308
Ferraiolo D, Cugini J, Kuhn D. Role based access control (RBAC): Features and motivations. In: Proceedings of 11th Annual Computer Security Applications Conference, 1995
Hoffman J. Implementing RBAC on a type enforced system. In: Proceedings of 13th Annual Computer Security Applications Conference. 1997. 158–163
Chandramouli R. A framework for multiple authorization types in a healthcare application system. In: Proceedings of the 17th Annual Computer Security Application Conference. 2001. 137–148
Portable Applications Standards. Committee of IEEE Computer Society. Standards Project, Draft Standard for Information Technology—Portable Operating System Interface (POSIX), PSSG Draft 17. New York: IEEE Inc., 1997
Ji Q G, Qing S H, He Y P. A new formal model for privilege control with supporting POSIX capability mechanism. Sci China Ser F-Inf Sci, 2005, 48(1): 46–66
Lampson B. A note on the confinement problem. Comm ACM, 1973, 16(10): 613–615
Tsai C, Gligor V, Chandersekaran C. On the identification of covert storage channels in secure systems. IEEE Trans Software Engin, 1990, 16(6): 569–580
Kemmerer R. Shared resource matrix methodology: An approach to identifying storage and timing channels. ACM Trans Comput Syst, 1983, 1(3): 256–277
Kemmerer R. Covert flow trees: A visual approach to analyzing covert storage channels. IEEE Trans Software Engin, 1991, 17(11): 1166–1185
McHugh J, Handbook for the computer security certification of trusted systems — covert channel analysis. Technical Report, Naval Research Laboratory, Feb. 1996
Kemmerer R, Taylor T. Modular covert channel analysis methodology for trusted DG/UX. IEEE Trans Software Engin, 1996, 22: 224–235
Qing S H. Covert channel analysis in secure operating systems with high security levels. J Software (in Chinese), 2004, 15(12): 1837–1849
Qing S H, Zhu J F. Covet channel analysis on ANSHENG secure operating system. J Software (in Chinese), 2004, 15(9): 1385–1392
Qing S H, Ji Q G. Formal model design for secure operating system (invited paper). In: Proceedings of ITI First International Conference on Information & Communications Technology (ICICT2003), Egypt, 2003. 27–47