The Risks Digest

The RISKS Digest

Forum on Risks to the Public in Computers and Related Systems

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

Volume 10 Issue 23

Wednesday 22 August 1990


o ATMs act up; software blamed
o Formal Verification of Safety-Critical Systems
Brian Randell
o Article on VDT Radiation
Jeff Johnson
o Terminally dumb — substitutions
Tony Scandora
o Useful credit-related addresses
Simson L. Garfinkel
o Software patent issues
John Bruner
o Re: compress
David Paul Hoyt
o New Book in Computer Ethics
Perry Morrison
o Info on RISKS (comp.risks)

ATMs act up; software blamed

Wed, 22 Aug 90 11:37:09 PDT
    PORTLAND, Ore. (UPI) — Hundreds of automated bank teller machines on
The Exchange network in Oregon and Washington went on the fritz this week, a
problem officials traced to a computer software glitch.
    The network includes most major financial institutions in Oregon,
except for First Interstate Bank.
    Tom Bass, president of The Exchange, based in Bellevue, Wash., said the
problem was ``a certain segment of the computer overloaded, and it had to be
    One Portland woman said she put her card in a machine to withdraw some
money and got a slip back showing the withdrawal but no cash.
    In other cases, customers using about 400 machines put in their cards,
watched the machine process their transactions and got their card back, but no
receipt. Others got no money, only a receipt showing that their request to
withdraw cash had been denied.
    Bass said Tuesday the problems had been corrected but that officials
were watching closely to prevent any repeat. He said the system can detect
errors and correct them automatically but advised anyone who has difficulties
with the machines to contact their bank's customer service department.

Formal Verification of Safety-Critical Systems

Brian Randell &>
Mon, 20 Aug 90 16:46:04 BST
As I know from personal experience, recommending an article on formal
verification to the RISKS readership is itself a risky act.  Nevertheless let
me, with some trepidation, recommend (without necessarily agreeing totally
with) the paper "Formal Verification of Safety-Critical Systems", by Moser and
Melliar-Smith, that has just appeared in the August 1990 issue of Software
Practice and Experience.

The paper's abstract is as follows:

 "We describe our practical experience in the use of formal verification to
 obtain increased confidence in the design of safety-critical systems. The
 experiment involved demonstrating the consistency of the design specifications
 of SIFT, a software-implemented fault-tolerant operating system for aircraft
 flight control. Specifications were written at successive levels of
 abstraction from the most abstract requirements definition down to the
 detailed level of program code.  Consistency of the successive levels of
 specification is demonstrated using the enhanced HDM verification system.
 Formal verification is currently feasible only for carefully simplified
 systems, but there appears to be no alternative method that can meet the
 extreme safety requirements for safety-critical systems."

Apart from the description of the SIFT experiment, I regard the article as
notable for its discussion of the advantages and disadvantages of software
testing, software fault tolerance, safety kernels, fault tree analysis, and (in
much more detail) formal verification.

Quoting from the paper's section entitled "Can Verification Ensure Safety?":

 "Formal verification is an elusive approach to achieving safety in computer
 systems. It is clear that whatever is demonstrated by formal verification is
 demonstrated with almost absolute certainty. But what is it that is
 demonstrated by formal verification and is it what is needed for safe

 Strictly speaking, formal verification only demonstrates a mathematical
 relationship between a mathematical representation of the requirements or
 specification of the system and a mathematical representation of the design or
 program code. Before we can assert that the verification has any significance,
 we must be confident that

 1. The top-level specifications or requirements are correct and
    sufficient to ensure the properties we need - a major problem.

 2. The mathematical representation of the specifications means what we
    think it means and the verification system does not permit invalid
    proofs - usually not a problem.

 3. The mathematical representation of the program code is identical to
    the actual code - often it is not.

 4. The formal semantics of the programming language and the
    verification conditions constructed for the program accurately
    reflect our intent for the language - a problem only for difficult
    constructs such as concurrency.

 5. The implementation of the design or program code, including
    compilation and instruction execution by the underlying computer,
    is correct - another significant problem.

 6. The fault models are realistic models of the risks of faults in the

