The RISKS Digest
Volume 8 Issue 73

Monday, 22nd May 1989

Forum on Risks to the Public in Computers and Related Systems

ACM Committee on Computers and Public Policy, Peter G. Neumann, moderator

Please try the URL privacy information feature enabled by clicking the flashlight icon above. This will reveal two icons after each link the body of the digest. The shield takes you to a breakdown of Terms of Service for the site - however only a small number of sites are covered at the moment. The flashlight take you to an analysis of the various trackers etc. that the linked site delivers. Please let the website maintainer know if you find this useful or not. As a RISKS reader, you will probably not be surprised by what is revealed…


o State computer system scrapped
Bruce Forstall
o Fax Attack
Chuck Dunlop
o Client responsibility for organization's head crash
David A Honig
o Re: Computers in mathematical proofs
Robert Lee Wilson Jr
Robert English
Travis Lee Winfrey
o Formal Methods — Call For Papers
Nancy Leveson
o Info on RISKS (comp.risks)

State computer system scrapped

Bruce Forstall <>
Mon, 22 May 89 12:20:11 PDT
(Reprinted WITH permission of The Seattle Times, Friday, May 19, 1989, p. B1)

                State bytes off more than it can chew
                    DSHS to scrap computer system
         by Jim Simon, Times Olympia bureau

OLYMPIA — After the state spent $20 million and nearly seven years trying to
computerize its public-assistance program, the first caseworkers to use the
so-called COSMOS system made their own discovery:  They could figure out a
client's benefits faster by hand than with the computer.
    The Department of Social and Health Services announced yesterday it was
swallowing its losses and terminating COSMOS, considered the most expensive,
and some say ill-advised, computerization effort ever undertaken by the state.
    ``The project needed to be stopped and we stopped COSMOS,'' said DSHS
Secretary Richard Thompson, the fifth agency head who has wrestled with the
system.  ``There's a lot of things that went wrong that we still have to look
at.  My concern was that we had to stop spending the money.''
    The state has so far spent about $4.1 million and federal agencies about
$15.2 million on COSMOS--the Community Services Management and Operations
System.  Thompson said DSHS ultimately may be liable for up to $4 million of
the federal share.
    A consultant's report released earlier this week recommended scuttling
COSMOS.  The report cited poor management, an overly complex design, difficulty
to use by caseworkers and the use of untested software.
    Proponents originally predicted the troubled system would save the state
money by allowing computers rather than caseworkers to calculate eligibility
for welfare, food stamps and medical assistance.
    COSMOS, designed by Pennsylvania-based UNISYS Corp., was thought so
advanced that Gov. Booth Gardner and some of the state's computer professionals
likened it to ``artificial intelligence.''
    But its complexity apparently kept it from working at all.
    That became obvious this year when the system was installed on a pilot
basis in the Longview and Vancouver DSHS offices, according to Thompson and
    Workers there found it took up to twice as long to figure out a client's
eligibility from COSMOS as it did manually.  Using the computer resulted in
frequent errors in simple calculations, and perhaps most nerve-wracking for
caseworkers, the screen often went blank for long intervals.
    ``This was an effort to create artificial intelligence so the computer
