1,720,970 research outputs found
Resilience of Hybrid Casper under varying values of parameters
Full text linkHybrid Casper is the new Ethereum blockchain protocol that uses both Proof of Work and Proof of Stake to reach a consensus between nodes. Here, we analyse the protocol using PRISM+, an extension of the probabilistic model checker PRISM with primitives for expressing blockchain data types. First, we extend PRISM+ to include data types and operations for modelling and analysing Proof of Stake-based consensus protocols. Then, we model Hybrid Casper in PRISM+ as a parallel composition of stochastic processes, thus precisely describing the behaviour of the protocol and highlighting its corner cases. PRISM+ is therefore used to rapidly and automatically analyse the resilience of Hybrid Casper when tuning, up or down, several basic parameters of the protocol, such as the rates of creating blocks, and the strategies for determining penalties. Finally, we study the robustness of Hybrid Casper to two well known attacks: the Eclipse attack and the majority attack
Pacta sunt servanda: Legal contracts in Stipula
Full text linkWe present Stipula, a domain specific language that may assist legal practitioners in programming legal contracts through specific patterns. The language is based on a small set of programming abstractions that correspond to common patterns in legal contracts. We illustrate the language by means of two paradigmatic legal contracts: a bike rental and a bet contract. Stipula comes with a formal semantics, an observational equivalence and a type inference system, that provide for a clear account of the contracts' behaviour and illustrate how several concepts from concurrency theory can be adapted to automatically verify the properties and the correctness of software-based legal contracts. We also discuss a prototype centralized implementation of Stipula
Utilizzo dei Carbon Token nella microeconomia: Il progetto “San Marino Low Carbon Ecosystem”
Full text linkAnalisi di un ecosistema a basse emissioni di anidride carbonica che coinvolga i cittadini nella lotta per l'ambiente. Proposta di idee per realizzare un tale ecosistema su scala nazionale italiana
Implementazione e test di SafeDrug un sistema di tracciabilità di farmaci basato su blockchain
No full textAttualmente la tecnologia blockchain sta emergendo in differenti ambiti e si sta ponendo come soluzione a diverse problematiche. In ambito sanitario, ad esempio, contrasta il fenomeno della contraffazione e del danneggiamento dei medicinali durante la distribuzione. Questa tesi analizza le fasi e gli attori della catena di distribuzione farmaceutica, mostra i vantaggi e gli svantaggi che derivano da un eventuale adozione della tecnologia blockchain nel settore sanitario, le linee guida per la progettazione e lo stato dell'arte con illustrazione di tre diverse realtà attuali. Inoltre viene presentata l'implementazione di un nuovo sistema, SafeDrug, che tramite blockchain, traccia i medicinali attraverso le aziende farmaceutiche, i corrieri e le farmacie e, ne permette una diffusione sicura e controllata lungo tutta la filiera. Infine viene trattata la fase di testing, l'implementazione e il funzionamento della Demo che mostra i diversi casi di esecuzione del sistema e la relativa sequenza degli eventi
An Analysis of the Ethereum Proof of Stake Protocol
Full text linkLa tesi indaga il protocollo Gasper della blockchain Ethereum, utilizzando una versione estesa del model checker Prism per quanto riguarda la simulazione e la verifica. Gasper rappresenta un significativo passo avanti nell’evoluzione di Ethereum, introducendo un nuovo meccanismo di consenso e affrontando le sfide della scalabilità. Questo lavoro mira a modellare e a valutare il protocollo Gasper in modo sperimentale, verificandone la coerenza e la robustezza, alla ricerca di vulnerabilità rispetto a vari attacchi.
Lo studio comprende un’analisi completa della transizione di Ethereum dalla Proof of Work (PoW) alla Proof of Stake (PoS), chiarendo le motivazioni e i vantaggi di questo cambiamento fondamentale.
Inoltre, approfondisce le caratteristiche uniche di Gasper e i miglioramenti rispetto ai suoi predecessori, come Hybrid Casper, evidenziando il suo ruolo nel raggiungimento di maggiore sicurezza e scalabilità.
Uno degli obiettivi principali della ricerca è la validazione del modello realizzato tramite Prism+ rispetto ai complessi requisiti di Gasper, garantendo che il modello simulato rifletta accuratamente il comportamento del protocollo. Attraverso test e verifiche, questo studio mira a fornire preziose informazioni sulla sua robustezza e affidabilità.
Inoltre, la tesi esplora potenziali attacchi al protocollo Gasper in modo teorico e pratico, valutandone la resilienza rispetto alle strategie avversarie. Identificando vulnerabilità e punti deboli, la ricerca contribuisce a migliorare la sicurezza del protocollo e a guidarne l’ulteriore sviluppo. Questa tesi offre un esame del protocollo Gasper di Ethereum, combinando l’analisi teorica con la simulazione pratica utilizzando il model checker Prism+. Lo studio comprende la transizione da PoW a PoS, i progressi di Gasper, la convalida della coerenza del modello e l’analisi della sicurezza, contribuendo alla continua evoluzione della tecnologia blockchain di Ethereum
Modelizzazione e analisi del protocollo Algorand
Full text linkLa tecnologia emergente delle blockchain sta attirando sempre più attenzioni portando alla creazione di una grande quantità di sistemi che adottano questa tecnologia. Il veloce sviluppo che hanno avuto dalla creazione di Bitcoin sta portando alla luce i problemi di scalabilità, efficienza e velocità che l’approccio Proof of Work porta con sè. In questa tesi esamineremo Algorand, una blockchain recente, basata sulla Proof of Stake, che si propone di arginare queste problematiche, sviluppandone un modello e testandolo con il tool di analisi statistica PRISM e verificandone sperimentalmente la resistenza alle fork e la rapidità nella creazione di nuovi blocchi, per poi modellizzare un possibile attacco tramite una partizione della rete e verificarne il comportamento anche in questo caso
A technique for detecting wait-notify deadlocks in Java
Full text linkDeadlock analysis of object-oriented programs that dynamically create threads and objects is complex, because these programs may have an infinite number of states.
In this thesis, I analyze the correctness of wait - notify patterns (e.g. deadlock freedom) by using a newly introduced technique that consists in an analysis model that is a basic concurrent language with a formal semantic. I detect deadlocks by associating a Petri Net graph to each process of the input program. This model allows to check if a deadlock occur by analysing the reachability tree.
The technique presented is a basic step of a more complex and complete project, since in my work I only consider programs with one object
La base di Bernstein in spazi polinomiali generalizzati a tratti
No full textLe funzioni polinomiali possono essere utilizzate per approssimare le funzioni continue. Il vantaggio è che i polinomi, le loro derivate e primitive, possono essere rappresentati in maniera semplice attraverso i loro coefficienti ed esistono algoritmi stabili e veloci per valutarli. Inoltre gli spazi polinomiali godono di numerose proprietà importanti.
In questo lavoro ci occuperemo di altri spazi funzionali, noti in letteratura come spazi di Chebyshev o polinomi generalizzati, per ragioni di riproducibilità. Infatti ciò che si ottiene attraverso i polinomi è soltanto una approssimazione che spesso risulta essere insufficiente. E' importante, quindi, considerare degli spazi in cui sia possibile avere una rappresentazione esatta di curve. Lo studio di questi spazi è possibile grazie alla potenza di elaborazione degli attuali calcolatori e al buon condizionamento di opportune basi di rappresentazione di questi spazi. Negli spazi polinomiali è la base di Bernstein a garantire quanto detto. Negli spazi di Chebyshev si definisce una nuova base equivalente. In questo lavoro andremo oltre gli spazi di Chebyshev ed approfondiremo gli spazi di Chebyshev a tratti, ovvero gli spazi formati dall'unione di più spazi del tipo precedente. Si dimostrerà inoltre l'esistenza di una base a tratti con le stesse proprietà della base di Bernstein per gli spazi polinomiali
Analisi dei più diffusi Algoritmi di consenso Blockchain
No full textLa nostra epoca è caratterizzata da innovazioni tecnologiche continue, alcune delle quali rappresentano delle vere e proprie sfide a sistemi esistenti e consolidati. Una di queste è sicuramente la tecnologia blockchain che, grazie ai suoi meccanismi, ha permesso di introdurre il concetto di criptovaluta, una moneta digitale (denominata anche criptomoneta) che può essere scambiata alla pari di quella cartacea.
Il grande successo di Bitcoin, la prima grande implementazione del concetto di criptovaluta, ha portato alla nascita di altre numerose monete digitali e ha favorito l’idea che la tecnologia blockchain potesse essere impiegata anche in ambiti diversi dai sistemi finanziari.
Con questo elaborato si intende dare un quadro dettagliato del funzionamento dei più diffusi algoritmi di consenso ad oggi esistenti nel panorama della tecnologia blockchain.
In particolare sono stati analizzati gli algoritmi Proof of Work, Proof of Stake, Delegated Proof of Stake e Proof of Authority (Aura e Clique).
Per ogni algoritmo di consenso sono state analizzate le principali differenze e sono stati realizzati degli algoritmi in pseudocodice per spiegare il funzionamento della creazione dei nuovi blocchi.
In conclusione si proporrà un’analisi comparativa degli algoritmi di consenso analizzati, dal punto di vista delle caratteristiche maggiormente desiderabili e delle prestazioni di un sistema blockchain
Implementazione di un Voting System su Blockchain
Full text linkIn questo documento si andranno ad analizzare i sistemi di voto, dai piu` antichi risalenti all’epoca romana, fino ad i più moderni utilizzati nei vari paesi del mondo ai giorni nostri. Parleremo delle varie tecnologie di voto ed innovazioni che si sono avvicendate nel trascorrere del tempo e di tutte le problematiche relative ad esse. Andremo ad analizzare nel dettaglio i più moderni sistemi di voto elettronici e la loro struttura. Si andrà quindi a definire una nuova e recente tecnologia, la blockchain e si andrà a spiegarne in dettaglio il funzionamento ed i maggiori algoritmi di consenso distribuito relativi ad essa. Infine verra` spiegato il progetto realizzato utilizzando la blockchain. Il progetto consiste in un innovativo sistema di voto elettronico decentralizzato, si andranno ad analizzare i vari componenti del sistema, le proprietà di voto mantenute nel sistema e i vari vantaggi e svantaggi che questa tecnologia se applicata potrebbe portare nel mondo moderno
- …
