Dynamic verification of operating system decisions

ABSTRACT

Dynamic verification of a decision implies that every time the decision is made there is a consistency check performed on the decision using independent hardware and software. The dynamic verification of operating system decisions is used on the PRIME system being designed and constructed at the University of California, Berkeley. PRIME is an experimental time-sharing system which is to have the properties of continuous availability, data privacy, and cost effectiveness. The technique of dynamic verification allows the construction of an operating system which does not make certain decisions improperly even in the presence of a single hardware or software fault. Furthermore, multiple faults lead to unreliable operation only if the faults happen to reinforce each other. On PRIME, dynamic verification is used to ensure that one user's information cannot become available to another user gratuitously even in the presence of a single hardware or software fault. The amount of additional hardware and software required for dynamic verification can be modest.

REFERENCES

• 1: Baskin, H. B., Borgerson, B. R., and Roberts, R. PRIME- a modular architecture for terminal-oriented systems. Proc. AFIPS 1972 SJCC, AFIPS Press, Montvale, N.J., pp. 431-437.
• 2: Borgerson, B. R. A fail-softly system for time-sharing use. Digest of the 1972 lnternat. Symp. on Fault Tolerant Computing, June 1972, pp. 89-93.
• 3: Quatse, J. T., Gaulene, P., and Dodge, D. The external access network of a modular computer system. Proc. AFIPS 1972 SJCC, AFIPS Press, Montvale, N.J., pp. 783-790.
• 4: Borgerson, B. R. Spontaneous reconfiguration in a faiLsoftly computer utility. Proc. Datafair 73, British Computer Society, London, pp. 326-333.
• 5: Lampson, B. W. Protection. Proc. 5th Princeton Conf. on lnformat. Sciences and Systems, 1971, pp. 437-443.
• 6: Amdahl, G. M. The structure of SYSTEM/360, Part 3- Processing unit design considerations. IBM Systems J. 3, 2 & 3 (196Zl), 144-164.
• 7: Weissman, C. Security controls in the ADEPT-50 timesharing system. Proc. AFIPS 1969 FJCC, AFIPS Press, Montvale, N.J., pp. 119-133.
• 8: Carter, W. C., and Bouricius, W.G. A survey of fault tolerant computer architecture and its evaluation. Computer (Jan. 1971), 10-15.
• 9: Edsger W. Dijkstra, The structure of the “THE”-multiprogramming system, Communications of the ACM, v.11 n.5, p.341-346, May 1968 [doi>10.1145/363095.363143]
• 10: Bernard Elspas , Karl N. Levitt , Richard J. Waldinger , Abraham Waksman, An Assessment of Techniques for Proving Program Correctness, ACM Computing Surveys (CSUR), v.4 n.2, p.97-147, June 1972 [doi>10.1145/356599.356602]

INDEX TERMS

Keywords:
data privacy, data security, fault tolerance, modular computer systems, operating systems, program verification, software reliability