[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [FYI] Ross Anderson - Open and closed security are roughly equivalent
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