[Erotavlas_turbo]

Originariamente inviato da cdimauro

Gli ho già risposto, ma so che già non ti piacerà quello che ho scritto.

Anche pratica. Vedi la risposta di cui sopra.

E con ciò è chiaro che NON hai capito in cosa si fondi la dimostrazione.

I termini sono chiari, pratici e reali, e ciò che hai scritto NON si applica (perché risulta già nelle ipotesi) o non ha senso (stessa obiezione).

Rileggiti e analizza per bene la dimostrazione, cortesemente.

La dimostrazione è e rimane perfettamente valida, checché tu ne dica. E siccome non la puoi smontare, anche perché non l'hai capita (vedi sopra), vedo che non ti resta altro che cercare (inutilmente) di sminuirla.

Forse sei tu che non riesci a capire l'evidenza dei fatti.
Secondo la tua dimostrazione x open source considerato sicuro e y closed source derivato da x dove è cambiata solo la grafica, è ugualmente sicuro.
Questo formalmente non fa una piega.
Praticamente non ha alcun senso in quanto per poter affermare che y sia derivato da x devi avere accesso al codice sorgente per verificare che sia effettivamente cosi oppure deve esserci qualcuno che ti dia questa garanzia. Nel primo caso ricadiamo in y=x mentre nel secondo andiamo a fiducia che vale poco visti i vari scandali...

Originariamente inviato da cdimauro

Che si riconduce proprio al teorema dell'arresto. Stessa pagina, poco più avanti: Proof by reduction to the halting problem.

Il che dimostra due cose: che quella pagina non hai l'hai nemmeno letta tutta. E che, soprattutto, continui a parlare di cose di cui non hai conoscenza.

Si vede che tu non hai letto il mio messaggio.
Per valutare se un programma ha una certa proprietà occorre applicare il teorema di Rice.
Il teorema di Rice generalizza il problema dell'arresto a qualunque proprietà di un programma o funzione parziale. Il problema dell'arresto è un caso particolare fondamentale e usato per dimostrare la validità dell'altro. Inoltre, la dimostrazione di Turing al problema dell'arresto e l'applicazione del teorema di Cantor alle macchine di Turing.

Originariamente inviato da cdimauro

Cose per le quali io ho, invece, sputato sangue all'università, e che come vedi non soltanto comprendo, ma applico correttamente.

Veramente? Conosco molte persone che hanno fatto l'università con ottimo profitto (io compreso) e non ho mai visto nessuno sputare sangue.
Ho visto invece farlo a persone che lavorano in fabbrica, lavorano la terra e in generale che fanno lavori veramente duri non come studiare.
Forse ti conviene moderare i termini per rispetto di queste persone.

Originariamente inviato da cdimauro

Difatti se tu avessi abbozzato una definizione di software "sicuro" (che non è certo un caso che abbia condito di virgolette, visto che non ne esiste una oggettiva), t'avrei dimostrato che si sarebbe ridotta anch'essa al problema dell'arresto. Com'è ovvio (almeno per me) che sia.

Per quanto già detto, non ne ho affatto bisogno. Stai soltanto nonché malamente cercando di ribaltare la frittata spostando l'onere della dimostrazione a me, che ne ho già fornito una inattaccabile.

Anche se il 100% degli esperti di sicurezza fosse d'accordo con te, rimarrebbero opinioni personali. Perché NESSUNO di loro è in grado di smontare la mia dimostrazione. Come, peraltro, di fornire una definizione OGGETTIVA e INCONTROVERTIBILE di sistema / software "sicuro".

Ed è bene che tu ne cominci a prenderne atto.

Ti ho detto più volte che non sono interessato a una dimostrazione delle mie affermazioni anche perché non è matematicamente possibile sei tu che vuoi una dimostrazione.
Ti ripeto (ultima volta) il mio punto di vista basato sull'analisi dei dati a disposizione:
Essere open source (avere il codice sorgente a disposizione di tutti) è una condizione necessaria affinché un programma sia sicuro (possa essere valutata la sua sicurezza). Non è una condizione sufficiente come dimostrano alcune falle su openSSL e linux.

Dato che la matematica non può dimostrare questa affermazione in modo formale occorre utilizzare il metodo sperimentale usato nella scienza.
Quante teorie scientifiche esistono che non sono dimostrabili matematicamente, ma che si applicano ai dati e alla realtà dei fatti?! Praticamente tutte.
Prendiamo la fisica, quando una teoria considerata valida (meccanica classica) non riesce a spiegare il motivo di un nuovo fenomeno (corpi che viaggiano alla velocità della luce), occorre rivederla, eventualmente estenderla (meccanica relativistica) o formularne una nuova.
Torniamo al nostro caso: esiste un solo esempio reale che invalidi l'affermazione precedente e quindi lo renda non valido?!
Ovvero che essere open source (avere il codice sorgente a disposizione di tutti) non è una condizione necessaria affinché un programma sia sicuro.

Inoltre, non ho mai visto nessuno ricercatore di sicurezza affermare il contrario.
La quasi totalità afferma che essere open source è una condizione necessaria, qualche eccezione afferma che questo è un fatto secondario e che la licenza non conta.

Originariamente inviato da cdimauro

How many lines of code are in the Linux kernel?:

"9,868,933 lines of code, 12,020,528 lines with comments included, spread over 36,595 unique files.

Breakdown by language

C - 7,896,318 lines, 16,397 files
C/C++ Header files - 1,629,064 lines, 13,542 files
Assembly - 250,097 lines, 1,231 files"

Mi son fermato ai primi 3 che sono i più rilevanti. Lascio a te il calcolo del 10-20% di cui sopra, e se sei in grado di fornire una dimostrazione formale della sicurezza di Linux su questa base.

