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

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

* Martin Uecker wrote:
> On Thu, Feb 13, 2003 at 04:55:57PM +0000, Lutz Donnerhacke wrote:
>> > Eigentlich nie, oder kennst Du ein Beispiel?
>>
>> Das CA System von Mondex, Hubschrauber, Rakten und Flugtechnik.
>
> Mißverständnis. Ich wollte eigentlich wissen, ob es ein 
> Open Source-Projekt gibt, das sowas macht.

Mir nicht bekannt.

> Beweis von Korrektheit setzt eine Spezifikation voraus.

Korrekt.

> Die kann aber auch fehlerhaft sein.

Richtig. Man bemerkt dann aber schnell viele Specfehler.

> Das ganze bringt also nicht so viel, wie man vielleicht denken könnte.

Die Abwesenheit von Fehlerklassen bewiesen zu haben, bringt unheimlich viel.
Z.B. keine Abstürze mehr. Oder fester RAM Bedarf. Dann kann man das auf
einen Chip/Platine gießen ohne Angst haben zu müssen.

Und für den Beweis der Abwesenheit von Laufzeitfehlern braucht man keine
formale Spezifikation.

> Aber selbst dann wird man für komplexe Programmsysteme, die in
> imperativen Sprachen geschrieben sind, niemals irgenwelche komplizierten
> Eigenschaften beweisen können.

Beweis durch Behauptung? Warum klappt das dann in den o.g. Beispielen?

> Aber es gibt Sprachen, die beweistechnisch wesentlich einfacher zu
> behandeln sind, und selber schon eine Art Spezifikationssprache in Form
> eines mächtigen Typsystems eingebaut haben. Meckert der Typechecker
> nicht, hat das Programm die im Typ spezifizierten Eigenschaften (siehe
> Curry-Howard-Isomorphismus).

Spark geht noch weiter und prüft die Imperativen Statements, den
Informations- und Datenfluß und einige kleine Stilfragen.

> Das ist in heute verfügbaren Sprachen wie Haskell noch kaum ausgereizt,
> aber z.B. Haskell ist IMHO schon heute der bessere Weg zu robuster
> Software als Ada + Z. Vielleicht nicht für Raketensteuerungen - aber
> darum ging es hier nicht.

Richtig. Darum geht es hier nicht. Es geht darum, daß es machbar ist und
gemacht werden sollte. Ob irgendwann mal mit Haskell oder jetzt und hier mit
Spark.

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