Re: [FYI] Ross Anderson - Open and closed security are roughly equivalent

[Lutz Donnerhacke <lutz@iks-jena.de>]

* Martin Uecker wrote:
> On Wed, Feb 12, 2003 at 09:56:41PM +0000, Lutz Donnerhacke wrote:
>> > Letzteres ist auch bei abstrakter ("hochsprachlicher") Formulierung
>> > aufwendig bis unmöglich, ersteres wird nicht wesentlich aufwendiger.
>>
>> Eine formale Verifizierung der Abwesenheit von Fehlerklassen (bis hin zur
>> Abwesenheit aller Laufzeitfehler) ist heute schon möglich und wird gemacht.
>> Jedoch kaum bei Open Source.
>
> Eigentlich nie, oder kennst Du ein Beispiel?

Das CA System von Mondex, Hubschrauber, Rakten und Flugtechnik.

> Aber Verifiziert wird auch seltenst bei Closed Source.

Das ist ein anderer Punkt.

> Und selbst dann heißt "Abwesenheit aller Laufzeitfehler" auch nur, daß
> die Runtime-Umgebung nicht kollabiert, und keineswegs, daß das Programm
> zur Laufzeit keine Scheiße baut.

Es sind drei Schritte:
  - Abwesenheit von Laufzeitfehler heißt: Keine Bereichsüberschreitungen
    für Feldgrenzen, Überläufe in der Arithmetik, keine Division durch Null,
    etc. pp. Das kann man maschinell beweisen.
  - Partielle Korrektheit. Das kann man maschinell beweisen.
  - Totale Korrektheit. Das ist nach der partiellen Korrektheit leichter,
    wird nicht maschinell angeboten.

Maschineller Beweis heißt, daß man ca. 90% des Codes als Korrekt abharken
kann und der Rest mit konktreten Randbedingungen hochschlägt.

> Programmen in einer Ada-Variante die Abwesenheit von Fehlern zu beweisen
> bringt IMHO wesentlich weniger, als von vornehein eher deklarative
> Programmiersprachen zu benutzen und die Zeit besser in deren Optimierung
> zu stecken.

;-) YMMV.

-- 
To unsubscribe, e-mail: debate-unsubscribe@lists.fitug.de
For additional commands, e-mail: debate-help@lists.fitug.de