[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



* Dietz Proepper wrote:
>> Eine formale Verifizierung der Abwesenheit von Fehlerklassen (bis hin zur
>> Abwesenheit aller Laufzeitfehler) ist heute schon möglich und wird gemacht.
>
> 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. 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.

> Hast Du Pointer auf "aktuelles"?

www.sparkada.com

>> Jedoch kaum bei Open Source.
>
> *g* work vs. fun...

Es ist Fun, zuverlässige Software zu schreiben. Es ist noch mehr Fun,
bewiesenermaßen partiell korrekte Software zu schreiben (das leistet SPARK
nur, wenn man formale Specs baut, z.B. in Z)

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