LIP6, salle 56-66/201 BIS Instructions pour venir ici.
Abstract : By applying decades of top-notch formal verification know-how to the blockchain space, Dowsers brings trust in smart contracts with a ground-breaking, scalable and accessible formal verification technology. Bugs and vulnerabilities in smart contract code erode trust in blockchain technology, posing a significant risk to developers, investors, and financial institutions. Dowsers is a suite of software tools and algorithms which automatically verify and formally prove the safety and providence of smart contracts before or after their deployment on a blockchain.
Abstract : The analysis of timed properties of programs is a complex task, as it is highly dependent on both the software and the hardware. In this work, we propose a framework for modeling with timed formal models the execution of programs, taking into account the micro-architecture of the machine on which it executes. We model both the program, at the instruction set architecture level, and the hardware, including the processor micro-architecture, using time Petri nets. Our implementation uses the ARM Cortex-M instruction set architecture and a hardware architecture representative of micro-controllers used in IoT nodes. The whole translation is fully automated and allows, starting from binary code, to automatically produce the models usable by the state-of-the-art time Petri net model checker Roméo. In addition, and as a proof of concept, we show how we can check, and enforce to some extent, opacity properties on programs, leveraging the ability of Roméo to verify a parametric timed extension of the classical computation tree logic.