could `think' about eligibility,'' Gardner said yesterday.  ``I don't think
we'll mess with artificial intelligence again.''
    But critics say DSHS had plenty of advance warning about just how high a
risk COSMOS represented.
    In 1982, when planning first began, the agency estimated it would cost
$10 million and be completed in 1985.
    But the agency later sought a more ambitious system that was to cost $22
million and be completed by the end of mid-1987.  Before killing COSMOS, the
most recent estimates were that it would cost $38 million and take until late
1990 to finish.
    Gerald Reilly, who headed the DSHS division of income assistance until
recently, said the agency decided to keep pressing on until they could test
COSMOS in the field.
    ``We believed you couldn't know how this would work until you took it that
far,'' Reilly said.
    Reilly and others acknowledge that the state was aware of problems UNISYS
had setting up similar systems for other states.
    ``But virtually all these big systems have troubles,'' Reilly said.  ``The
welfare programs themselves are very complex.''
    ``Killing COSMOS was a gutsy move by Thompson,'' said Rep. Gary Locke,
chairman of the House Appropriations Committee.  ``There's going to be a lot
of finger-pointing but there was no sense chasing the good money after the
    The death of COSMOS could prove an embarrassment for UNISYS, which has
already been paid about $4.7 million.  Two sources said the state attorney
general's office is considering legal action.  The attorney general's office
declined to comment.
    A spokesman for UNISYS' local office also would not comment.
    Thompson said the agency will still pursue a system to computerize its
benefit programs.  But the next effort will probably use one of the 17 systems
certified by the federal government using technology that has been tested in
other states, he said.
    Another major state computer project that has cost taxpayers $17 million
is expected to be scrapped next year.  State officials have said they expect
to cancel the project to transfer district-court records because it doesn't
perform anywhere near the number of tasks court officials expected it would.

Fax Attack

Sat, 13 May 89 12:29:28 EDT
             Governor's try to ban unsolicited ads backfires
                    (The Ann Arbor News, 5/13/89)

   HARTFORD, Conn - The great fax attack of 1989 — an all-out lobbying
campaign against a bill banning unsolicited facsimile advertising — may have
backfired when the governor's fax machine was jammed for hours with unwanted
   Starting Thursday and continuing Friday, Gov. William A. O'Neill's fax
machine has been beeping constantly, spitting out unwanted messages from angry
businesses that advertise by fax.
   The businesses oppose a bill now awaiting O'Neill's signature that would
prohibit them from marketing their products by fax without first obtaining
the permission of the recipient.  Violators would face a $200 fine.
   Starting Thursday morning, dozens of Connecticut businesses faxed to
O'Neill's office a form letter arguing against the fax ban.
   The stream of fax messages was so constant — 40 came in before 10 a.m.
-- that the governor's office turned off the fax machine Thursday.
   O'Neill's press secretary, Jon. L. Sandberg, said the governor still hasn't
decided whether he will sign the bill.  But aides to the governor said the
persistent lobbying campaign proved how annoying unwanted messages casn be.
The inconvenience was compounded because the governor's office was unable to
use its fax machine to receive information about spring flooding around the

Client responsibility for organization's head crash

David A Honig <honig@BONNIE.ICS.UCI.EDU>
Wed, 17 May 89 09:22:49 -0700
I recently was sent a bill ($70) for two "lost books" from the campus's (U.C.
Irvine) main library.  Since I knew I had returned them, I went to check the
shelves.  I found one of them; I didn't have time to search for the other.
When I inquired as to why I had been falsely charged and billed, I was told by
the checkout clerk that it was a "computer error".  Upon phoning the library, I
found that the day I had returned the books the library had had a head crash.

The library policy is to search for "lost" books if the charge is contested,
but if they are not found, I am assumed guilty.  (What if the reshelvers
erred?)  There is essentially no recourse; I understand that the Ombudsman
would be impotent.  Worse, I am told that this occurs occasionally to others,
head crash or not.

What I find remarkable is that this organization would not give the client the
benefit of the doubt when they are *aware of an internal problem*.  Besides
this, I wonder about the tradeoffs they made in designing a book-return system
so vulnerable to the failure of one of its components (disk drive or human book
checker).  Are redundant drives or paper records so expensive that a major
library cannot use them?  I suspect the adminstrators who specified the
existing system did not understand what they were doing.  I suppose I should
not be surprised.

Re: Computers in mathematical proofs

Robert Lee Wilson Jr <bobw@ford-wdl44>
Tue, 16 May 89 10:24:27 PDT
While "dying off" of some of the mathematicians who found the computerized
4-color proof intolerable is certainly part of the reason that the
computerized "no projective plane of order 10" proof is being accepted, I
think there is another significant difference.  I knew several
mathematicians who had "gone out on a limb" with statements that 4 colors
would not suffice, no matter what the predominant belief. I can recall one
whose entire career and psyche were devoted to finding non-4-colorable maps.
He would literally give new graduate students maps to color, hoping to find
one which seemed to require 5 colors. Of course each one got colored with 4
colors, but his faith did not waver.

I have not seen this fervor in regard to the planes of order 10.  I have
seen papers which included theorems of the form "If there is a projective
plane of order 10 then ....", but frequently they also included "If there
does NOT exist ..." theorems as well.

The point I am trying to make is more or less this: It is all well and good
to give "objective" arguments about why computer proofs are valid or are
not, but somehow those arguments wind up supporting what the speaker wanted
to believe anyway!
                                         Bob Wilson

Re: Computers in mathematical proofs

Robert English <>
Wed, 17 May 89 10:21:21 pdt
I don't really see that much difference between a computerized proof and
standard proof.  In both cases, all steps of the proof must be rigorous.
In a computerized proof, the mathematician must rigorously prove that
his program is correct.  In effect, the program definition becomes a
lemma within the larger proof.

Philosophical problems don't crop up until you ask whether the computer
operated correctly, or whether defects in the underlying software (such
as the compiler or the operating system) corrupted the results.  Since
the entire system does not admit rigorous examination, some claim that
the process is fundamentally different than rigorous proof.

What this argument overlooks is that rigor does not guarantee correct-
ness to any greater degree than can be achieved in a computer-aided
proof.  A complicated proof can have errors at many stages, and
reviewers cannot be trusted to find them all, any more than programmers
can be trusted to find all of the bugs in a complicated computer
system.  Furthermore, while program proofs do not admit direct human
verification, they do allow independent verification by other humans
using similar, but different, tools.

The question of whether independent verification actually takes place
for program proofs is equivalent to the question of whether each step in
a rigorous proof is really verified by independent auditors.  In both
cases, theoretical verification is possible, but in practice, it may not
take place, or the auditing process may fail.

Re: Computers in mathematical proofs

Travis Lee Winfrey <>
Mon, 15 May 89 15:35:22 EDT
  >Lam himself says he was hoping for a positive result, which would be easy
  >to check, rather than a negative one.  But he is fairly confident in his
  >result, citing two reasons:  (a) the programs did do some internal
  >consistency checks; (b) the result agrees with "mathematical intuition"
  >(for example, an order-10 projective plane is known to be forbidden to
  >have any symmetry, which apparently is almost unheard-of for such an object).

Is anyone more familiar with this work, such as any testing or proving
techniques he attempted on his program?  100 trillion bug-free executions
seems rather high, particularly given the binary nature of the answer he
needed.  Has the Lam proof been published yet?

Formal Methods — Call For Papers

Thu, 11 May 89 16:43:21 -0400
Given the forthcoming MoD standard in Great Britain requiring the use of
formal methods on safety-critical software, we thought the following might
be of interest to Risks readers.

             Call for Papers for Special Issues of
     IEEE Software, Computer, Transactions on Software Engineering:

          Formal Methods for Software Engineering

Formal Methods are design and construction methods explicitly based on 
well-defined mathematical formalisms.  Examples are: VDM, Z, box-structures, 
traces, predicate transformers, state transition systems, axiomatic data 
types, and many more.  These methods promise (1) better control over the 
system development process through clarity and precision of specification 
and then of development steps and (2) reduced error commission and 
persistence through rigor, systematic review, and formal analysis.  Much 
progress has been made in using formal methods, developing support systems 
for them, and evaluating their applicability on industrially-oriented 
problems.  Applications to critical systems are appearing world-wide, and 
there is now some commercial interest based on advances in verifiable 
execution environments.  Several standards groups are using formal methods 
and one - VDM - is undergoing the international standards process.

A coordinated set of papers is planned for September 1990 with a survey
plus a tutorial in IEEE Computer, application case studies in IEEE Software,
and research papers in IEEE Transactions on Software Engineering.

    Oct. 1, 1989 Drafts Due (earlier submissions welcome)
    Mar. 1, 1990 Reviews Completed
    May 1, 1990 Revisions Completed
    September, 1990 Publication

A complete call for papers containing detailed information about submission 
and content will be published in SEN (July) and each of the journals.  
Information and a copy of the complete call for papers is available from 
the editors:

 Applications, tutorial, survey:         Research Contributions:

   Susan Gerhart                           Nancy Leveson
   MCC Software Technology Program         Info. & Computer Science Dept.
   3500 W. Balcones Dr.                    University of California
   Austin TX 78759, U.S.A.                 Irvine, CA 92717
   Phone: 512-338-3492                     Phone: 714-856-5517
   Fax: 512-338-3899                       Fax: 714-856-4056
   e-mail:                 e-mail:

Please report problems with the web pages to the maintainer