A bounded model checker for web cryptocurrency wallets

Cryptocurrency wallets play a crucial role in the web3 ecosystem, not only managing keys but also facilitating interaction with decentralized applications and protecting valuable assets. Web3 and also web crypto wallets are often targeted by attackers, and a single exploit can result in millions of dollars in losses. Testing these wallets presents unique challenges due to the combined complexities of browser extensions and crypto wallets, including the absence of a precise failure state. In this work, we present an automated approach based on bounded model checking, to test the expected wallet's behavior. Using our framework, we were able to perform a systematic analysis of different versions of a popular web crypto wallet. We examined their behavior under various conditions such as heavy loads and overlapping actions, triggering some issues and errors difficult to be addressed by manual analysis. Moreover, we also applied our framework to model and re-discover a real-world vulnerability, and finally, test the patch against new wallet versions.

I portafogli di criptovalute svolgono un ruolo cruciale nell'ecosistema Web3, non solo nella gestione le chiavi crittografiche, ma anche facilitando l'interazione con le applicazioni decentralizzate e proteggendo beni preziosi. Il web3 e anche i portafogli di criptovalute web sono spesso presi di mira dagli attaccanti e un singolo attacco può causare perdite di milioni di dollari. Il test di questi portafogli presenta sfide uniche a causa della complessità combinata data delle estensioni del browser e dei portafogli di criptovalute, compresa l'assenza di uno stato di fallimento preciso. In questo lavoro, presentiamo un approccio automatizzato basato sulla verifica di un modello vincolato, per testare il comportamento aspettato del portafoglio. Utilizzando il nostro sistema, siamo stati in grado di eseguire un'analisi sistematica di diverse versioni di un popolare portafoglio di criptovalute web. Abbiamo esaminato il loro comportamento in varie condizioni, come carichi pesanti e sovrapposizione di azioni, innescando alcuni problemi ed errori. Inoltre, abbiamo anche applicato il nostro sistema per modellare e riscoprire una reale vulnerabilità e, infine, testare la mitigazione sulle nuove versioni del portafoglio.