Cost profile of a highly assured, secure operating system

ABSTRACT

The Logical Coprocessing Kernel (LOCK) began as a research project to stretch the state of the art in secure computing by trying to meet or even exceed the “A1” requirements of the Trusted Computer System Evaluation Criteria (TCSEC). Over the span os seven years, the project was transformed into an effort to develop and deploy a product: the Standard Mail Guard (SMG). Since the project took place under a US government contract, the development team needed to maintain detailed records of the time spent on the project. The records from 1987 to 1992 have been combined with information about software code size and error detection. This information has been used to examine the practical impacts of high assurance techniques on a large-scale software development program. Tasks are associated with the A1 formal assurance requirements added approximately 58% to the development cost of security-critical software. In exchange for these costs, the formal assurance tasks (formal specifications, proofs, and specification code correspondence) uncovered 68% of the security flaws detected in LOCK's critical security mechanisms. However, a study of flaw detection during the SMG program found that only 14% of all flaws detected were of the type that could be detected using formal assurance, and that the work of the formal assusrance team only accounted for 19% of all flaws detected. While formal assurance is clearly effective at detecting flaws, its practicality hinges on the degree to which the formally modeled system properties represent all of a system's esential properties.

REFERENCES

• 1: AIM TECHNOLOGY. 1988. AIM Technology published price list. AIM Technology, Santa Clara, CA.
• 2: ANDERSON, J. P. 1972. Computer security technology planning study. Tech. Rep. ESD-TR-73-51. James P. Anderson and Co., Fort Washington, PA.
• 3: BELL,D.E.AND LA PADULA, L. 1975. Secure computer system: Unified exposition and Multics interpretation. Tech. Rep. ESD-TR-75-306; ESD/AFSC; DTIC AD-A023588.
• 4: BOEBERT, W. E. 1988. Annotated TCSEC. Tech. Rep.. Honeywell Information Systems, Waltham, MA.
• 5: BOEBERT,W.E.AND KAIN, R. Y. 1985. A practical alternative to hierarchical integrity policies. In Proceedings of the 8th National Conference on Computer Security. 18-27.
• 6: BOEBERT,W.E.,KAIN,R.Y.,AND YOUNG, W. D. 1985. Secure computing: The secure Ada target approach. Scientific Honeyweller (June).
• 7: Barry W. Boehm, Software Engineering Economics, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 8: William R. Cheswick , Steven M. Bellovin, Firewalls and Internet security: repelling the wily hacker, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1994
• 9: Santosh Chokhani, Trusted products evaluation, Communications of the ACM, v.35 n.7, p.64-76, July 1992 [doi>10.1145/129902.129907]
• 10: CLARK,D.AND WILSON, D. 1987. A comparison of commercial and military computer security policies. In Proceedings of the IEEE Symposium on Security and Privacy (Oakland, CA). IEEE Computer Society Press, Los Alamitos, CA, 184-194.
• 11: Richard A. De Millo , Richard J. Lipton , Alan J. Perlis, Social processes and proofs of theorems and programs, Communications of the ACM, v.22 n.5, p.271-280, May 1979 [doi>10.1145/359104.359106]
• 12: Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
• 13: DOD. 1978. Security requirements for automatic data processing (ADP) systems. DOD Directive 5200.28.
• 14: DOD. 1985. Specification practices. MIL-STD 490A.
• 15: DOD. 1985. Department of Defense trusted computer system evaluation criteria. Department of Defense Standard DoD 5200.28-STD.
• 16: DOD COMPUTER SECURITY CENTER. 1985. Computer security requirements: Guidance for applying the Department of Defense trusted computer system evaluation criteria in specific environments. CSC-STD-003-85.
• 17: DOD. 1991. Department of Defense Federal acquisition regulation supplement: 48 code of Federal regulations.
• 18: FRAIM, L. 1986. The challenge after A1: A view of the security market. In Proceedings of the 9th National Conference on Computer Security (Sept.). 41-46.
• 19: Allen L. Ambler , Donald I. Good , James C. Browne , Wilhelm F. Burger , Richard M. Cohen , Charles G. Hoch , Robert E. Wells, Gypsy: A language for specification and implementation of verifiable programs, Proceedings of an ACM conference on Language design for reliable software, p.1-10, March 28-30, 1977, Raleigh, North Carolina
• 20: GOOD,D.I.,COHEN,R.M.,HOCH,C.G.,HUNTER,L.W.,AND HARE, D. F. 1978. Report on the language Gypsy. Tech Rep. ICSCA-CMP-10. University of Texas at Austin, Austin, TX.
• 21: J. Thomas Haigh , William D. Young, Extenting the noninterference version of MLS for SAT, IEEE Transactions on Software Engineering, v.13 n.2, p.141-150, Feb. 1987 [doi>10.1109/TSE.1987.226478]
• 22: KAIN, R. Y. 1988. Throughput benchmarks with AIM. Memorandum. LOCK program archives.
• 23: Butler W. Lampson, A note on the confinement problem, Communications of the ACM, v.16 n.10, p.613-615, Oct. 1973 [doi>10.1145/362375.362389]
• 24: LEVIN,T.E.,PADILLA,S.J.,AND SCHELL, R. R. 1989. Engineering results from the A1 formal verification process. In Proceedings of the 12th NIST/NCSC National Conference on Computer Security (Gaithersburg, MD, Oct.). 65-74.
• 25: LIPNER, S. 1985. Secure system development at Digital Equipment: Targeting the needs of a commercial and government customer base. In Proceedings of the 8th National Conference on Computer Security (Sept.). 47-54.
• 26: NATIONAL COMPUTER SECURITY CENTER. 1997. Trusted network interpretation of the trusted computer system evaluation criteria. NCSC-TG-005, Version 1.
• 27: NATIONAL COMPUTER SECURITY CENTER. 1994. Introduction to certification and accreditation. NCSC-TG-029, Version 1.
• 28: NEUMANN,P.G.,ROBINSON, L., LEVITT,K.N.,BOYER,R.S.,AND SAXENA, A. R. 1975. Provably secure operating system. M79-225. Institute of Communication Research, Stanford University, Stanford, CA.
• 29: O'BRIEN,R.C.AND ROGERS, C. 1991. Developing applications on LOCK. In Proceedings of the 14th NIST-NCSC National Conference on Computer Security (Washington,DC, Oct.).
• 30: ROCHKIND, M. J. 1975. The source code control system. IEEE Trans. Softw. Eng. SE-1,4 (Dec.), 364-370.
• 31: Ravi S. Sandhu, Lattice-Based Access Control Models, Computer, v.26 n.11, p.9-19, November 1993 [doi>10.1109/2.241422]
• 32: SAYDJARI,O.S.,BECKMAN,J.K.,AND LEAMAN, J. R. 1987. LOCKing computers securely. In Proceedings of the 10th National Conference on Computer Security.
• 33: SAYDJARI,O.S.,BECKMAN,J.K.,AND LEAMAN, J. R. 1989. LOCK trek: Navigating uncharted space. In Proceedings of the IEEE Symposium on Research in Security and Privacy (Oakland, CA, May 1-3). IEEE Computer Society Press, Los Alamitos, CA.
• 34: SCHAFFER,M.A.AND WALSH, G. 1988. LOCK/ix: On implementing Unix on the LOCK TCB. In Proceedings of the 11th National Conference on Computer Security (NIST-NCSC, Balti-more, MD, Oct.17-20). National Institute of Standards and Technology, Gaithersburg, MD.
• 35: SMITH, R. E. 1994. Constructing a high assurance mail guard. In Proceedings of the 17th National Conference on Computer Security (Baltimore, MD).
• 36: SMITH, R. E. 1996. Sidewinder: Defense in depth using type enforcement. J. Syst. Manage.
• 37: SMITH, R. E. 2000. Trends in government endorsed security product evaluations. In Proceedings of the 23rd National Conference on Information Systems Security (Baltimore, MD, Oct.).
• 38: STONEBURNER,G.R.AND SNOW, D. A. 1989. The Boeing MLS LAN: Headed towards an INFOSEC security solution. In Proceedings of the 12th NIST/NCSC National Conference on Computer Security (Gaithersburg, MD, Oct.). 254-266.
• 39: TAYLOR, T. 1991. FTLS-based security testing for LOCK. In Proceedings of the 14th NIST-NCSC National Conference on Computer Security (Washington,DC, Oct.).
• 40: THOMSEN,D.AND SCHWARTAU, W. 1996. Is your network secure? BYTE (Jan.).
• 41: WARE, W. 1970. Security controls for computer systems (U): Report of Defense Science Board Task Force on Computer Security. Rand Rep. R609-1. RAND, Santa Monica, CA.
• 42: WEISSMAN, C. 1969. Security controls in the ADEPT-50 time-sharing system. In Proceedings of the 1969 Fall Joint Conference on Computers.

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS

General Terms:
Economics, Security, Verification

Keywords:
LOCK (Logical Coprocessing Kernel), security kernels