USSC

Usable Security of Smart Contract Development and Verification

This project will apply state-of-the-art scientific methods from usable security research in order to adapt Smart Contract tools to the developers’ needs, and create templates, which aid developers in SC scripting, designing, and formal verification. A wide range of industrial use cases will directly benefit from the increase in usability and security of SCs and their development tools.

Motivation

Smart contracts (SCs) are computer programs that build up on blockchain technology to ensure secure distributed computation in trustless environments and have recently received increased attention in industry and academia. Along with their growing adoption in various business applications, a plethora of attacks caused by programming errors has been reported. These incidents led to tremendous financial losses and service disruptions. To defeat such attacks, various approaches have been suggested in the academic community. However, these approaches lack usability and hence, the proposed tools are rarely adopted for real-world applications. Scripting-languages are to a large extent non-intuitive and do not offer appropriate constructs to deal with such aspects. Moreover, the available tools for debugging lack interactive support and formal verification tools are in practice hard to use since they require a formal representation of the SC, whose specification is complex.

Expected Outcome

We will extend current SC debugging tools to best guide developers through code auditing in real-world scenarios. Regarding formal verification tools, this project will create approaches to aid developers in constructing sound formal models, which is crucial for meaningful verification results. Moreover, we will develop templates mapping the developers’ intentions (in natural language) to actual code snippets in order to ensure that the complexity of human reasoning is correctly translated to SC implementations. It is our overall aim that SC developers are not required to have specialized IT knowledge and profound background in SC programming in order to use SC tools. We are confident that our work will yield useful tools and templates, which will effectively increase the security of SC code before deployment.

Further Information

• The project is led by SBA Research.
• This FFG programme is sponsored by Nationalstiftung für Forschung, Technologie und Entwicklung and Österreich-Fonds. The focus lies on funding industrial PhD projects to improve qualifications of research and innovation staff in companies and non-university research institutions.  An Industrial PhD project is performed by an employee of an Austrian company/non-university research institution, who is enrolled as a PhD student at a university during the whole project.