Projets-App
Projets
Editer un projet
Cadre de travail
Unité de recherche rattachée au CNRS
IRIF
LIPN
LMF
Information du ou de la responsable scientifique du projet :
Prénom
Nom
E-mail
Présentation du projet scientifique
Nom du project
Résumé publiable du projet (10 lignes max.)
The goal of this project is to develop and implement a framework that aids smart contract designers, including those without expertise in formal methods, in designing and implementing correct contracts. Our aim is to prevent vulnerabilities that could compromise the security of SCs, thereby delivering more reliable and trustworthy SC‐based applications to users.The ultimate goal of this project is to develop and implement a framework that aids smart contract designers, including those without expertise in formal methods, in designing and implementing correct contracts. Our aim is to prevent vulnerabilities that could compromise the security of SCs, thereby delivering more reliable and trustworthy SC‐based applications to users.
Champs thématiques adressés (séparés par des virgules)
Type
proof-of-concept
prototype
maintenance/évolution logiciel existant
prématuration
Décrivez les innovations attendues à l'issue du projet (5 lignes max.)
Improve SOLIDITY-TO-CPN tool from practical perspectives: - Guide the user, through the interface of the tool, to define vulnerability as well as specific properties and generate the appropriate temporal formula to be checked. - Translate back the output of Helena model-checker tool into a comprehensive format.
Argumentaire scientifique qui décrit le projet, l'état de l'art, les travaux antérieurs et les résultats attendus (20 lignes max.)
Blockchain technology, with its security and transparency features, has revolutionized industries by providing a decentralized platform for secure transactions. Smart contracts, within this ecosystem, automate digital agreements, holding potential applications from finance to supply chain management. However, ensuring their reliability is crucial to avoid costly errors and vulnerabilities. Numerous attacks on Blockchain platforms have exploited vulnerabilities in smart contracts, highlighting the need for robust verification methods. To mitigate the risks of deploying faulty SCs, several methods and tools have been proposed. Most existing formal approaches focus on analysing EVM (Ethereum Virtual Machine) bytecode rather than the higher‐level Solidity (a mainstream language for writing SCs) source code. Working on SCs code instead of EVM bytecode, that we defend in the present project, opens the door to reduce the complexity of the verification process. Indeed, the SC code consists, in general, in small programs that abstract low level details that could be necessarily pertinent for the verification of the properties of in‐ terest. Current methods may also produce false positives, identifying vulnerabilities that do not actually exist. Moreover, these approaches are restricted to checking contract‐specific properties, and fail to account for interactions between multiple SCs within the same system. The ultimate goal of our work is to develop and implement a framework that aids smart contract designers, including those without expertise in formal methods, in designing and implementing correct contracts. Our aim is to prevent vulnerabilities that could compromise the security of SCs, thereby delivering more reliable and trustworthy SC‐based applications to users.
Description du besoin en ingénierie
Évaluez le temps ingénieur dont vous avez besoin pour votre projet:
Frequence
2 jour/semaine
3 jour/semaine
Durée
1 mois
2 mois
3 mois
4 mois
5 mois
6 mois
Quelles sont les compétences spécifiques d'ingénierie attendues ; notamment, langages ou frameworks qui seront utilisés dans le projet, outils existants, connaissances requises ?
C++
Décrivez les activités qui seront confiées à·aux ingénieur·e·s (si possible, avec un planning de tâches attendues)
T1 - Guide the user, through the interface of the tool, to define vulnerability as well as specific properties and generate the appropriate temporal formula to be checked. T2 - Translate back the output of Helena model-checker tool into a comprehensive format.
Commentaires
Mettre à jour