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…
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
rebalanced.''
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.
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
operation?
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
system."
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
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.
JJ
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 <goun@ddif.enet.dec.com> on 28 July 90,
Rob Gross <ROSS@BCVMS.BITNET> on 1 Aug 90,
David 'Witt' <wittenberg%ultra.DEC@src.dec.com> 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]
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:
TRW
P.O. Box 5450
Orange, CA 92667
714-991-5100
Equifax
5505 Peachtree Dunwoody, Suite 600
Atlanta, GA 30358
404-252-1134
Trans Union Corporation Consumer Relations Dept.
P.O. Box 119001
Chicago, IL 60611
312-645-6008
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
617-426-3660
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.
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
bruner@csrd.uiuc.edu (217) 244-4476
> 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@vx.acs.umn.edu | dhoyt@umnacvx.bitnet
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