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 <firstname.lastname@example.org> 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 email@example.com (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 | firstname.lastname@example.org | email@example.com
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