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

[Dietz Proepper <dietz@rotfl.franken.de>]

Lutz Donnerhacke:
[Verifikation]
> > Das Ganze war auch schon von 15 Jahren möglich und wurde (zumindest auf
> > dem Papier) auch gemacht. Leider kann man einfach zeigen das "alle"
> > automatisch nicht geht. Schon sind wir wieder bei harter Handarbeit,
> > diese ist fehlerträchtig und keine prinzipielle Verbesserung über
> > "n-Augen".
>
> Ich rede von einem automatisierten Beweis der Laufzeitfehlerfreiheit, der
> eine Abdeckung von über 90% erreicht.

Abdeckung im Bezug auf was? Lines of Code? Nett aber eher uninteressant da man 
dergleichen durch klassische Tests mit coverage-Analyse auch erreicht.
Im Bezug auf Fehlerklassen? Glaube ich nicht. Bzw. habe bei den SPARKs hierzu 
nichts gefunden was einem Beweis dieser Aussage auch nur nahe kommt. Und ohne 
Beweis ist so eine Aussage eher wertlos.

> Die wenigen Zeilen, die in solchen
> Prjekten dann noch übrigbleiben werden mit klaren Randbedingungen
> angegeben, so daß man sich überlegen kann, ob es wirklich notwendig ist,
> den 32bit Sekundenzähler der Uptime eines medizinischen Geräts tatsächlich
> auf Überlauf zu testen.

Wenn man automatisiert so weit kommt wäre dies äußerst wertvoll. Ich würde 
ohne einen Beweis dieser These aber Magenschmerzen bekommen.

> > Hast Du Pointer auf "aktuelles"?
>
> www.sparkada.com

Den pointer auf die selbst überprüfbare "Demo" habe ich übersehen. Nach kurzem 
Querlesen bin ich wirklich beeindruckt, wieviele tolle Dinge damit gemacht 
wurden. Nach etwas längerem Querlesen fällt mir auf daß sie zumindest ein 
gutes Marketing haben. Ebenfalls übersehen habe ich wohl den Part in welchem 
sie Regress zusichern, sollten ihre claims übertrieben sein.

Zusammengefasst - es sieht den letzten 50 magic bullets leider recht ähnlich.

> >> Jedoch kaum bei Open Source.
> >
> > *g* work vs. fun...
>
> Es ist Fun, zuverlässige Software zu schreiben. Es ist noch mehr Fun,

Nicht wenn man zunächst zu toolmonger mutieren muß ;).

> bewiesenermaßen partiell korrekte Software zu schreiben (das leistet SPARK
> nur, wenn man formale Specs baut, z.B. in Z)

Man möchte bewiesenermaßen korrekte Software schreiben. Alles andere scheint 
mir eher formalisierter Selbstbetrug, sorry.

Grüß' Gödel von mir,
	Dietz

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