The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - July-September (1997 vol.19)
pp: 41-59
ABSTRACT
<p><it>A distinctive concern in the U.S. military for computer security dates from the emergence of time-sharing systems in the 1960s. This paper traces the subsequent development of the idea of a "security kernel" and of the mathematical modeling of security, focusing in particular on the paradigmatic Bell-LaPadula model. The paper examines the connections between computer security and formal, deductive verification of the properties of computer systems. It goes on to discuss differences between the cultures of communications security and computer security, the bureaucratic turf war over security, and the emergence and impact of the Department of Defense's Trusted Computer System Evaluation Criteria (the so-called Orange Book), which effectively took its final form in 1983. The paper ends by outlining the fragmentation of computer security since the Orange Book was written.</it></p>
CITATION
Donald Mackenzie, Garrel Pottinger, "Mathematics, Technology, and Trust: Formal Verification, Computer Security, and the U.S. Military", IEEE Annals of the History of Computing, vol.19, no. 3, pp. 41-59, July-September 1997, doi:10.1109/85.601735
REFERENCES
1. See, e.g., General Accounting Office, Information Security: Computer Attacks at Department of Defense Pose Increasing Risks.Washington, D.C.: General Accounting Office, 1986, GAO/AIMD-96-84.
2. For a good description of batch operation and of the shift to time-sharing, see A.L. Norberg and J.E. O'Neill, A History of the Information Processing Techniques Office of the Defense Advanced Research Projects Agency.Minneapolis, Minn.: Charles Babbage Institute, Oct. 1992, chapter 1 and appendix 1; an amended version of this report has been published as Transforming Computer Technology: Information Processing for the Pentagon, 1962-1986. Baltimore, Md.: Johns Hopkins Univ. Press, 1996.
3. K.L. Wildes and N.A. Lindgren, A Century of Electrical Engineering and Computer Science at MIT, 1882-1982.Cambridge, Mass.: MIT Press, 1985, p. 348. Project MAC had wider aims, captured in the alternative version of the acronym, Machine-Aided Cognition, for which see, e.g., Norberg and O'Neill, Transforming Computer Technology, and P.N. Edwards, The Closed World: Computers and the Politics of Discourse in Cold War America. Cambridge, Mass.: MIT Press, 1996.
4. See, for example, J.B. Dennis, "Segmentation and the Design of Multiprogrammed Computer Systems," J. ACM, vol. 12, pp. 589-602, esp. 599, 1965.
5. K.C. Redmond and T.M. Smith, Project Whirlwind: The History of a Pioneer Computer.Bedford, Mass.: Digital Press, 1980, pp. 52, 65.
6. H. Goldstine, Computer From Pascal to von Neumann.Princeton, N.J.: Princeton Univ. Press, 1972.
7. W.H. Ware personal communication to D. MacKenzie, Oct.17 1996.
8. W.H. Ware, "Security and Privacy in Computer Systems," AFIPS Conf. Proc., Spring Joint Computer Conf.Washington, D.C.: Thompson Books, vol. 30, pp. 279-282, at p. 279, 1967.
9. B. Peters, "Security Considerations in a Multi-Programmed Computer System," AFIPS Conf. Proc., Spring Joint Computer Conf.Washington, D.C.: Thompson Books, 1967, vol. 30, pp. 283-286, at p. 283, 1967.
10. E.W. Pugh, L.R. Johnson, and J.H. Palmer, IBM's 360 and Early 370 Systems.Cambridge, Mass.: MIT Press, pp. 362-363, 1991.
11. Peters, "Security Considerations," p. 283.
12. Peters, "Security Considerations," p. 283.
13. Peters, "Security Considerations," pp. 283 and 285, emphasis in original.
14. W.H. Ware personal communication to D. MacKenzie, Oct.17 1996.
15. W.H. Ware, ed., Security Controls for Computer Systems: Report of Defense Science Board Task Force on Computer Security.Santa Monica, Calif.: Rand Corporation, Feb. 1970, R-609. Originally classified "confidential," the report was declassified in Oct. 1975. The quotations are from Ware's foreword to the version reissued by Rand in Oct. 1979 and from p. 18 of the latter.
16. Ibid., pp. 36, 8, and 29, respectively.
17. R. Schell telephone interview by G. Pottinger, Oct.10 1993.
18. W.H. Ware personal communication to D. MacKenzie, Oct.21 1996.
19. J.P. Anderson, Computer Security Technology Planning Study.Bedford, Mass.: HQ Electronic Systems Division, U.S. Air Force, 1972, ESDF-TR-73-51, vol. 1, pp. 3 and 33.
20. Ibid, footnote 9, footnote 14.
21. R.R. Schell, "Computer Security: The Achilles' Heel of the Electronic Air Force?" Air Univ. Rev., vol. 30, pp. 16-33, at pp. 28-29, Jan.-Feb. 1979.
22. G. Pottinger, Proof Requirements in the Orange Book: Origins, Implementation, and Implications, typescript, p. 39, Feb. 1994.
23. Anderson panel, op. cit., p. 15.
24. W.L. Schiller, Design of a Security Kernel for the PDP-11/45.Bedford Mass.: Electronic Systems Division, Dec. 1973, ESD-TR-73-294; Schell, "Computer Security," op. cit., p. 28; Wildes and Lindgren, A Century, op. cit., p. 300.
25. R.R. Schell, "Computer Security: The Achilles Heel of the Electronic Air Force?" Air Univ. Rev., vol. 30, pp. 16-33, at p. 31, Jan.-Feb. 1979.
26. P.A. Karger, M.E. Zurko, D.W. Bonin, A.H. Mason, and C.E. Kahn, "Retrospective on the VAX VMM Security Kernel," IEEE Transactions on Software Engineering, vol. 17, pp. 1,147-1,165, at p. 1,159, 1991, emphasis in original.
27. Schell interview, op. cit.
28. Schell, "Computer Security," op. cit., p. 29.
29. Ware report, op. cit., p. 48.
30. C. Weissman, "Security Controls in the ADEPT-50 Time-Sharing System," Proc. FJCC, vol. 5, pp. 119-131, quotation at p. 122, 1969.
31. Anderson panel, op. cit., vol. 1, p. 4.
32. K.G. Walter, W.F. Ogden, W.C. Rounds, F.T. Bradshaw, S.R. Ames, and D.G. Shumway, Primitive Models for Computer Security.Bedford, Mass.: Air Force Electronic Systems Division, Jan.25 1974, AD-778 467.
33. D.E. Bell and L.J. LaPadula, Secure Computer Systems: Mathematical Foundations.Bedford, Mass: Air Force Electronic Systems Division, Nov. 1973, ESD-TR-73-278, vol. 1; L.J. LaPadula, personal communication to D. MacKenzie, 29 Oct. 1996; M.D. Mesarovic, D. Macko, and Y. Takahara, Theory of Hierarchical, Multilevel, Systems. New York: Academic Press, 1970.
34. D.E. Bell and L.J. LaPadula, Secure Computer Systems: A Mathematical Model.Bedford, Mass: Air Force Electronic Systems Division, Nov. 1973, ESD-TR-73-278, vol. 2, p. 15.
35. Anderson panel, op. cit., vol. 2, p. 62.
36. D.E. Bell and L.J. LaPadula, Secure Computer Systems: A Mathematical Model, op. cit., vol. 2, p. 17.
37. D.E. Bell and L.J. LaPadula, Secure Computer System: Unified Exposition and Multics Interpretation.Bedford, Mass: Air Force Electronic Systems Division, Mar. 1976, ESD-TR-75-306, p. 17.
38. Ibid., 94, pp. 19-21.
39. Ibid., pp. 64-73.
40. Schell, "Computer Security," op. cit., p. 29.
41. P. Naur and B. Randell, eds., Software Engineering: Report of a Conference Sponsored by the NATO Science Committee.Brussels: NATO Scientific Affairs Division, p. 120, 1969.
42. E. Peláez, A Gift From Pandora's Box: The Software Crisis. PhD thesis, Univ. of Edinburgh, 1988.
43. Peters, "Security Considerations," op. cit., p. 285.
44. C.E. Landwehr, "The Best Available Technologies for Computer Security," Computer, vol. 16, pp. 86-100, at p. 96, 1983.
45. Anderson panel, op. cit., 10.
46. R.J. Feiertag, A Technique for Proving Specifications Are Multi-Level Secure.Menlo Park, Calif.: SRI Computer Science Laboratory, Jan. 1980, CSL-109.
47. L. Robinson and K.N. Levitt, "Proof Techniques for Hierarchically Structured Programs," Comm. ACM, vol. 20, pp. 271-283, 1977.
48. P.G. Neumann, R.S. Boyer, R.J. Feiertag, K.N. Levitt, and L. Robinson, A Provably Secure Operating System: The System, Its Applications, and Proofs.Menlo Park, Calif.: SRI Computer Science Laboratory, May 1980, CSL 116.
49. R.J. Feiertag and P.G. Neumann, "The Foundations of a Provably Secure Operating System (PSOS)," National Computer Conference.New York: AFIPS, 1979, pp. 329-343.
50. P. Neumann interviewed by A.J. Dale, Menlo Park, Calif., Mar.25 1994.
51. Neumann et al., op. cit., p. 2.
52. Landwehr, "Technologies for Computer Security," op. cit., p. 96.
53. Landwehr, "Technologies for Computer Security," op. cit., p. 97.
54. Jelen, "Information Security," op. cit., pp. III-83 to III-91.
55. D.E. Bell, "Concerning 'Modelling' of Computer Security," IEEE Computer Society Symp. Security and Privacy, 1988, pp. 8-13, at p. 12.
56. D.E. Bell, Secure Computer Systems: A Refinement of the Mathematical Model.Bedford, Mass.: Air Force Electronic Systems Division, Apr. 1974, ESD-TR-73-278, vol. 3, pp. 29 and 31.
57. This example is taken from G. Pottinger, Proof Requirements in the Orange Book, op. cit., p. 46.
58. We draw these examples from Feiertag and Neumann, "Foundations of PSOS," p. 333.
59. A term used, e.g., by G.H. Nibaldi, Proposed Technical Evaluation Criteria for Trusted Computer Systems.Bedford, Mass.: Mitre Corporation, Oct. 1979, M79-225, p. 9.
60. B.W. Lampson, “A Note on the Confinement Problem,” Comm. ACM, vol. 16, no. 10, pp. 613–615, 1973.
61. C.E. Landwehr, "Formal models for computer security," ACM Computing Survey, vol. 13, no. 3, pp. 247-278, Sept. 1981.
62. Bell and LaPadula, Unified Exposition and Multics Interpretation, pp. 67ff.
63. See, e.g., M. Schaefer, B. Gold, R. Linde, and J. Scheid, "Program Confinement in KVM/370," ACM 77: Proceedings of the Annual Conference.New York: Association for Computing Machinery 1977, pp. 404-410; J.T. Haigh, R.A. Kemmerer, J. McHugh, and W.D. Young, "An Experience Using Two Covert Channel Analysis Techniques on a Real System Design," IEEE Transactions on Software Engineering, vol. 13, pp. 157-168, 1987.
64. See, e.g., J.K. Millen, "Security Kernel Validation in Practice," Comm. ACM, vol. 19, pp. 244-250, 1976.
65. M.A. Harrison, W.L. Ruzzo, and J.D. Ullman, "Protection in operating systems," Comm. ACM, vol. 19, no. 8, pp. 461-471, Aug. 1976.
66. Schaefer et al., "Program Confinement in KVM/370," op. cit., p. 409.
67. See D. Kahn, The Codebreakers.London: Sphere, 1973; and J. Bamford, The Puzzle Palace: A Report on America's Most Secret Agency. Boston: Houghton Mifflin, 1982.
68. G.F. Jelen, Information Security: An Elusive Goal.Cambridge, Mass.: Harvard Univ., Center for Information Policy Research, June 1985, P-85-8, pp. III-43, I-II.
69. Ibid., I-11.
70. Norberg and O'Neill, Transforming Computer Technology.
71. Anderson panel, op. cit., vol. 1, p. 4, parenthetical remark in original.
72. Jelen, Information Security, op. cit., pp. i and II-74 to II-75.
73. Jelen, Information Security, op. cit., p. II-75.
74. S.T. Walker interviewed by G. Pottinger, Glenwood, Md., Mar.24 1993.
75. Jelen, Information Security, op. cit., p. II-79.
76. Walker interview, op. cit.
77. "A Plan for the Evaluation of Trusted Computer Systems," typescript, Feb.22 1980, reprinted in Jelen, Information Security, op. cit., pp. V-2 to V-9.
78. Walker interview.
79. Ibid.
80. Walker quoted by Jelen, Information Security, op. cit., p. II-81.
81. Admiral B.R. Inman as interviewed by G. Jelen, as quoted in Jelen, Information Security, op. cit., p. II-81.
82. S.T. Walker personal communication to D. MacKenzie, Aug.22 1996.
83. F.C. Carlucci Department of Defense Directive 5215.1, "Computer Security Evaluation Center," Oct.25 1982, reproduced in Jelen, Information Security, op. cit., pp. V-11 to V-17.
84. G.H. Nibaldi, Proposed Technical Evaluation Criteria for Trusted Computer Systems.Bedford, Mass.: Mitre Corporation, Oct. 1979, M79-225, p. 37.
85. S.T. Walker, "Thoughts on the Impact of Verification Technology on Trusted Computer Systems (and Vice Versa)," Software Engineering Notes, vol. 5, p. 8, July 1980.
86. W.D. Young and J. McHugh, "Coding for a Believable Specification to Implementation Mapping," IEEE Computer Society Symp. Security and Privacy, pp. 140-148, at p. 140,Washington, D.C., 1987, emphasis in original.
87. Department of Defense, Trusted Computer System Evaluation Criteria.Washington, D.C.: Department of Defense, Dec. 1985, DOD 5200.28-STD, pp. 19, 26, 40, and 50.
88. R.S. Boyer and J.S. Moore, "Program Verification," J. Automated Reasoning, vol. 1, pp. 17-23, at p. 22, 1985.
89. Neumann interview, op. cit.
90. Pottinger, Proof Requirements in the Orange Book, op. cit.
91. T.C.V. Benzel, "Verification Technology and the A1 Criteria," Software Engineering Notes, vol. 10, pp. 108-109, at p. 109, Aug. 1985.
92. For descriptions of them, see M.H. Cheheyl, M. Gasser, G.A. Huff, and J.K. Millen, "Verifying Security," Computing Surveys, vol. 13, pp. 279-339, Sept. 1981.
93. Walker interview, op. cit.
94. C. Weissman personal communication to G. Pottinger, Dec.18 1993.
95. Ibid.
96. C. Weissman, "Blacker: Security for the DDN. Examples of A1 Security Engineering Trades," IEEE Computer Society Symp. Research in Security and Privacy, pp. 286-292, at p. 289, 1992. This paper was presented by Weissman to the 1988 IEEE Symp. Research and Privacy, but "not published at that time because of a four year rescission of publication release," ibid., p. 286.
97. Ibid., p. 289.
98. Weissman electronic mail, op. cit.
99. Weissman, "Blacker," op. cit., p. 291.
100. National Research Council, System Security Study Committee, Computers at Risk: Safe Computing in the Information Age.Washington, D.C.: National Academy Press, 1991, p. 195.
101. S. Lipner personal communication to G. Pottinger, Oct.22 1993.
102. P.A. Karger, M.E. Zurko, D.W. Bonin, A.H. Mason, and C.E. Kahn, "Retrospective on the VAX VMM Security Kernel," IEEE Transactions on Software Engineering, vol. 17, pp. 1,147-1,165, at p. 1,159, 1991, emphasis in original.
103. Ibid., p. 1,163.
104. Lipner personal communication, op. cit.
105. Karger et al., "A Retrospective," op. cit., p. 1,163.
106. Lipner personal communication, op. cit.
107. Karger et. al., "A Retrospective," op. cit., p. 1,163.
108. Lipner personal communication, op. cit.
109. C. Bonneau telephone interview by G. Pottinger, Nov.20 1993.
110. Ibid.
111. National Research Council, System Security Study Committee, Computers at Risk: Safe Computing in the Information Age.Washington, D.C.: National Academy Press, 1991, p. 195.
112. Bonneau interview, op. cit.
113. National Research Council, System Security Study Committee, Computers at Risk: Safe Computing in the Information Age.Washington, D.C.: National Academy Press, 1991, p. 195.
114. Walker interview, op. cit.
115. Benzel, "Verification Technology," op. cit., p. 108.
116. Karger et al., "A Retrospective," p. 1,156.
117. Common Criteria for Information Technology Security Evaluation.Cheltenham, Gloucesteshire, U.K., IT Security and Certification Scheme, 1996.
118. Walker interview, op. cit.
119. Pottinger, Proof Requirements in the Orange Book, op.cit., pp. 16-17.
120. D.D. Clark and D.R. Wilson, "A Comparison of Commercial and Military Computer Security Policies," IEEE Computer Society Symp. Security and Privacy, pp. 184-194, Apr. 1987.
121. K.J. Biba, Integrity Considerations for Secure Computer Systems.Bedford, Mass.: Air Force Electronic Systems Division, 1977, ESD-TR-76-372.
122. C.E. Landwehr, C.L. Heitmeyer, and J. McLean, "A Security Model for Military Message Systems," ACM Trans. Computer Systems, vol. 2, pp. 198-222, 1984.
123. J. McLean, "A Comment on the 'Basic Security Theorem' of Bell and LaPadula," Information Processing Letters, vol. 20, pp. 67-70, 1985.
124. J.A. Goguen and J. Meseguer, "Security Policies and Security Models," Proc. Berkeley Conf. Computer Security.Los Alamitos, Calif.: IEEE CS Press, 1982, pp. 11-22.
125. T. Fine, J.T. Haigh, R.C. O'Brien, and D.L. Toups, "Noninterference and Unwinding for LOCK," Computer Security Foundation Workshop,Franconia, N.H., June11 1989. For a description of LOCK, see National Research Council, Computers at Risk, op. cit., pp. 251-252. LOCK is now known as the Secure Network Server, and the Honeywell division responsible for it is now the Secure Computing Corporation.
126. C.T. Sennett, Formal Methods for Computer Security.Malvern, Worcestershire, U.K.: Defence Research Agency, 1995, typescript, p. 2.
127. National Research Council, System Security Study Committee, Computers at Risk: Safe Computing in the Information Age.Washington, D.C.: National Academy Press, 1991, p. 195.
128. See, e.g., General Accounting Office, Information Security, op. cit.
129. Anon, "Microsoft Admits Limited NT Security," Computing, July4 1996, p. 3.
130. P. Mellor, Boeing 777 Avionics Architecture: A Brief Overview.London: City Univ. Centre for Software Reliability, 1995, typescript.
295 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool