Formal Specification and Verification Method for the Prevention of Denial of Service in Ada Services.

摘要

The Institute for Defense Analyses was asked by the Ada Joint Program Office and the Rome Air Development Center to review the denial-of-service problem and introduce a new formal specification and verification method for the prevention of denial of service. A formal method for establishing the specification-to-code correspondence was used. This enabled the authors to verify formally the prevention of denial-of-service in Ada services. To verify the absence of denial of service, a service specification model is introduced. A key component of that model is the separation of the service sharing mechanism from the service sharing policy. The argument is that, in contrast with other properties, the prevention of denial-of-service requires specification of service use, i.e., user agreements which external constraints on service invocations and which must be obeyed by all service users.