Some of the authors' overall conclusions will, no doubt, arouse
controversy, but nevertheless are I think worth quoting from here:

 "Within the current technology, formal verification is a possible
 approach for small sets of safety properties in clean simple
 carefully-designed systems, where the cost of failure is high enough
 to justify the cost of verification. Examples of such systems include
 nuclear reactor safety shutdown systems, simple security systems such
 as red/black encryption schemes, and simple operating system kernels.
 To be verifiable such systems must be highly restricted in their
 levels of complexity, and desired features may have to be sacrificed.

 It is clear that it is still infeasible to verify typical real
 systems of sizes in the tens and hundreds of thousands of lines of
 code.  Examples of systems that are still infeasible are nuclear
 control systems, aircraft flight control systems, and multi-user
 secure operating systems.

 For systems that must be very safe, there appears to be no alternative
 to verification. Testing, fault tolerance, and fault tree analysis can
 make important contributions to safety, but they alone are unlikely to
 achieve the high levels of safety that are necessary for safety-
 critical applications. Without improved verification systems these
 applications should not be certified at the level of 10**-10
 safety-critical failures per hour.

 Formal verification is, therefore a critical enabling technology for
 many important applications, both civil and military. It is far from
 clear that imminent advances in verification technology will suffice
 to render feasible the verification of these systems. A realistic
 time-scale for the improvement in verification technology required to
 verify real systems cannot be less that twenty years, even assuming
 sufficient interest and funds.

 Unfortunately, interest in and support for research in formal
 verification has been limited and, consequently, progress has been
 slow. Potential users have been reluctant to accept verification for
 fear that they may be forced into premature use of a technology that is
 currently difficult and costly to apply. This reluctance is bolstered
 by wishful thinking about techniques, such as software fault
 tolerance, that are easier to apply but that are unlikely to achieve
 the high levels of safety required."

Let me end by stating explicitly that my aim in making these selective
quotations is to encourage RISKS readers to study the full paper and
debate its conclusions (preferably in that order!); as I mentioned at the
outset, it is not to imply my total agreement even with those parts of
the paper I have chosen to quote.

Brian Randell, Computing Laboratory, University of Newcastle upon Tyne, UK

Article on VDT Radiation

