This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Kit: A Study in Operating System Verification
November 1989 (vol. 15 no. 11)
pp. 1382-1396

The author reviews Kit, a small multitasking operating system kernel written in the machine language of a uniprocessor von Neumann computer. The kernel is proved to implement on this shared computer a fixed number of conceptually distributedcommunicating processes. In addition to implementing processes, the kernel provides the following verified services: process scheduling, error handling, message passing, and an interface to asynchronous devices. As a by-product of the correctness proof, security-related results such as the protection of the kernel from tasks and the inability of tasks to enter supervisor mode are proved. The problem is stated in the Boyer-Moore logic, and the proof is mechanically checked with the Boyer-Moore theorem prover.

[1] C. G. Bell, and A. Newell,Computer Structures: Readings and Examples. New York: McGraw-Hill, 1971.
[2] D. E. Bell and L. J. LaPadula, "Secure computer systems: Unified exposition and multics interpretation," Mitre Corp., Tech. Rep. MTR-2997, July 1975.
[3] T. A. Berson and G. L. Barksdale, Jr., "KSOS--Development methodology for a secure operating system," inAFIPS Conf. Proc., 1979, pp. 365-371.
[4] W. R. Bevier, A Verified Operating System Kernel. Computational Logic, Inc., Tech. Rep. 11, Oct. 1987.
[5] W. R. Bevier, W. A. Hunt, J. S. Moore, and W. D. Young, "An approach to systems verification,"Automated Reasoning, to be published.
[6] W. E. Boebert, W. D. Young, R. Y. Kain, and S. A. Hansohn, "Secure Ada target: Issues, system, design, and verification," inProc. Symp. Security and Privacy, 1985, pp. 176-183.
[7] R. S. Boyer and J. S. Moore,A Computational Logic Handbook. Boston, MA: Academic, 1988.
[8] Dijkstra, E. W., "The Structure of the "THE Multiprogramming System", ACM Symposium on Operating Systems,Communications of the ACM, Vol. 11, No. 5, May 1968, pp.341-346.
[9] R. J. Feiertag, K. N. Levitt, and L. Robinson, "Proving multilevel security of a system design," inProc. 6th ACM Symp. Operating System Principles, 1977, pp. 57-65.
[10] R. J. Feiertag and P. G. Neumann, "The foundations of a provably secure operating system (PSOS)," inAFIPS Conf Proc., 1979, pp. 329-334.
[11] L. Flon, "On the design and verification of operating systems. Ph.D. dissertation, Carnegie-Mellon Univ., 1977.
[12] L. Fraim, "Scomp: A solution to the multilevel security problem,"Computer, vol. 16, no. 7, pp. 26-34, July 1983.
[13] S. L. Gerhart, D. R. Musser, D. H. Thompson, D. A. Baker, R. L. Bates, R. W. Erickson, R. L. London, D. G. Taylor, and D. S. Wile, "An overview of AFFIRM: A specification and verification system," inInformation Processing 80, S. H. Lavington, Ed. Amsterdam, The Netherlands: North-Holland, Oct. 1980, pp. 343-348.
[14] B. D. Gold, R. R. Linde, R. J. Peeler, M. Schaefer, J. F. Scheid, and P. D. Ward, "A security retrofit of VM/370," inAFIPS Conf. Proc., 1979, pp. 335-344.
[15] D. Goodet al., "Report on the language GYPSY Version 2.0," Computing Science and Computer Applications, Univ. Texas at Austin, Tech. Rep. ICSCA-CMP-10, 1978; also available through Computational Logic, Inc., Austin, TX.
[16] C. A. R. Hoare, "Proof of correctness of data representations,"Acta Inform., vol, 1, pp. 271-281, 1972.
[17] C. A. R. Hoare, J. He, and J. W. Sanders, "Prespecification in data refinement,"Inform. Processing Lett., vol. 25, pp. 71-76, May 1987.
[18] M. Gordon, "HOL: A proof generating system for higher-order logic," Comput. Lab., Univ. Cambridge, Tech. Rep. 103, 1987.
[19] W. A. Hunt, Jr., "FM8501: A verified microprocessor," Inst. Comput. Sci., Univ. Texas at Austin, Tech. Rep. 47, Dec. 1985.
[20] C.B. Jones,Systematic Software Development Using VDM, Prentice Hall Int'l, 1986.
[21] R. A. Karp,Proving Operating Systems Correct. Ann Arbor, MI: UMI Research Press, 1983.
[22] R. A. Kemmerer,Formal Verification of an Operating System Security Kernel. Ann Arbor, MI: UMI Research Press, 1982.
[23] C. E. Landwehr, "The best available technologies for computer security,"Computer, vol. 16, no. 7, pp. 86-100, July 1983.
[24] E. J. McCauley and P. J. Drongowski, "KSOS--The design of a secure operating system," inAFIPS Conf. Proc., 1979, pp. 345-353.
[25] P. M. Melliar-Smith and R. L. Schwartz, "Hierarchical specification of the SIFT fault-tolerant flight control system," SRT Comput. Sci. Lab., Tech. Rep. CSL-123, Mar. 1981.
[26] R. Milner, "An algebraic definition of simulation between programs," Stanford Al Project, Tech. Rep. AIM-142, Feb. 1971.
[27] J. S. Moore, "A mechanically verified language implementation," Computational Logic, Inc., Austin, TX, Tech. Rep. CLI-30, Sept. 1988.
[28] 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," SRI, Tech. Rep., Feb. 1977.
[29] G. J. Popek and D. A. Farber, "A model for verification of data security in operating systems,"Commun. ACM, vol. 21, no. 9, pp. 737-749, Sept. 1978.
[30] G. J. Popek, M. Kampe, C. S. Kline, A. Stoughton, M. Urban, and E. Walton, "UCLA secure Unix," inAFIPS Conf. Proc., 1979, pp. 355-364.
[31] L. Robinson, K. N. Levitt, P. G. Neumann, and A. R. Saxena, "A formal methodology for the design of operating system software," inCurrent Trends in Programming Methodology, Volume I: Software Specification and Design. Englewood Cliffs, NJ: Prentice-Hall, 1977.
[32] L. Robinson and K. Levitt, "Proof techniques for hierarchically structured programs,"Commun. ACM, vol. 20, no. 4, Apr. 1977.
[33] J. Rushby, "Proof of separability: A verification technique for a class of security kernels," Comput. Lab., Univ. Newcastle upon Tyne, Tech. Rep, SSM/8, May 1981.
[34] J. Rushby, "Specification and design of secure systems," Comput. Lab., Univ. Newcastle upon Tyne, Tech. Rep. SSM/6, Mar. 1981.
[35] A. R. Saxena, "A verified specification of a hierarchical operating system," Ph.D. dissertation, Stanford Univ., 1976.
[36] N. Shankar, "Checking the proof of Godel's incompleteness theorem," Inst. Comput. Sci., Univ. Texas at Austin, Tech. Rep., 1986.
[37] J.M. Spivey,Introducing Z: A Specification Language and its Formal Semantics, Cambridge Univ. Press, 1988.
[38] B. J. Walker, R. A. Kemmerer, and G. J. Popek, "Specification and verification of the UCLA Unix security kernel,"Commun. ACM, vol. 23, no. 2, pp. 118-131, Feb. 1980.
[39] W. D. Young, "A verified code generator for a subset of Gypsy," Computational Logic, Inc., Austin, TX, Tech. Rep. CLI-33, Nov. 1988.

Index Terms:
verification; Kit; multitasking operating system kernel; machine language; uniprocessor von Neumann computer; conceptually distributed communicating processes; process scheduling; error handling; message passing; interface; asynchronous devices; correctness proof; security-related results; supervisor mode; Boyer-Moore logic; Boyer-Moore theorem prover; multiprogramming; operating systems (computers); program verification; theorem proving
Citation:
W.R. Bevier, "Kit: A Study in Operating System Verification," IEEE Transactions on Software Engineering, vol. 15, no. 11, pp. 1382-1396, Nov. 1989, doi:10.1109/32.41331
Usage of this product signifies your acceptance of the Terms of Use.