ARMS-D-Request@XX.LCS.MIT.EDU (Moderator) (11/10/86)
Arms-Discussion Digest Monday, November 10, 1986 9:11AM
Volume 7, Issue 54
Today's Topics:
Yet more on SDI (Star Wars flawed #5-of-10)
defenses, first strike
Re: killing someone if we had to look them in the eye
appropriateness of second strike
Meteorite as A-explosion
prompt response (2 msgs)
defenses, first strike (2 msgs)
perfectness of SDI
----------------------------------------------------------------------
Date: Monday, 3 November 1986 08:05-EST
From: Jane Hesketh <jane%aiva.edinburgh.ac.uk at Cs.Ucl.AC.UK>
To: ARMS-D
Re: Star Wars flawed #5-of-10
From Specification to Implementation
Robin Milner
Abstract
Producing a specification of a computing system is a largely
informal task. Certainly the specification should be a
formal (i.e. mathematical or logical) statement of how the
system should behave; but the specification can only be
accepted on the basis of human agreement that it accurately
specifies the required behaviour.
In contrast, the process of building a computing system
which meets the specification can be completely formal,
since both specifications and computer programs are formal
objects.
Such a formal design process is not normally automatic;
it involves interaction between a human and a machine, using
a formal language of some kind. The input to the process
consists of the specification, and its outcome will be a
system design whose every detail has been validated by
formal reasoning.
We argue here that research in how to conduct such
design processes, is in its early stages; that we cannot
reasonably predict when it will be well enough developed to
cope with a Battle Management System (BMS); and that this
development is extremely unlikely to occur within the time
apportioned.
Ratifying a specification
A specification for a computing system is a formal text
which describes the required behaviour of the system, but
not how this behaviour is to be realised. Though formal,
it must be intelligible to non-experts in computing; it is
they who must agree upon it.
How can the task of agreeing upon a spec be made easier
for these non-experts? It is not enough to ask them to
peruse it and announce `OK'; they need to ask it questions
- e.g. "Does it follow from the spec that if one component
computer is defective, the system performance will still lie
within specified limits?"
This process may be called ratifying the spec. It
cannot be left to error-prone human reasoning. The process
must employ computer-assisted reasoning, using computer
programs which themselves have been proved to prevent any
invalid deduction.
Techniques for computer-assisted reasoning - both about
specs and about programs - are under development. It is,
however, rash to predict when they will be adequate to
ratify the spec of BMS. This for two reasons. First, the
size of such a spec is likely to be orders of magnitude
greater than any text hitherto successfully analysed; it is
a common experience in complex systems that methods which
`scale-up' are hard to achieve. Not only does the effort
increase non-linearly; sheer size will raise problems of a
new and unpredicted nature. Second, the BMS spec is likely
to involve a variety of formalisms for logical statements,
ballistic properties, communications media and so on. The
design of specification languages which admit such plurality
of formalism is a rather profound research problem, unlikely
to be solved adequately within a particular applied project.
Verifying the software which implements a specification
Both a spec and a computer program are formal objects. In
principle, therefore, the business of verifying that a
program satisfies a spec is another task amenable to
computer-assisted reasoning. There is plenty of evidence
that critical programs which haven't been subjected to this
process actually exhibit errors in performance; BMS is
hypercritical, and must not exhibit errors.
At present, the size of programs which have been
verified formally (i.e. by computer-assisted reasoning) is
a small number of thousands of lines. Again, the problem of
`scaling-up' the methods to cope with programs of one or two
orders of magnitude higher is one which will not be solved
within a predictable time.
The problem is more intricate for `real time' programs
(like BMS) whose specification contains critical timing
constraints. It is also harder for programs which will be
run concurrently on several computers; here, the methods for
formal verification are truly in their infancy - and have to
cope with the verification of communications media as well
as programs.
It is sometimes argued that the process of deriving a
program from a spec, in such a way that it is guaranteed to
meet the spec, can be made automatic. This has never been
shown to work for any system of reasonable size, and must
therefore be discounted.
The process of verifying a program is fraught with the
same difficulty of sheer size as the problem of ratifying a
specification.
Verifying the hardware which implements a program
It is likely that a sophisticated high-level language,
perhaps Ada, will be needed for software as complex and
large as BMS.
Such a language must be implemented to run on several
computers concurrently. To verify that this implementation
is correct is itself a daunting task. One reason is that it
is still an open problem how best to specify this task -
i.e. what mathematics to use to represent the formal
semantics of a concurrent programming language. The
attempts for Ada are sadly deficient.
This constitutes a vital sub-problem of the whole; both
to ratify the semantics of a programming language, and to
verify its implementation in terms of the basic code and
communications media of a multi-computer system. I know of
no successful instances of solving this problem.
Summary
We have analysed the passage from formal specification to
correct implementation of a BMS into parts, each resting
critically upon computer-assisted reasoning. BMS will be of
such size and complexity that it cannot be expected to work
reliably unless this passage is conducted formally; but our
conclusion is that any prediction of when this will be
feasible is rash, precisely because of size and complexity.
Be this as it may, this uncertainty is probably exceeded
by the uncertainty of whether the initial specification
itself is adequate, given the changing world in which BMS
will continually find itself. So the specification and its
implementation will continually evolve, compounding the
difficulties of verification even further.
Information about the author
Robin Milner is Professor of Computer Science at the
University of Edinburgh. He is also the Director of the
Laboratory for Foundations of Computer Science, newly
established at Edinburgh with Alvey and SERC funding. He
has worked since 1968 on semantics of computation, including
concurrent computation, aiming at rigorous theories of
program behaviour.
------------------------------
Date: Sun, 9 Nov 86 20:13:48 PST
From: weemba@brahms.berkeley.edu (Matthew P Wiener)
Subject: defenses, first strike
>From: cfccs at HAWAII-EMH
>Re: defenses, first strike
>
>On the other hand, there is always the chance of an accident or
>irresponsible entity (terrorist or terroristic country?) who has
>nothing to lose, getting a nuclear weapon capability and using it
>indiscriminately. It seems that no amount of retaliation will deter a
>fanatic who has already decided to give up his life for his cause.
It also seems that SDI will do nothing to prevent a terrorist from
smuggling in a few nuclear weapons, and setting them off from below.
ucbvax!brahms!weemba Matthew P Wiener/UCB Math Dept/Berkeley CA 94720
------------------------------
Date: Sun, 9 Nov 86 22:19:27 PST
From: weemba@brahms.berkeley.edu (Matthew P Wiener)
Subject: Re: killing someone if we had to look them in the eye
Apropos this subject, I'd like to quote Batman, as presented in Frank
Miller's _Batman: The Dark Knight Returns_:
A gun ... is a coward's weapon. A liar's weapon. We
kill ... too often ... because we've made it easy ...
too easy ... sparing ourselves ... the mess ... and the
work ...
(And shame on you if you haven't read the comic book sensation of the
decade.)
ucbvax!brahms!weemba Matthew P Wiener/UCB Math Dept/Berkeley CA 94720
------------------------------
Date: Mon, 10 Nov 86 00:57:23 CST
From: osmigo1@ngp.utexas.edu (Ron Morgan)
Subject: appropriateness of second strike
Reply-To: ngp!osmigo1@ngp.utexas.edu (Ron Morgan)
>of attack on the U.S. you posited, what matters is to
>eliminate the Soviet Union as a functioning national entity. Under
>this type of response, there is no critical part of the target set.
I've been following this group for quite some time, but have never
submitted any comment. I will raise a question now, however. A number
of times, I've read that the only logical reaction to a large-scale,
generally "successful" Soviet first strike is to *not* strike back.
The main rationales have been, of course, that it would be pointless
murder of millions of innocent people, that there are "no winners,"
that it would accentuate the "nuclear winter," and that we'd be in
such bad shape that it wouldn't really matter WHAT kind of shape the
Soviets were in. I raise the following questions:
1. What do we "officially" fear from the Soviets if we withold
striking back? Occupation? Land invasion? Isolation of Europe?
2. What do you think the Soviets *would* do after a successful strike?
Tanks rolling down the roads? Dark-coated men knocking on doors?
3. How would we react to a single "warning" detonation on a single
city, as in the book "The Third World War"? Massive retaliation?
All in all, there's been so much talk about striking back, "second
strikes," etc., and not a word about what could happen afterwards,
given various alternative responses on our (or their) part.
Ron Morgan
--
osmigo1, UTexas Computation Center, Austin, Texas 78712
ARPA: osmigo1@ngp.UTEXAS.EDU
UUCP: ihnp4!ut-ngp!osmigo1 allegra!ut-ngp!osmigo1 gatech!ut-ngp!osmigo1
seismo!ut-sally!ut-ngp!osmigo1 harvard!ut-sally!ut-ngp!osmigo1
------------------------------
Date: Mon, 10 Nov 86 00:26:25 PST
From: weemba@brahms.Berkeley.EDU (Matthew P Wiener)
Subject: Meteorite as A-explosion
> Besides, the
>conversion of 1 gram of anti-matter (a cube less than 1 cm on a side)
>to energy would produce 9 x 10^20 ergs of energy, which is probably
>enough to split the earth in two.
Uh, off the back of my envelope, if fission works at .1% efficiency, and
an A-bomb uses 1 kilogram of plutonium, then 1 gram of anti-matter gives
us an A-bomb sized explosion. Moral: ergs are real teensy critters.
ucbvax!brahms!weemba Matthew P Wiener/UCB Math Dept/Berkeley CA 94720
------------------------------
Date: Monday, 10 November 1986 06:13-EST
From: cfccs at HAWAII-EMH
To: LIN, arms-d
Re: prompt response
Since we agree on most things, why do you still want a 24-hour wait?
This only serves to give the Soviet Union a greater chance of
surviving a war, and perhaps a hope that it might be pulled off
successfully. I don't really think that anyone there, or here, would
be foolish enough to try it anyway so it doesn't really matter. What
does matter is that the proliferation of nuclear technology and
weaponry is getting out of hand. That is what must be addressed! I
don't think that anyone seriously believes the S.U. or U.S. will
begin a nucuclear confrontation. Both have come through too much. If
it happens, it will be a minor player like Libya or some facsimile.
How are we protected against nuclear weapons held by fanatics with
nothing to lose? How can we move toward anti-nuclear weapons?
Gary Holt
CFCCS @ HAWAII-EMH
------------------------------
Date: Monday, 10 November 1986 08:56-EST
From: LIN
To: cfccs at HAWAII-EMH.ARPA
cc: lin, arms-d
Re: prompt response
From: cfccs at HAWAII-EMH
Since we agree on most things, why do you still want a 24-hour wait?
This only serves to give the Soviet Union a greater chance of
surviving a war, and perhaps a hope that it might be pulled off
successfully.
As I pointed out in a previous message to another discussant, a 24
hour wait provides time to verify conclusively that an attack has
indeed happened, and to think about a proper response. There IS a
downside to waiting. I happen to think that it is worth paying
the cost of that downside to obtain conclusive confirmation of attack.
It is precisely because I agree with your statement that
I [Holt] don't think that anyone seriously believes the S.U. or U.S.
will begin a nuclear confrontation.
that I judge the odds of such an occurrence to be very low that I want
to be very sure that I have solid and conclusive evidence. If nuclear
attack were a very likely thing, I might require less evidence.
What
does matter is that the proliferation of nuclear technology and
weaponry is getting out of hand. That is what must be addressed!
I agree that it is an important problem, worth effort and energy in
solving. But I don't think that a terrorist nuclear weapon would
start World War III. The only possible ways for that to happen are if
the US or the SU get involved.
How are we protected against nuclear weapons held by fanatics with
nothing to lose?
Probably pre-emptive strikes are the only way.
------------------------------
Date: Monday, 10 November 1986 06:43-EST
From: cfccs at HAWAII-EMH
To: LIN, arms-d
Re: defenses, first strike
Some of the topics you mentioned have not died and are not on a trash heap.
They are just not being looked at by the military any longer. I would like
to hear some of the projects you have in mind that have better odds than SDI.
I would also like to remind you that the odds of SDI are based on *current*
Current technology changes daily. No one can predict the future. They only
guess. The odds of a successful space program weren't very good until
the Soviets did it first. I also would like to bring attention back to the
attention the Soviets are giving SDI. If the odds are so low, why are they
so concerned? Maybe the odds are not as low as has been let out!
Gary Holt
CFCCS @ HAWAII-EMH
------------------------------
Date: Mon, 10 Nov 1986 09:07 EST
From: LIN@XX.LCS.MIT.EDU
Subject: defenses, first strike
From: cfccs at HAWAII-EMH
I would like to hear some of the projects you have in mind that have
better odds than SDI.
A real defensive problem is building a man-portable anti-tank weapon
that will work against modern battle tanks. There is no such beast
now. Given a billion dollars in R&D money, I am quite certain that we
could build such a thing.
A big defensive problem in Europe is the rapid construction of
anti-tank barriers between East and West Germany. We should be
working on a way to create such barriers without raising West German
fears that the two Germanys will never be reunited.
The development of mines for anti-submarine and anti-tank warfare is
sadly lacking. Both would do much to improve U.S. conventional
defense posture.
I would also like to remind you that the odds
of SDI are based on *current* Current technology changes daily. No
one can predict the future. They only guess.
Are you willing to bet on the future of a faster-than-light weapon?
Is it worth research money? Is it worth research money given other
pressing needs?
The odds of a
successful space program weren't very good until the Soviets did it
first.
Not true. The U.S. has its own program underway when the Soviets
launched the first satellite.
I also would like to bring attention back to the attention the
Soviets are giving SDI. If the odds are so low, why are they so
concerned? Maybe the odds are not as low as has been let out!
The Soviet say they are concerned because it is easier to build a
defense against a ragged retaliation than against a first strike.
They note MX, Trident II, Pershing II and so on, and conclude that the
U.S. BMD program is part of a first strike strategy that will leave
them defenseless.
I don't think that's plausible, but I'm not a Soviet. Look at it from
THEIR perspective, and they're not so crazy.
------------------------------
Date: Monday, 10 November 1986 07:10-EST
From: cfccs at HAWAII-EMH
To: ARMS-D
Re: perfectness of SDI
The perfectness of SDI has nothing to do with an immediate dismantling
or a 100% retention of nuclear weapons. The plan is to reduce nuclear
weapons as the effectiveness of SDI increases. The plan also includes
releasing the SDI technology to the Soviets, but again, gradually.
Nothing of such a magnitud is done in one move of a chess piece. It
is done in steps with the goals changing along the way to meet
*current* needs. Of course the ultimate goal is to have a perfect
system! Why would anyone set a finite goal to build a faulty
anything? An engineer would build a machine that comes closest to his
ultimate goal rather than quit because he can't do the whole thing at
once.
CFCCS @ HAWAII-EMH
------------------------------
End of Arms-Discussion Digest
*****************************