Jeff Johnson <>
Wed, 22 Aug 90 11:17:35 PDT
The 8/17 issue of The Nation has an article by Herbert Kohl that describes the
effect upon the industry of an article by Paul Brodeur on the hazards of VDT
radiation that appeared in MacWorld.  Brodeur's MacWorld article reviews the
evidence on VDT radiation (a summary of what is in his book, "Currents of
Death: Power Lines, Computer Terminals, and the Attempt to Cover Up Their
Threat to Your Health"), then gives the results of testing ten monitors
commonly used with the Macintosh.  From Kohl's article:

  "At twelve inches electromagnetic radiation ranged from a low of 1.11 milli-
  gauss (but was generally higher than 2) at the front of the screen to a high
  of 15.86 milligauss at the side of a color, high resolution monitor. (The sides
  and backs of monitors emit the highest levels of radiation.)  They found that
  only at a distance of twenty-eight inches — 'arm's length' — was it 'sensible'
  to sit at the front of the screen.  Four feet was their recommended distance
  from the sides and back."

Brodeur contends that epidemiological studies strongly suggest that levels of
low-frequency electromagnetic radiation from power lines, water-bed heaters,
electric blankets, and VDTs may increase risk of leukemia, brain cancer, and
reproductive disorders.

In response to the MacWorld article, Apple announced that it will support the
development of industry-wide safety standards for electromagnetic emissions,
but argued that there is yet no scientific proof of how electromagnetic
radiation affects the body.

Terminally dumb — substitutions

Tony Scandora 708-972-7541 &35048@ANLCMT.CMT.ANL.GOV>
Wed, 22 Aug 1990 14:26:43 CDT
The Chicago Tribune, sometime around 30 July 1990, reported the following:

The computer terminals at newspapers are equipped with all sorts of dangerous
buttons that should be purged from the keyboard.  One is the "spell" key, which
transforms poor spellers into non-spellers.  Another is the "search-and-replace"
key, which at a single touch can, for example, change "FBI" to "Federal Bureau
of Investigation," or vice versa.  The Fresno Bee in California has this
technology, and because of it had to run the following correction the other
day: "An item in Thursday's Nation Digest about the Massachusetts budget crisis
made reference to new taxes that will help put Massachusetts `back in the
African-American.'  This item should have said `back in the black.'"

Tony Scandora, Argonne National Lab, 708-972-7541

   [An article in the 28 July 90 Boston Globe was previously reported to
   RISKS by
       Roger H. Goun <> on 28 July 90,
       Rob Gross <ROSS@BCVMS.BITNET> on 1 Aug 90,
       David 'Witt' <> on 6 Aug 90,
   among others.  I finally got around to running Tony's version today, because
   the Globe article did not note the automated substitution capability, and it
   could have been just a human reedit.  For those of you for whom this is a
   new phenomenon, RISKS has run many similar tales in the past.  PGN]

useful credit-related addresses

Simson L. Garfinkel <>
Fri, 17 Aug 90 08:51:08 EDT
Protecting Your Credit and Your Privacy

By Simson L. Garfinkel

1. The first step to protecting your credit record is to get a copy of
it.  If there is invalid information on the report, have it corrected.

   If you have been denied credit within the last 30 days, the credit reporting
agency is obligated under the Fair Credit Reporting Act (FCRA) to provide you
with a copy of your credit report for free.  Otherwise, you will be required to
pay $15 for the report.  (If you live in Maryland, the cost for the report is
$5; in California, $8; and in Connecticut, $10.)
   When requesting your report, be sure to include your name, address, previous
addresses for the past five years, your social security number, your signature,
and a telephone number where you can be reached during the day.
   In addition to your credit history, the report will include the names of
every business that has requested your report within the past two years.  If
you do not recognize any of the companies, someone may have obtained credit in
your name.
   Since each credit bureau maintains its own files, some may have errors that
others do not.  You should be sure to check with more than one bureau.  The
``big three'' are:
    P.O. Box 5450
    Orange, CA 92667

    5505 Peachtree Dunwoody, Suite 600
    Atlanta, GA 30358

    Trans Union Corporation Consumer Relations Dept.
    P.O. Box 119001
    Chicago, IL 60611

There are also many local credit bureaus.  Bankcard holders of America, a
non-profit consumer education group, publishes a ``credit-check kit'' that
includes the name, address and phone numbers of legitimate credit bureaus
across the country, as well as a pamphlet that explains in details your rights
under the FCRA.  The kit costs two dollars and is available from:

    Bankcard Holders of America
    560 Herndon Parkway Suite 120
    Herndon, VA 22070

   If you disagree with anything on your report, contact the credit bureau.
The FCRA requires the bureau to reinvestigate the facts in the dispute; if you
do not agree with their conclusion, you have the right to include a statement
in the report with your version of the story.

   2. Obtain a statement of your earnings from the Social Security
Administration every two years.  This will tell you if someone else is earning
wages under your social security number, which can lead to many difficulties at
retirement.  If you suspect an error, you have three years, three months and 15
days after the mistake is made to challenge it.

   To get your statement, you need to fill out a Request For Earnings and
Benefit Estimate Statement card, which can be ordered by telephone from the
Social Security Administration's toll free number, 800-234-5772.

   3. You can ``opt-out'' of direct marketing and telemarketing by having your
name added to the databases maintained by the Direct Marketing Association.
Write to:

    Telephone Preference Service
    Mail Preference Service
    Direct Marketing Association
    6 East 43rd Street
    New York, NY 10017
    212-689-4977 ext. 369

   The major credit bureaus also use their credit databases for direct
marketing, and many magazines also sell their subscription lists for
advertising purposes.  You can write to each company that has your name and
address and ask that your names not be released for marketing purposes.
   4.  You can get a copy of your medical information file by writing to:
    Medical Information Bureau
    P.O. Box 105
    Essex Station Boston, MA 02112

   The MIB will tell you if they have a file on you, but in some cases they
will send its contents only to your physician or dentist.  Therefore, be sure
to include that person's name and address.
   5.  Do not permit merchants to record your credit or charge card account
number on personal checks; these numbers are often transcribed and used for
fraudulent purposes.

software patent issues

John Bruner <>
Fri, 17 Aug 90 09:07:45 CDT
Those who are concerned with the issues surrounding software patents
may find the following of interest:

    Pamela Samuelson, ``Should Program Algorithms be Patented?''
    (``Legally Speaking'' column), Communications of the ACM,
    volume 33, number 8 (August 1990), pp. 23-27.

    Michael Slater, ``Failings of the Patent System,'' (``Micro
    View'' column), IEEE Micro, volume 10, number 4 (August 1990),
    pp. 96-95.

John Bruner Center for Supercomputing R&D, University of Illinois        (217) 244-4476

Re: compress (Sill, RISKS-10.21)

david paul hoyt <>
Thu, 16 Aug 90 16:28 CDT
> Not true.  Although the LZW compression algorithm is transparent to users of
> compress, as it should be, files compressed using it couldn't be uncompressed
> by a replacement program.

  Hmmm, I wonder if Unisys holds a patent on uncompressing LZW files.  I'm not
a patent lawyer, but it's the method of LZW compression that is patented.  It
seems (IMHO) that one couldn't patent the parsing of a published file format.
Or if one can, why isn't Lotus suing the pants off of everyone who 'imports'
1-2-3 files?

david paul hoyt | | dhoyt@umnacvx.bitnet

New Book in Computer Ethics [See RISKS-9.15]

Perry Morrison MATH <>
17 Aug 90 01:20:13 GMT
I'm pleased to announce the availability (like NOW) of a new book designed
for teaching courses in computer ethics. It is available from MIT Press in
the States and Basil Blackwell in the UK.

                            Computer Ethics
                 Cautionary Tales and Ethical Dilemmas in Computing
                by Tom Forester and Perry Morrison

Tom Forester, Perry Morrison, School of Computing & Information Technology,
Griffith University, Queensland, Australia

   [The Contents and Preface were included in full in RISKS-9.15.
   Let Perry or me know if you want a reiteration.  PGN]

Please report problems with the web pages to the maintainer