[OT] software ed errori [Era: OpenSSL: Altro bug]
Ciao,
Innanzitutto cito Davide...
> Il 09/06/2014 21:49, Davide Prina ha scritto:
>> ahi, ahi, ahi... top quoting... questo è male ;-)
>>
>> fare il top quoting impedisce una corretta lettura del discorso e
>> causa una difficile risposta.
Ora veniamo al dunque.
Il Mar, 10 Giugno 2014 9:38 am, franchi@modula.net ha scritto:
> Non importa se poi l'errore è del tuo comando o della shell o di chissà
> cosa: il fatto è che il sistema, nel suo complesso, può produrre
> risultati diversi da quelli che ci aspettiamo.
Invece importa, se l'errore non è nel mio comando, non puoi imputare il
bug al mio software. Inoltre non bisogna confondere i bug dagli errori
estemporanei. Se un surriscaldamento, un raggio cosmico o un altro evento
del genere possono generare errori imprevedibili nell'esecuzione di un
software, questo non significa che il software abbia bug (anche se
certamente è possibile scrivere software più resiliente di altri nei
confronti di eventi del genere).
Il bug di OpenSSL da cui è partita questa discussione era tale che, al
verificarsi di un evento riproducibile a volontà, OpenSSL
_sistematicamente_ e _prevedibilmente_ permetteva di aprire una falla di
sicurezza, indipendentemente da errori di compilazione, hardware
malfunzionante o simili "incidenti"... Di questo stiamo parlando.
> se meriterebbe rifletterci): voglio solo dire che la complessità del
> software non è completamente dominabile e che anche in questo campo si
> procede per errori e correzioni come in qualsiasi altro ambito
> scientifico.
Io penso si debba distinguere tra scienza e tecnologia.
Forse la tecnologia procede per errori e correzioni, non mi pronuncio.
La scienza dovrebbe procedere per teorie, verifiche e dimostrazioni; chi
commette errori grossolani di solito non usa il metodo scientifico e
magari ha finge di poter estendere la validità di una teoria al di fuori
del suo ambito di applicazione.
Tanto per fare un esempio in breve, dire una cosa come "la meccanica
relativistica Einsteiniana è la versione corretta della meccanica
classica di Galileo e Newton che era un errore" sarebbe una sciocchezza.
La meccanica classica continua a fornire previsioni attendibili se le
masse, i tempi, gli spazi e le velocità in gioco, assieme alla precisione
richiesta dalla previsione non eccedono certi limiti. Scommetto che chi
progetta mezzi di trasporto terrestri continua (correttamente) ad usarla
senza tener conto delle "correzioni" relativistiche. Scommetto anche che
chi progetta la traiettoria di "astronavi" usa la meccanica Einsteiniana e
non la quantistica... e chi... etc etc.
Un esempio più informatico potrebbe essere l'articolo di chi ha proposto
i B-heap [ http://queue.acm.org/detail.cfm?id=1814327 ]. L'autore fa
notare che per i computer moderni non è valida l'ipotesi di costo
costante per un accesso in memoria indipendentemente dalla locazione, ne
conclude quindi che usare la teoria classica per implementare un heap,
oggi, è sbagliato. Anche in questo caso sarebbe sciocco dire che quella
teoria contiene un errore, quando questo è nel suo uso (tecnologico?)
fuori dalle ipotesi.
Detto questo, le teorie scientifiche restano certamente tutte
falsificabili, lungi da me sostenere che affermino "la verità". Descrivre
però il metodo scientifico come "errori e correzioni" è un po'
riduttivo.
>> meglio dire che non esiste un metodo automatico che possa essere usato
>> per dimostrare la correttezza di un software qualsiasi.
Questa frase è di Davide (infatti concordo ;-); giustamente non esclude
la possibilità di dimostrare la correttezza di software specifici!
Anche qui, vale la pena fare un esempio, magari un po' più significativo
del "return 0"... va bene un intero compilatore?
Non è software libero (ha una clausola che ne esclude l'uso commerciale;
anche se ampie porzioni del codice sono rilasciate con doppia licenza,
talvolta affiancando la BSD, talaltra GPL o LGPL) ma bisogna ammettere che
CompCert [ http://compcert.inria.fr/ ] è un progetto estremamente
interessante: si tratta di un compilatore la cui correttezza è (quasi
completamente) certificata da sistemi di dimostrazione automatica!
Certo, scrivere oltre al software (e alla documentazione :-) anche il
sistema di teoremi che ne dimostrano la correttezza richiede _MOLTO_ più
tempo che andare per tentativi affidandosi alla propria esperienza e alle
revisione di colleghi e (nel caso del software libero) volenterosi per
commettere meno errori possibile.
Si può certamente sostenere (ci sono validi argomenti a supporto) che per
software "troppo" complessi, che devono anche velocemente adattarsi alle
innovazioni tecnologiche (come OpenSSL), l'approccio della dimostrazione
automatica sia impraticabile...
Bisogna però ammettere che c'è gente tutt'altro che ignorante che usa un
approccio (davvero) scientifico per scrivere software con certificazione
della correttezza.
Per installare il compilatore citato, bisogna scaricare dal sito il
sorgente (verificare l'impronta hash); aver installato gcc, coq, menhir,
ocaml; eseguire "./configure <opzioni> && make" e ... aspettare un tempo
piuttosto lungo che tutti i teoremi necessari vengano dimostrati ;-)
Buon divertimento ;-)
m
--
http://bodrato.it/papers/
Reply to: