Re: Heartbleed

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 14-04-12 21:15 , Pascal J. Bourguignon wrote:
> Simon Wright <simon@pushface.org> writes:
> 
>> "Pascal J. Bourguignon" <pjb@informatimago.com> writes:
>>
>>> But strongly late dynamically typed programming languages are probably
>>> better for mission critical systems, since they can adapt dynamically
>>> the type of the values at run-time, instead of crashing.
>>
>> If the system designers have thought about what to do under such
>> circumstances so that the system can carry on, OK,
>>
>> If not, the system is operating outside its design envelope, which I
>> think is equivalent to the Ada "erroneous behaviour; so you don't know
>> _what_ it will do, and the best response is probably to fall back to a
>> pre-planned recovery mode. Or, as you say, to crash; which has at least
>> the virtue, during development, of making it obvious that there's a
>> problem to be fixed.
> 
> The Ariane 5 and Mars Climate Orbiter are proof that this is not the
> right methodology.  Those systems were specified, developed with crashes
> and erroneous behaviour during development, and all bugs were obvious
> (to the point of making big explosions).  Oops, too late!

Your irony makes it hard to understand what you really mean.

So what would have been a better approach for the Ariane 5? As I
understand it, the catastrophic failure was not due to any SW technology
issue, but to the human choice of the wrong recovery action for a
particular run-time error (value out of range) which occurred in
different circumstances in the Ariane 4 and the Ariane 5. Nothing to do
with static typing, all to do with FMECA and proper requirements management.

How would the use of any other typing style have prevented the failure?
It seems to me that (given the choice of recovery action) the only
alternative would be not to detect the out-of-range value, which could
create other failure modes.

As for the Mars Climate Orbiter, the reason for that failure was a
mix-up of physical units of data: the producer and consumer assumed
different units, leading to "controlled but unintended flight into
atmosphere". That would have been difficult to prevent with any typing
scheme. Even if the concept of type in the programming language would
have included physical units, the data were computed in one program and
then transferred as input for another program, breaking the
type-checking chain. A failure of interface control and documentation.

> There are life-or-death systems that needs to continue running, even in
> a degrated mode, whatever happens, whatever bug they may still contain
> once deployed. 

"Whatever bug" is a bit unrealistic. But then, it depends on how far you
are willing to degrade the behaviour :-)

> Statically checked, variable-typed languages aren't up to the job for
> those systems.

That seems to be disproved by current and long practice. Remembering
that nothing is perfect, of course.

> There will always be bugs remaining, even in tested and more
> importantly, even in proven software!  Cf. for example, the Deep Space 1
> RAX software, written in Lisp, and proven!  Despite the proof, a bug
> remained.  If it had been a statically checked programming language, it
> would have meant a terminal dead-lock or a crash (what else to do with a
> static language when we reach a state that has been proved impossible?).

The usual: raise an exception to abandon that computation and to discard
the weird (part of) the state, then continue, if necessary in a degraded
mode.

Even if the SW is 100% correct, HW failures (for example,
radiation-induced bit-flips) can create unexpected states, and the SW
must have some resiliency for that. But some bit-flips are recoverable
only by reboot, whether the language is static or dynamic.

> But since it was a dynamic programming language, (with very late
> binding, including a on-board compiler), it was debugged and patched
> remotely, as a last ressort solution.

The programming language and compiler location are mostly irrelevant to
that. Software in spacecraft is routinely debugged remotely (but usually
not interactively) and patched in flight, whatever the language and
whether it is compiled to machine code or to some VM code. The most that
can be said IMO is that using a VM helps to isolate the code running in
the VM (perhaps less trusted) from the code running natively (perhaps
more trusted).

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .