A formal specification and verification method for the prevention of denial of service

Author

Yu, Che-Fn ; Gligor, Virgil D.

Author_Institution

GTE Labs. Inc., Waltham, MA, USA

fYear

1988

fDate

18-21 Apr 1988

Firstpage

187

Lastpage

202

Abstract

The authors present a formal specification and verification method for the prevention of denial of service in absence of failures and integrity violations. They introduce the notion of user agreements and argue 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 authors illustrate the use of this method with two examples and explain why current methods for specification and verification of safety and liveness properties of concurrent programs have been unable to handle this problem. The proposed specification and verification method is meant to augment current methods for secure system design

Keywords

multiprocessing systems; operating systems (computers); parallel programming; program verification; security of data; specification languages; concurrent programs; denial-of-service prevention; fair service access; formal specification; prevention of denial of service; simultaneity conditions; user agreements; verification method; Computer crime; Educational institutions; Formal specifications; Laboratories; Logic; Safety; Trademarks;

fLanguage

English

Publisher

ieee

Conference_Titel

Security and Privacy, 1988. Proceedings., 1988 IEEE Symposium on

Conference_Location

Oakland, CA

Print_ISBN

0-8186-0850-1

Type

conf

DOI

10.1109/SECPRI.1988.8111

Filename

8111