Anticipo una possibile nonché realistica risposta, a beneficio di chi legge il thread e che risulta digiuno in materia: su quella enorme base di codice, puoi soltanto fare un atto di fede nell'affermare che Linux sia "sicuro".

Vuoi dimostrare anche il principio di Pareto?! Non esiste una dimostrazione formale nemmeno per questo.
Questo principio è un punto di partenza valido e applicato nella realtà, non solo in informatica.
Vorresti fare un audit del codice di linux adesso quando il codice sorgente è una creazione di oltre 25 anni?
L'operazione è fattibile, ha un costo in termini di tempo e denaro. Il principio di Pareto afferma che è sufficiente controllare il 10-20% del codice per avere la sicurezza che il 90-80% del codice sia esente da bug. Se vuoi raggiungere il 100% di sicurezza, lo devi analizzare tutto.
Stesso ragionamento vale nell'ottimizzazione del codice per renderlo più efficiente.

Originariamente inviato da cdimauro

Ma anche prendendo software di gran lunga più semplice e piccolo come TrueCrypt, che in passato è stato citato come software che è stato dimostrato essere formalmente sicuro, ho già avuto modo di evidenziare notevole pecche / lacune dell'audit, e che infine gli stessi autori caldeggiassero una verifica formale.

Questo per ribadire l'ovvietà: il 10-20% di codice di cui parli rimane comunque TROPPO.

Non ho ben capito: prima dici che TrueCrypt è stato citato come software dimostrato formalmente sicuro e poi che gli autori volessero una dimostrazione formale?
Il 10-20% è troppo?! Conviene fare una verifica formale o analizzare il 10-20% del codice critico in termini di tempo e soldi?

Originariamente inviato da cdimauro

A parte il fatto che adesso sei scaduto nella mistificazione cercando di mettermi in bocca cose che non mi sono mai sognato di dire/negare, la questione primaria è e rimane l'ACCESSIBILITA' dei sorgenti.

Mentre tu continui a farne una battaglia ideologica open vs closed, che non c'entra nulla nei riguardi dei termini della questione, oltre al fatto che ho DIMOSTRATO essere falsa.

Misitificazione?!
Come ti ho detto N volte con N molto grande , essere open source (qualunque licenza) per definizione rende disponibili il codice sorgente a tutti cosa impossibile con closed source. Per questo essere open source ovvero avere il codice sorgente è una condizione necessaria.

Originariamente inviato da cdimauro

Su questo mi sono già espresso: SE fosse come riporti (e ho i miei dubbi, visto che ti è molto facile mettere in bocca alla gente cose che non si sono sognate di dire. E che peraltro non sarebbero qui a correggerti), sarebbero in ogni caso in torto, visto che ho DIMOSTRATO che tale asserzione sia falsa.

Per vedere cosa riporto in bocca, basta leggere quello scritto nei messaggi precedenti.

Originariamente inviato da cdimauro

E invece sì, visto che le asserzioni sono passibilissime di essere smontate. Non stiamo parlando di frutta e verdura, o roba da bar dello sport, ma di questioni squisitamente tecniche. Anzi: matematiche.

Vedi sopra riguardo ai miei dubbi su ciò che riporti, e rimane in ogni caso la mia DIMOSTRAZIONE.

Certo, infatti tutte le teorie scientifiche reali, invenzioni e in generale tutto cià che funziona e si applica alla realtà è dimostrabile...

Originariamente inviato da cdimauro

Non è nemmeno una congettura, veramente. Le congetture, come già detto, si basano su (NUMEROSI) FATTI che lasciano ipotizzare/costruire induttivamente una certa via.

Qui finora sono soltanto spese parole, al massimo del tutto autoreferenziali: tizio ha detto questo e quest'altro. Chiacchiere.

Ovvio: so bene che è impossibile averla.

Il che non significa nulla riguardo ai termini della questione.

Oltre al fatto che, prendendo in prestito queste tue parole, le potrei benissimo e tranquillamente applicare a qualunque software, anche closed.

Una congettura è una affermazione o un giudizio fondato sull'intuito, ritenuto probabilmente vero, ma non dimostrato. Cioè un'ipotesi.
In matematica il termine trova un'applicazione quantomai appropriata: una congettura matematica è infatti un enunciato formulato da uno o più matematici che lo ritenevano probabilmente vero, per il quale non è tuttora conosciuta una dimostrazione.

L'informatica è piena di congetture ed euristiche...

Dove sarebbe il problema? Riportami dove ho detto di voler dimostrare qualcosa? Tu sei fissato con dimostrazioni non dimostrabili.
L'evidenza dei fatti fa dedurre quanto affermato da me in precedenza anche in questo messaggio, poi puoi benissimo credere a quello che vuoi.

Originariamente inviato da cdimauro

Detto in altri termini: ti stai smentendo con le tue stesse mani.

Vediamo adesso cosa t'inventerai per sostenere le tue asserzioni. Perché non ti rimane altro che inventare, considerato che risulta piuttosto evidente che tu non abbia le competenze / conoscenze per affrontare argomenti come questi.

Risulta evidente una cosa: tu ti ostini a chiedere una dimostrazione formale di una cosa che non può essere dimostrata come hai fatto notare anche più volte.
Io sto cercando di farti vedere la realtà oggettiva dei fatti, supportata da quasi la totalità dei ricercatori di sicurezza (non ne ho trovati con pareri contrari, riportali se ne conosci), ovvero che avere un software open source è necessario affinché il software sia sicuro.
Solo avendo il codice sorgente è possibile verificare la validità del programma. Questo non è possibile con un codice closed source.