Issue No. 06 - June (1990 vol. 16)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.55087
<p>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.</p>
specification method; failure absence; verification method; integrity violations; user agreements; simultaneity conditions; denial-of-service prevention; concurrent programs; formal specification; security of data.
C. Yu and V. Gligor, "A Specification and Verification Method for Preventing Denial of Service," in IEEE Transactions on Software Engineering, vol. 16, no. , pp. 581-592, 1990.