Re: RISC-V: quanta parte del processore ha licenza libera?
Il 01/03/21 20:56, Davide Prina ha scritto: [...] In generale Debian è ritenuta: * contenere solo software libero (quindi se vuoi/devi installare parti proprietarie è sconsigliata, non funziona su determinati hardware, ...) * contenere software non aggiornato da tanto tempo (parlano di stable... e quindi sconsigliano l'uso per chi non vuole avere software obsoleto che non funziona su hardware recente) * viene rilasciata ogni morte di papa e non si sa mai la data in cui sarà rilasciata (questa era la politica del rilascio di stable) * è usata/usabile solo per server non si capisce perché molti parlino ed esprimano giudizi su cose che non conoscono... Ma in effetti non c'è da stupirsene... Piviul
Verifiche formali di programmi [era: Ripristino GRUB2 e conversione GPT...]
Saluton Marco, Il 2021-03-01 19:37 Marco Ciampa ha scritto: ecco, diciamo che lo hai detto meglio ma il "succo" è lo stesso... perdonami Non proprio lo stesso... È un po' come la differenza tra "in Italia ci sono dei mafiosi" e "gli italiani sono tutti mafiosi". Il non distinguere tra le due di solito porta a gravi conseguenze :-P ...e non solo parlando di Italia e di mafia. Per fare un esempio che potrebbe non interessare molte persone, ma che affascina enormemente me, c'è un'intera libreria di calcolo matematico in precisione arbitraria che è formalmente verificata: https://gitlab.inria.fr/why3/whymp Interessante. Domanda da profano: verifica formale equivale ad assenza di bachi o semplicemente indica che quello che viene descritto nell'algoritmo (che potrebbe avere dei problemi) viene correttamente Per fare un esempio interno alla libreria citata, la verifica formale fatta dagli autori (pubblicata e riproducibile) di una funzione come "radice quadrata intera di un intero" garantisce che la funzione non legga/scriva in aree di memoria diverse da quelle in cui può leggere/scrivere. Garantisce anche che per qualunque intero "arbitrariamente" lungo x fornito come argomento, venga fornito nel formato atteso un risultato r tale che r^2 <= x < (r+1)^2. Certo, se qualcuno usa la funzione powm per l'esponenziazione modulare da quella libreria e ci costruisce sopra della crittografia RSA; la libreria garantirà che le potenze-modulo diano il risultato matematicamente corretto partendo da quel che le verrà dato in pasto. Se pero il programma che usa la libreria è sbagliato o la crittografia RSA non è sicura, non sarà l'uso di una libreria formalmente verificata ad eliminare questi problemi. Perché questa chiacchierata non scivoli troppo nel fuori luogo (Off Topic), l'infrastruttura di programmi che serve per verificare queste dimostrazioni è presente in Debian, nel pacchetto why3 https://packages.debian.org/source/sid/why3 Un primo germe della libreria che ho indicato è presente nel pacchetto why3-examples ed una volta installatolo si trova in /usr/share/doc/why3-examples/examples/multiprecision Per un matematico 0,99\ \ è completamente diverso da 1. Dillo ad una cassiera del supermercato e sta pronto ad abbassare la testa... ;-) Prova a dirlo tu alla stessa persona che invece di digitare 1 sulla cassa può tranquillamente scrivere 0 seguito dalla sfilza di 9 che hai proposto, oppure prova a dirlo ad una tipografa che quelle tre righe di 9 sono la stessa cosa di un singolo "1" e vedrai che le opinioni in proposito sono più variegate di quelle che ti aspettavi :-) Poi suvvia, sono sicuro che esistano anche cassiere del supermercato acculturate, capaci di cogliere le sottigliezze, come chessò... la differenza tra software libero e software gratuito! E se per caso la capacità di discernere non è sufficientemente diffusa, bene adoperiamoci perché lo sia! vedi che anche tu guardi le probabilità e non le certezze matematiche? L'importante è non confonderle! Ĝis, m
RISC-V: quanta parte del processore ha licenza libera?
Leggendo questo articolo: https://hackaday.com/2021/02/27/exploring-the-open-source-that-really-goes-into-a-risc-v-chip/ e guardando il filmato indicato (purtroppo è in inglese): https://www.youtube.com/watch?v=VdPsJW6AHqc è possibile capire molto di più cosa sia RISC-V e come sono distribuite le sue componenti. Leggendo vari articoli mi ero fatto l'idea che l'intero RISC-V più tutto quello che gli gira attorno fosse distribuito con licenze libere... ...vedendo però il filmato si capisce che non è affatto così, anche se vi sono degli spunti positivi che potrebbero di avere in un futuro, purtropo non troppo vicino, un hardware con licenze completamente libere. C'è anche una parte dove si parla di Debian, con un errore nel sito visualizzato. Mi sono accorto che ogni distro si è fatta una fama e tutti dichiarano per vero tale fama, anche se non è così ora o non è mai stato così (un po' come l'errore di pubblicazione sugli spinaci che gli davano una quantità di ferro astronomica, quando in realtà vi sono altri vegetali che ne contengono di più, ma ormai per tutti gli spianaci sono i vegetali che hanno più ferro di qualsiasi altro). In generale Debian è ritenuta: * contenere solo software libero (quindi se vuoi/devi installare parti proprietarie è sconsigliata, non funziona su determinati hardware, ...) * contenere software non aggiornato da tanto tempo (parlano di stable... e quindi sconsigliano l'uso per chi non vuole avere software obsoleto che non funziona su hardware recente) * viene rilasciata ogni morte di papa e non si sa mai la data in cui sarà rilasciata (questa era la politica del rilascio di stable) * è usata/usabile solo per server * ... Ciao Davide -- Elenco di software libero: http://tinyurl.com/eddgj GNU/Linux User: 302090: http://counter.li.org Non autorizzo la memorizzazione del mio indirizzo su outlook
Re: Ripristino GRUB2 e conversione GPT...
On 01/03/21 18:37, Marco Bodrato wrote: Il 2021-03-01 17:31 Marco Ciampa ha scritto: NESSUN tool, né commerciale né libero, garantisce al 100% la riuscita dell'operazione. Equivarrebbe a dire che il sw è senza alcun baco, cosa che è dimostrabile matematicamente che è impossibile. Questa frase non si capisce tanto :-) Probabilmente si può dimostrare matematicamente che esistono programmi la cui correttezza non è dimostrabile, "parafrasando" il teorema di Goedel. ma anche, come diceva il mio prof di metodi, non esiste nessun programma che fornisce sempre un risultato errato o, in altre parole, che c'è sempre qualcuno che può considerare corretto il risultato finale che per te è errato :-) Quindi un bug, per un utente, può essere il comportamento corretto per un altro :-) e negli utlimi, anni blasonate case produttrici di microprocessori ci hanno purtroppo abituato alla sciatteria più vergognosa. purtroppo, alcune di queste case hanno cercato le sole prestazioni, senza considerare per nulla la sicurezza... almeno la sicurezza di chi comprava i loro prodotti. In questi ultimi anni gli esperti di sicurezza stanno avendo strumenti per poter fare test sull'hardware in tempi/costi accettabili e stanno scoprendo un sacco di cose: * progettazione di hardware senza la minima considerazione di rendere sicure le operazioni eseguite * presenza di istruzioni macchina non documentate... * ... il problema è che per noi utenti questi sono bug, ma per altri invece sono funzionalità attese! :-( Ciao Davide -- Client di posta: https://www.thunderbird.net GNU/Linux User: 302090: http://counter.li.org Non autorizzo la memorizzazione del mio indirizzo su outlook
Re: [Forse un po' OT] Aiuto per uno script - RISOLTO
On 01/03/21 17:31, Giuliano Grandin wrote: https://fatsort.sourceforge.io/ riordinando la fat della chiavetta, scrive molte più volte che non usandolo e questo deteriorerà la pennetta in modo più rapido. È corretto? in teoria sì, ma bisogna vedere come fa a fare quell'ordinamento, inoltre se devi aggiungere un nuovo file per riordinarli dovresti rimuoverli tutti e riscriverli. Infine, da quello che ho letto, gli SSD di ultima generazione supportano un numero di riscritture davvero elevato. Ciao Davide -- Browser: http://www.mozilla.org/products/firefox GNU/Linux User: 302090: http://counter.li.org Non autorizzo la memorizzazione del mio indirizzo su outlook
Re: [Forse un po' OT] Aiuto per uno script
On 01/03/21 15:47, Enrico Agliotti wrote: Davide Prina ha scritto: 2) reimpostare IFS per evitare che il ciclo for spezzi i nomi contenenti spazi, es: OLDIFS=$IFS IFS=" " for ... ... done IFS=$OLDIFS Ho provato anche a impostare IFS=" " e mi sembra funzioni comunque. è vero, hai fatto un ciclo tipo: for f in *; do di solito io uso qualcosa del genere for f in $(ls *); do dove "ls *" in realtà è spesso qualcosa di più complesso con più comandi in pipe che poi spezza i file con spazi Ciao Davide -- I didn't use Microsoft machines when I was in my operational phase, because I couldn't trust them. Not because I knew that there was a particular back door or anything like that, but because I couldn't be sure. Edward Snowden
Re: errore signature verification in testing
On 26/02/21 08:21, Piviul wrote: $ sudo apt update Get:1 http://deb.debian.org/debian bullseye InRelease [142 kB] Err:1 http://deb.debian.org/debian bullseye InRelease Unknown error executing apt-key Erano anni che non vedevo problemi sulle chiavi dei repository... Prima di tutto io passerei ad usare la versione https al posto della http. Poi aggiornerei gli indici # apt update Poi reinstallerei le chiavi dei repository Debian # apt install --reinstall debian-archive-keyring Verificherei che non vi sia qualche errore nell'installazione dei pacchetti # apt -f install apt-key è deprecato, ma può essere ancora usato per visualizzare l'elenco delle chiavi e cancellarle. per vedere l'elenco: # apt-key list indica il contenuto di /etc/apt/sources.list indica se vi sono file in # ls /etc/apt/sources.list.d e il loro contenuto. Un'altra cosa che si può fare è verificare i pacchetti con debsums (se pensi che il tuo sistema possa essere compromesso, allora dovresti eseguirlo avviando il sistema su quella macchina con una live) Ciao Davide -- I lati oscuri del secure boot: https://www.fsf.org/campaigns/secure-boot-vs-restricted-boot/whitepaper-web Petizione contro il secure boot: https://www.fsf.org/campaigns/secure-boot-vs-restricted-boot/statement GNU/Linux User: 302090: http://counter.li.org Non autorizzo la memorizzazione del mio indirizzo su outlook
Re: Ripristino GRUB2 e conversione GPT...
On Mon, Mar 01, 2021 at 06:37:13PM +0100, Marco Bodrato wrote: > Saluton, Marco! > > Il 2021-03-01 17:31 Marco Ciampa ha scritto: > > On Sat, Feb 27, 2021 at 01:55:15AM +0100, Sabrewolf wrote: > > > NESSUN tool, né commerciale né libero, garantisce al 100% la riuscita > > dell'operazione. Equivarrebbe a dire che il sw è senza alcun baco, cosa > > che è dimostrabile matematicamente che è impossibile. > > Questa frase non si capisce tanto :-) > > Probabilmente si può dimostrare matematicamente che esistono programmi la > cui correttezza non è dimostrabile, "parafrasando" il teorema di Goedel. ecco, diciamo che lo hai detto meglio ma il "succo" è lo stesso... perdonami non sono un matematico, sono un praticone / smanettone > Ti assicuro però che per funzioni sufficientemente specifiche è possibile > dimostrare matematicamente che fanno esattamente quel che dovrebbero, senza > bachi. Questo lo so. So anche che funzioni specifiche non sono programmi. Sostanzialmente programmi non banali sono impossibili da verificare, per le cose che dici tu stesso sotto. Questa è una cosa che si sa, anzi che sanno tutti, non è che stia dicendo una cosa rivoluzionaria. Tant'è che _tutti_ i programmi hanno una licenza che espressamente toglie qualsiasi responsabilità per errori. > Per fare un esempio che potrebbe non interessare molte persone, ma che > affascina enormemente me, c'è un'intera libreria di calcolo matematico in > precisione arbitraria che è formalmente verificata: > https://gitlab.inria.fr/why3/whymp Interessante. Domanda da profano: verifica formale equivale ad assenza di bachi o semplicemente indica che quello che viene descritto nell'algoritmo (che potrebbe avere dei problemi) viene correttamente implementato? Perché non mi pare che le due cose si equivalgano, ma qui vado in un campo di cui non so niente per cui potrei dire delle cavolate. > Va da sé che poi servirebbe anche la verifica formale del compilatore, la > verifica formale dell'hardware sul quale il software gira... e negli utlimi, > anni blasonate case produttrici di microprocessori ci hanno purtroppo > abituato alla sciatteria più vergognosa. A ecco infatti mi pareva che ci fosse "il trucco". Ergo, non si può mettere la mano sul fuoco su niente... anzi, si può quasi fare il contrario e scommettere sui problemi... > Ma tra la grande complessità e l'impossibilità matematica, c'è differenza > :-D ... c'è differenza ... per un matematico. Per un matematico 0,99\ \ è completamente diverso da 1. Dillo ad una cassiera del supermercato e sta pronto ad abbassare la testa... ;-) Diciamo che è molto difficile provare la correttezza formale di un programma. Contento? ;-) > Chi in questi anni ha prodotto CPU scadenti, o venduto software con una > bella confezione, tanta propaganda e poca qualità, non è giustificabile da > una presunta impossibilità matematica di lavorare bene. Ma anche no. Ci sono i difetti di fabbricazione, i raggi cosmici, la radioattività naturale, gli effetti quantici, ecc. ragioni per non avere la certezza della correttezza ce ne sono a bizzeffe... Inoltre la complessità computazionale aumenta esponenzialmente la probabilità di problemi per cui hai quasi la certezza matematica (ho messo il quasi, ok?) che ci siano problemi. Se la certezza è 1 allora il mio "quasi" somiglia al numero espresso sopra... > Che poi errare sia > umano (e perseverare anche) è cosa che tutti sappiamo, ma non ne facciamo > una gistificazione matematica o scientifica, che sarebbe altra cosa. Si ma io sono un _pratico_ e dico che _praticamente_ assumo che i programmi abbiano bachi, _tutti_ i programmi. Se sbaglio, sbaglio di poco, molto poco. La differenza con 1 di cui sopra. > > > Cioè, se non vuoi "perdere i dati" allora significa che sono > > > importanti e quindi dovresti avere già un backup e quindi anche se > > > perdi > > > i dati il problema non si pone :-D > > > > Esatto. Il metodo è: faccio backup, cancello la partizione, la ricreo > > GPT, ricopio i dati. Questo funziona al 100%, per forza. > > Questo metodo è lento... e non "funziona al 100%, per forza". > Hai tenuto conto dei bachi del software per fare il backup? Della > possibilità che il disco di backup sia difettoso? Certamente e infatti i backup vanno verificati, e la norma 321 dice anche che bisogna farne almeno due... > Un metodo più veloce nel caso medio e non troppo più lento nel caso peggiore > e comunque più sicuro è: > > Faccio il backup (questo è imprescindibile) ok > Non cancello i dati, ma uso il software che mi promette di funzionare nella > maggior parte dei casi per fare la conversione. se c'è... e se il tempo che perdi a cercare di fare la conversione è superiore al tempo necessario ad _avviare_ (mica stai li a guardare no?) il backup, recover e controllo, allora
Re: Ripristino GRUB2 e conversione GPT...
Saluton, Marco! Il 2021-03-01 17:31 Marco Ciampa ha scritto: On Sat, Feb 27, 2021 at 01:55:15AM +0100, Sabrewolf wrote: NESSUN tool, né commerciale né libero, garantisce al 100% la riuscita dell'operazione. Equivarrebbe a dire che il sw è senza alcun baco, cosa che è dimostrabile matematicamente che è impossibile. Questa frase non si capisce tanto :-) Probabilmente si può dimostrare matematicamente che esistono programmi la cui correttezza non è dimostrabile, "parafrasando" il teorema di Goedel. Ti assicuro però che per funzioni sufficientemente specifiche è possibile dimostrare matematicamente che fanno esattamente quel che dovrebbero, senza bachi. Per fare un esempio che potrebbe non interessare molte persone, ma che affascina enormemente me, c'è un'intera libreria di calcolo matematico in precisione arbitraria che è formalmente verificata: https://gitlab.inria.fr/why3/whymp Va da sé che poi servirebbe anche la verifica formale del compilatore, la verifica formale dell'hardware sul quale il software gira... e negli utlimi, anni blasonate case produttrici di microprocessori ci hanno purtroppo abituato alla sciatteria più vergognosa. Ma tra la grande complessità e l'impossibilità matematica, c'è differenza :-D Chi in questi anni ha prodotto CPU scadenti, o venduto software con una bella confezione, tanta propaganda e poca qualità, non è giustificabile da una presunta impossibilità matematica di lavorare bene. Che poi errare sia umano (e perseverare anche) è cosa che tutti sappiamo, ma non ne facciamo una gistificazione matematica o scientifica, che sarebbe altra cosa. Cioè, se non vuoi "perdere i dati" allora significa che sono importanti e quindi dovresti avere già un backup e quindi anche se perdi i dati il problema non si pone :-D Esatto. Il metodo è: faccio backup, cancello la partizione, la ricreo GPT, ricopio i dati. Questo funziona al 100%, per forza. Questo metodo è lento... e non "funziona al 100%, per forza". Hai tenuto conto dei bachi del software per fare il backup? Della possibilità che il disco di backup sia difettoso? Un metodo più veloce nel caso medio e non troppo più lento nel caso peggiore e comunque più sicuro è: Faccio il backup (questo è imprescindibile) Non cancello i dati, ma uso il software che mi promette di funzionare nella maggior parte dei casi per fare la conversione. Controllo che tutto sia andato a buon fine, nel qual caso ho risparmiato un sacco di tempo. In caso contrario, recupero i dati dal backup direttamente nella nuova struttura di disco/partizioni/filesystem. È più sicuro, perché si rischia di perdere dati solo nel caso in cui la particolare configurazione risveglierà sia un bug nella procedura di backup/ripristino, sia in quella di conversione. La probabilità che entrambe siano bacate è più bassa della probabilità che anche solo una delle due lo sia. La cosa su cui tutti, mi pare, concordiamo è: fare copie di sicurezza, frequentemente e soprattutto (ma non solo) in occasione di operazioni delicate. Ĝis, m
Re: Ripristino GRUB2 e conversione GPT...
On Mon, Mar 01, 2021 at 06:19:47PM +0100, Alessandro Rubini wrote: > > Questo funziona al 100%, per forza. > > Ma hai appena detto che non e` possibile dimostrare che non ci sono > bachi in una procedura software. Amo i tecnici che si contraddicono. Non è una contraddizione. L'operazione (la copia di backup) può funzionare correttamente anche se il comando (cp, rsync, ecc.) ha sicuramente dei bachi. Inoltre la copia è verificabile, per esempio con un altro comando. Se due comandi completamente diversi danno lo stesso risultato è facile che sarà giusto (non hai la certezza matematica però). > Il tutto con massimo rispetto e pensato come critica costruttiva. > Chi non fa non sbaglia, e chi non parla non sparla. Certamente. -- Saluton, Marco Ciampa
Re: Ripristino GRUB2 e conversione GPT...
On Sat, Feb 27, 2021 at 01:55:15AM +0100, Sabrewolf wrote: > Non so se questi tools > garantiscono al 100% la riuscita dell'operazione ma forse è un falso > problema. NESSUN tool, né commerciale né libero, garantisce al 100% la riuscita dell'operazione. Equivarrebbe a dire che il sw è senza alcun baco, cosa che è dimostrabile matematicamente che è impossibile. > Cioè, se non vuoi "perdere i dati" allora significa che sono > importanti e quindi dovresti avere già un backup e quindi anche se perdi > i dati il problema non si pone :-D Esatto. Il metodo è: faccio backup, cancello la partizione, la ricreo GPT, ricopio i dati. Questo funziona al 100%, per forza. -- Saluton, Marco Ciampa
Re: [Forse un po' OT] Aiuto per uno script - RISOLTO
Il Lun 1 Mar 2021, 15:48 Enrico Agliotti ha scritto: ... > Le virgolette attorno alla variabile in effetti sono importanti (mi scuso > per > ... Di nuovo grazie ancora. Ho risolto in altro modo: ravanando ancora un po', ho trovato questi due siti che fanno al mio caso, specie il secondo e quel programmino è anche in Buster! https://grammarofdev.blogspot.com/2012/05/copy-files-in-order-using-linux-or-os-x.html https://fatsort.sourceforge.io/ Ho però un dubbio, in pratica riordinando la fat della chiavetta, scrive molte più volte che non usandolo e questo deteriorerà la pennetta in modo più rapido. È corretto? Buona serata a tutti Giuliano
Re: [Forse un po' OT] Aiuto per uno script
Il giorno sab 27 feb 2021 alle ore 10:24 Davide Prina < davide.pr...@gmail.com> ha scritto: > 2) reimpostare IFS per evitare che il ciclo for spezzi i nomi contenenti > spazi, es: > OLDIFS=$IFS > IFS=" > " > for ... > ... > done > IFS=$OLDIFS > Le virgolette attorno alla variabile in effetti sono importanti (mi scuso per la dimenticanza) ma questo perché? Ho provato anche a impostare IFS=" " e mi sembra funzioni comunque. Grazie Enrico -- Inviato dal computer che sto usando in questo momento Enrico Agliotti cell. +39-328-0517312 tel. con segreteria: +39-011-23415553
Re: errore signature verification in testing
Il 26/02/21 18:08, liste DOT girarsi AT posteo DOT eu ha scritto: Il 26/02/21 08:21, Piviul ha scritto: Ciao a tutti, è qualche giorno che ricevo questo errore durante l'update: $ sudo apt update Get:1 http://deb.debian.org/debian bullseye InRelease [142 kB] Err:1 http://deb.debian.org/debian bullseye InRelease Unknown error executing apt-key Ho provato adesso, non mi da nessun errore, riprova adesso, forse era giù il server, o c'erano problemi. No, l'errore continua... si dev'essere corrotto qualcosa: $ sudo apt update Scaricamento di:1 http://deb.debian.org/debian bullseye InRelease [142 kB] Errore:1 http://deb.debian.org/debian bullseye InRelease Errore sconosciuto durante l'esecuzione di apt-key Lettura elenco dei pacchetti... Fatto Generazione albero delle dipendenze... Fatto Lettura informazioni sullo stato... Fatto Tutti i pacchetti sono aggiornati. W: Si è verificato un errore nel verificare la firma. Il repository non è aggiornato e verranno usati i file indice precedenti. Errore GPG: http://deb.debian.org/debian bullseye InRelease: Errore sconosciuto durante l'esecuzione di apt-key W: Impossibile recuperare http://deb.debian.org/debian/dists/bullseye/InRelease Errore sconosciuto durante l'esecuzione di apt-key W: Impossibile scaricare alcuni file di indice: saranno ignorati o verranno usati quelli vecchi. :( Piviul
