Extraction of Dead Atomic Conditions for Smart Contracts

(Tutorials)

Objective

Smart contracts are the scripts holding the properties to perform the activities in Blockchain. Advances in blockchain technologies enable the society towards trust-based applications. Smart contracts are prepared between the parties to hold their requirements and promises. If the deal held by a smart contract is huge and expensive, then there is a high chance of attracting issues and loss of assets. This necessitates the verification and testing of a smart contract. Since we have the source code of a smart contract, then it is easy to apply white-box testing approaches. In this work, we present an approach for generating test cases to satisfy condition coverage of smart contracts using a solidity bounded model checker. We annotate the original smart contract as per the condition coverage specification and drive the bounded model checker to prove the feasibility of the asserted properties. Finally, we collect all feasible targets and show the condition coverage score. Also, the proposed approach generates test input values for each feasible atomic condition. Our work can be utilised to certify any smart contract to check whether the Optimal or Maximal condition coverage is achieved or not.

Framework:

Target audience

The target audience include Master students, Ph.D. Scholars, Faculties, and Industry personnel.

Speaker's Profile: Sangharatna Godboley

Dr. Sangharatna Godboley did his M.Tech (2011-2013) and Ph.D. (2014-2017) from National Institute of Technology Rourkela, India. He worked as a Researcher (Aug 2017 - Jan 2018) in the School of Computing, National University Singapore. He worked as a Postdoctoral Research Fellow (Feb 2018 to June 2020) in the School of Computing, National University Singapore. Currently, He is working as an Assistant Professor in the Department of Computer Science and Engineering, National Institute of Technology Warangal, India. Broadly, my area of interests are Program Analysis, Software Testing, Security, Verification, Smart Contracts. Specifically, He is working on Bounded Model Checking, Fuzzing, Dynamic Symbolic Execution (DSE), Mutation Testing, and Combinatorial Testing. He is interested in using program analysis techniques to solve the problems of software testing. He is focusing on Modified Condition / Decision Coverage (MC/DC), Short-circuit Multiple Condition Coverage (SC-MCC), and Relational Operator Replacement (ROR) Mutants. He is a team member of Tracer-X Research group (https://github.com/tracer-x).

Duration
  • Half Day