Mechanisms for compile-time enforcement of security

ABSTRACT

This paper discusses features of a secure systems programming language designed and implemented at IBM's Watson Research Lab. Two features of the language design were instrumental in permitting security to be enforced with minimum run-time cost: (1) Language constructs (e.g. pointer variables) which could result in aliasing were removed from the programmer's direct control and replaced by higher level primitive types; and (2) traditional strong type checking was enhanced with typestate checking, a new mechanism in which the compiler guarantees that for all execution paths, the sequence of operations on each variable obeys a finite state grammar associated with that variable's type. Examples are given to illustrate the application of these mechanisms.

REFERENCES

• 1: {AMB 76} Ambler, A. L., Good, D.I., Burger, W. F. "Report on the Language Gypsy". ICSCA-CMP-1, The University of Texas at Austin, 1976.
• 2: {CAM 74} The specification of process synchronization by path expressions. Lecture Notes in Computer Science 16, New York, 1974.
• 3: {CON 79} "Process Synchronization by Behavior Controllers", Ph. D. thesis, University of Texas at Austin, December 1979.
• 4: Ole-Johan Dahl, SIMULA 67 common base language, (Norwegian Computing Center. Publication), 1968
• 5: {EGG 81} Eggert, P. R., Detecting Software Errors Before Execution, UCLA Computer Science Department, Report No. CSD-810402, April 1981.
• 6: {HAL 82} Halim, N., and Pershing, J., "A New Language for Writing Portable and Secure Systems", IBM Research Report RC 9650
• 7: Charles Antony Richard Hoare, The emperor's old clothes, Communications of the ACM, v.24 n.2, p.75-83, Feb. 1981 [doi>10.1145/358549.358561]
• 8: {KIE 79} Kieburtz, R., and Silberschatz, A., "Access-Right Expressions", University of Texas, Technical Report, 1979.
• 9: {NIL 82} NIL Reference Manual, IBM T. J. Watson Research Laboratory, internal document.
• 10: {PAR 81} Parr, F. N., and Strom, R. E., "Portable, Secure, Communications Software", Proceedings, International Conference on Communications, Denver, June, 1981, also IBM Research Report RC 8875.
• 11: {PAR 82} Parr, F. N., and Strom, R. E., "NIL: A Programming Language for Software Architecture", Proc. IEEE 6th International Conference on Software Engineering, Tokyo, expanded version also available as IBM Research Report RC 9227.
• 12: {PAR 83} Parr, F. N., and Strom, R. E., "A High Level Language for Distributed Systems Programming", to appear in IBM Systems Journal, special issue on communication, 1983.
• 13: G. J. Popek , J. J. Horning , B. W. Lampson , J. G. Mitchell , R. L. London, Notes on the design of Euclid, Proceedings of an ACM conference on Language design for reliable software, p.11-18, March 28-30, 1977, Raleigh, North Carolina