This Article 
 Bibliographic References 
 Add to: 
A Specification and Verification Method for Preventing Denial of Service
June 1990 (vol. 16 no. 6)
pp. 581-592

A specification and verification method is presented for preventing denial of service in absence of failures and of integrity violations. The notion of user agreements is introduced, and it is argued that lack of specifications for these agreements and for simultaneity conditions makes it impossible to demonstrate denial-of-service prevention, in spite of demonstrably fair service access. The use of this method is illustrated with an example and it is explained why current methods for specification and verification of safety and liveness properties of concurrent programs do not handle this problem. The proposed specification and verification method is meant to augment current methods for secure system design.

[1] V. D. Gligor, "A note on the denial-of-service problem," inProc. IEEE Symp. Security and Privacy, Oakland, CA, Apr. 1983, pp. 5101-5111.
[2] V. D. Gligor, "A note on denial-of-service in operating systems,"IEEE Trans. Software Eng., vol. SE-10, no. 3, pp. 320-324, May 1984.
[3] V. D. Gligor, "On denial of service in computer networks," inProc. Int. Conf. Data Eng., Los Angeles, CA, Feb. 1986, pp. 608-617.
[4] A. N. Habermann, "Prevention of system deadlocks,"Commun. ACM, vol. 12, no. 7, pp. 373-377, July 1969.
[5] B. T. Hailpern, "Verifying concurrent process using temporal logic," Ph.D. dissertation, Stanford Univ., 1980; alsoLecture Notes in Computer Science, vol. 129. New York, Springer-Verlag, 1982.
[6] B. Hailpern and S. Owicki, "Modular verification of computer communication protocols,"IEEE Trans. Comm., vol. COM-31, Jan. 1983.
[7] J. W. Havender, "Avoiding deadlock in multitasking systems,"IBM Syst. J., vol. 7, no. 2, pp. 74-84, 1968; alsoActa Inform., vol. 1, no. 4, pp. 271-281, 1972.
[8] C. A. R. Hoare, "Monitors: an operating system structuring concept,"Commun. ACM, vol. 17, no. 10, pp. 549-557, Oct. 1974.
[9] L. Lamport, "Specifying Concurrent ProgramModules,"ACM Trans. Programming Languages and Systems, Vol. 5, No. 2, Apr. 1983, pp. 190-222.
[10] Owicki, S., and L. Lamport, "Proving Liveness Properties of Concurrent Programs,"ACM Trans. Programming Languages and Systems, Vol. 4, No. 3, July 1982, pp. 455-495.
[11] A. Pneuli, "The temporal logic of programs," inProc. 18th Annu. Symp. Foundations Comput. Sci., Nov. 1977, pp. 46-57.
[12] K. Ramamritham, "Synthesizing code for resource controllers,"IEEE Trans. Software Eng., vol. SE-11, no. 8, pp. 774-783, Aug. 1985.
[13] C.-F. Yu and V. D. Gligor, "A formal specification and verification method for the prevention of denial of service in ADATMServices," Inst. Defense Anal., paper no. P-2120, July 1988.

Index Terms:
specification method; failure absence; verification method; integrity violations; user agreements; simultaneity conditions; denial-of-service prevention; concurrent programs; formal specification; security of data.
C.-F. Yu, V.D. Gligor, "A Specification and Verification Method for Preventing Denial of Service," IEEE Transactions on Software Engineering, vol. 16, no. 6, pp. 581-592, June 1990, doi:10.1109/32.55087
Usage of this product signifies your acceptance of the Terms of Use.